## Stream: maths

### Topic: linear_isometry_complex

#### François Sunatori (Mar 14 2021 at 20:12):

Hi,
I've been working on proving the following lemma since last week:

import analysis.complex.basic

open complex

local notation | x | := complex.abs x

lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z)) :=
begin
sorry
end


I proved another helper lemma:

lemma linear_isometry_complex' (z : ℂ) (h : ℂ →ₗᵢ[ℝ] ℂ) :
h 0 = 0 → h 1 = 1 → ((h z = z) ∨ (h z = conj z)) :=
begin
...
end


I would now like to use the helper lemma linear_isometry_complex' in my proof of linear_isometry_complex and am uncertain how to go at this.
Since linear_isometry_complex has a ∃ a : ℂ, |a| = 1, I wanted to use:

use exp ^ I * θ


and I need to define a function, say h that will fit the hypotheses of linear_isometry_complex':
h 0 = 0 and h 1 = 1
for h 0 = 0I can use linear_isometry.map_zero, but I get stuck with the definition of h because I would need to take in θ as an argument.
I'm wondering if I'm going in a good direction here or if there is a way to define this h function without using exp ^ I * θ.

#### Heather Macbeth (Mar 14 2021 at 20:20):

How about defining a := f 1 and then letting h be a⁻¹ • f, (i.e., λ z, a⁻¹ * f z, but the first definition will make it automatically a linear map)?

#### François Sunatori (Mar 14 2021 at 20:30):

ok nice thanks, then there is no need to define a θ. I'll try it out!

#### Heather Macbeth (Mar 14 2021 at 20:42):

By the way, conj a might work more nicely than a⁻¹, I'm not sure, you could try it both ways!

#### Kevin Buzzard (Mar 14 2021 at 20:49):

The advantage of conj a is that you don't need to get division involved, which is in general a good idea (you can use ring to do your algebra, for example, if division is not involved).

#### François Sunatori (Mar 14 2021 at 20:54):

thanks for the tips :)

#### François Sunatori (Mar 14 2021 at 20:55):

btw for the definition of h I'm guessing I need to do something like:

h : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a⁻¹ * f z
, map_smul' := sorry
},


otherwise I'll just get a h with type ℂ → ℂ

#### Kevin Buzzard (Mar 14 2021 at 20:59):

If your f is already linear then just bub it with conj a like Heather said and hopefully you won't need to fill in those sorries

#### Kevin Buzzard (Mar 14 2021 at 21:00):

Bubbing should send a linear map to a linear map

#### Heather Macbeth (Mar 14 2021 at 21:01):

@Kevin Buzzard I guess François is saying that he can't do this because f lives in ℂ →ₗᵢ[ℝ] ℂ which is only a real vector space, not complex? My bad.

#### François Sunatori (Mar 14 2021 at 21:10):

Sorry if I'm not understanding completely.. I'm still new to Lean. @Kevin Buzzard What does bubbing mean (does it mean that Lean will just understand the type of h from using conj)? and I'm still unsure about the meaning of the notation ℂ →ₗᵢ[ℝ] ℂ.. I know it is some sort of linear map but not sure what the ᵢ stands for, nor the [ℝ].

#### Heather Macbeth (Mar 14 2021 at 21:16):

Indeed, one limitation of Lean's tools is that it can be hard to discover where a notation is defined. ℂ →ₗᵢ[ℝ] ℂ is notation for docs#linear_isometry, here an ℝ-linear map from ℂ to ℂ which also preserves lengths.

#### Heather Macbeth (Mar 14 2021 at 21:17):

So, in your constructor, you'll have

h : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a⁻¹ * f z,
map_smul' := sorry,
norm_map' := sorry },


#### François Sunatori (Mar 14 2021 at 21:22):

ok right, that's what I observed (Lean was asking me to provide something for norm_map' as well and I imagine this case isn't one where bubbing will work? (since for me just setting h := λ z, a⁻¹ * f z directly gives ℂ → ℂ instead of ℂ →ₗᵢ[ℝ] ℂ)

#### Heather Macbeth (Mar 14 2021 at 21:25):

Right ... the property norm_map' is not preserved under scalar multiplication/\bub/• !

#### Kevin Buzzard (Mar 14 2021 at 22:45):

@François Sunatori sorry to mislead you! Bub is \bub, the dot. But as you have pointed out you might not be able to use it (I was reading on my phone and couldn't even see the little l and i because of a font issue). Yes why not just make it a function, and then beef it up to a linear isometry manually, the way you originally said. By the way if you write def foo : ℂ →ₗᵢ[ℝ] ℂ := {! !} and then click on the light bulb and then click on the bottom-but-one option (something about fields of a structure) then it will print out all the fields of the structure which you need to fill in.

#### François Sunatori (Mar 15 2021 at 01:24):

@Kevin Buzzard Thanks for the clarification about the bub (I was searching for that word in the codebase but didn't find anything related to what we were talking about haha, but I just tried typing \bub now and indeed it gives the •)! and also thanks for the trick involving {! !}. I didn't know I could do that.

#### François Sunatori (Mar 21 2021 at 21:59):

I've gotten further in the proof of linear_isometry_complex but not as quickly as I did with linear_isometry_complex'

import analysis.complex.basic

open complex

local notation | x | := complex.abs x

lemma linear_isometry_complex (z : ℂ) (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 → ((f z = a * z) ∨ (f z = a * conj z)) :=
begin
have h : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, (f 1)⁻¹ * f z,
intros x y,
},
map_smul' := by {
intros m x,
rw linear_isometry.map_smul,
rw algebra.mul_smul_comm,
},
norm_map' := by {
intros x,
simp,
rw ← complex.abs_inv,
rw ← complex.abs_mul,
sorry
},
},
use f 1,
intros f1,
{
have H0 : h 0 = 0 := linear_isometry.map_zero h,
have H1 : h 1 = 1 := by {
-- TODO from use to_fun definition: λ z, (f 1)⁻¹ * f z?
sorry,
},
-- TODO from use to_fun definition: λ z, (f 1)⁻¹ * f z?
exact (linear_isometry_complex' z h H0 H1),
sorry
},
end


I'm left with 3 sorrys. I'm trying to tackle the proof of have H1 : h 1 = 1.
I'm not sure how to apply λ z, (f 1)⁻¹ * f z that I defined in h.to_fun.
Once I write a proof for a field in an instance of a Lean record, can I invoke h.to_fun and use it with exact or rw for example?

Thanks :)

#### Kevin Buzzard (Mar 21 2021 at 22:35):

You're proving the wrong thing:

lemma linear_isometry_complex (z : ℂ) (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 → ((f z = a * z) ∨ (f z = a * conj z)) :=
begin
use 0,
intro h,
simp at h,
cases h,
end


This says "there exists a complex number a such that if |a|=1 then something is true" so you can prove it by supplying any complex number whose norm isn't 1.

#### François Sunatori (Mar 21 2021 at 22:38):

Oh ok... so in that case it needs to be:

lemma linear_isometry_complex (z : ℂ) (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((f z = a * z) ∨ (f z = a * conj z))


?
(replace the → with ∧)

#### François Sunatori (Mar 21 2021 at 22:46):

but I would still like an answer to the following question:

I'm not sure how to apply λ z, (f 1)⁻¹ * f z that I defined in h.to_fun.
Once I write a proof for a field in an instance of a Lean record, can I invoke h.to_fun and use it with exact or rw for example?

#### Heather Macbeth (Mar 21 2021 at 22:48):

Instead of have, use let; have forgets the definition, let remembers it.

#### Heather Macbeth (Mar 21 2021 at 22:48):

Thus,

let h : ℂ →ₗᵢ[ℝ] ℂ :=


#### Heather Macbeth (Mar 21 2021 at 22:48):

Then, when the time comes to remember how h was defined, you can do something like rw h or simp only [h] or unfold h.

#### Kevin Buzzard (Mar 21 2021 at 22:52):

I think you're going the wrong way with the first sorry. You have to use that |f(x)|=|x|. How about

      norm_map' := by {
intros x,
simp,
change ∥f 1∥⁻¹ * ∥f x∥ = ∥x∥,
rw linear_isometry.norm_map,
rw linear_isometry.norm_map,
simp,
},


#### Kevin Buzzard (Mar 21 2021 at 22:55):

For the others, I think Heather's advice on let v have should see you through.

While I'm here I should point out that in early 2018 I was running around on the Lean chat going "me and a bunch of undergraduates have defined schemes!" and there were essentially no other number theorists or algebraic geometers here at the time, so the definition just sat there for a while with the computer scientists looking bemusedly at it, and then Johan Commelin showed up, took one look at the definition and said "you know that ->, don't you think it should be an \and?"

#### François Sunatori (Mar 21 2021 at 23:00):

Thanks @Kevin Buzzard for the trick to change to ∥-∥.. I actually wasn't too sure how far I would be able to get with route I had taken. And thanks for the story ! I guess I'll remember to watch out for that one in the future!

#### François Sunatori (Mar 21 2021 at 23:01):

Thank you @Heather Macbeth let is exactly what I need! I guess I should have tried let in the first place.. I think I wrongly assumed that it was a synonym for have and maybe the parts of mathlib I was looking at weren't using let so much.

#### Kevin Buzzard (Mar 21 2021 at 23:20):

have is for proofs, let is for data.

#### François Sunatori (Mar 22 2021 at 00:25):

Heather Macbeth said:

Then, when the time comes to remember how h was defined, you can do something like rw h or simp only [h] or unfold h.

In the proof for

let H1 : h 1 = 1


When I try to use rw h or unfold hI get

rewrite tactic failed, lemma is not an equality nor a iff


but using simp only [h]
gives me
A: ⇑{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _} 1 = 1
and I would like to apply λ (z : ℂ), a⁻¹ * ⇑f z to 1
so I tried using simp (which simplified the expression and applied λ (z : ℂ), a⁻¹ * ⇑f z when I used it norm_map') but it gives me simplify tactic failed to simplify.
How would I go at getting λ (z : ℂ), a⁻¹ * ⇑f z out of A?

#### Heather Macbeth (Mar 22 2021 at 01:19):

@François Sunatori Does it work to do simp rather than simp only?

#### François Sunatori (Mar 22 2021 at 01:20):

no...

let H1 : h 1 = 1 := by {
simp,
}


gives

simplify tactic failed to simplify


#### Heather Macbeth (Mar 22 2021 at 01:21):

Sorry, I should have been more precise. I meant you to keep the h -- simp [h] rather than simp only [h].

#### François Sunatori (Mar 22 2021 at 01:23):

oh ok, yes it works but it gives me the same result as simp only [h]

⇑{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _} 1 = 1


#### François Sunatori (Mar 22 2021 at 01:25):

I would still need some way to get λ (z : ℂ), a⁻¹ * ⇑f z out somehow... when I worked on the proof for norm_map' in the definition of h, I was able to use simp to get λ (z : ℂ), a⁻¹ * ⇑f z out and apply it to an argument, but not in this case...

#### Heather Macbeth (Mar 22 2021 at 01:28):

Ah, I see! OK, here's a line that seems to do it:

change (f 1)⁻¹ * f 1 = 1,


Basically this is the come_on_lean tactic that people joke about ...

#### Heather Macbeth (Mar 22 2021 at 01:29):

That is, we're instructing Lean to check that the following statement is definitionally equal to our goal.

#### François Sunatori (Mar 22 2021 at 01:29):

oh lol I haven't heard about that one yet!

#### François Sunatori (Mar 22 2021 at 01:29):

could it be because in the case of norm_map' I was dealing with

⇑{to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}


while this time I'm dealing with

⇑{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _}


where to_fun is a level deeper?

Seems plausible!

#### François Sunatori (Mar 22 2021 at 01:31):

Thanks a lot! I really couldn't wrap my head around why it worked for norm_map' but not in this case (I still don't know why but at least I have a workaround now!)

#### Heather Macbeth (Mar 22 2021 at 01:32):

There are not many uses of change in mathlib, because usually each definition (in the library proper rather than a definition hidden inside a proof like yours is) is immediately followed by a lemma which unfolds that definition, whose proof is rfl. Often this "definition-unfolding" lemma is even a simp-lemma.

#### François Sunatori (Mar 22 2021 at 01:35):

Oh I see. Would it make sense to have that extra lemma or is it so specific that it doesn't really make sense to define it outside of this proof?

#### Heather Macbeth (Mar 22 2021 at 01:38):

I'd say, not at this stage. That sort of "infrastructure" can be figured out after everything else is working.

#### Heather Macbeth (Mar 22 2021 at 01:41):

By the way, here's an example of the kind of thing I was describing: see how the imaginary part function docs#complex.im_clm, as a continuous linear map, is immediately followed by a simp-lemma docs#complex.im_clm_apply explaining what it does as a function.

#### Scott Morrison (Mar 22 2021 at 01:44):

(I tend to write my @[simp] lemmas as soon as they're needed --- every time I try simp and it doesn't solve the goal, I stop to think if a lemma is missing. Life is so much easier once they're in place.)

#### François Sunatori (Mar 22 2021 at 01:47):

Oh yes I remember seeing a few of those rfl lemmas often just after a definition.. Thanks, now I understand why they're there!

#### François Sunatori (Mar 22 2021 at 02:08):

Interestingly when I try the next step to go from (f 1)⁻¹ * f 1 = 1 to 1 = 1,

let H1 : h 1 = 1 := by {
change (f 1)⁻¹ * f 1 = 1,
rw mul_left_inv (f 1),
...
}


I get

failed to synthesize type class instance for
z : ℂ,
f : ℂ →ₗᵢ[ℝ] ℂ,
a : ℂ := ⇑f 1,
h : ℂ →ₗᵢ[ℝ] ℂ :=
{to_linear_map := {to_fun := λ (z : ℂ), a⁻¹ * ⇑f z, map_add' := _, map_smul' := _}, norm_map' := _},
H0 : ⇑h 0 = 0 := h.map_zero
⊢ group ℂ


but when I look in analysis.normed_space.linear_isometry I see an instance : group (E ≃ₗᵢ[R] E) with mul_left_inv defined..
Is there something I'm missing to make Lean aware that f has access to mul_left_inv?

#### François Sunatori (Mar 22 2021 at 02:09):

I also tried adding import analysis.normed_space.linear_isometry but it didn't change anything

#### Heather Macbeth (Mar 22 2021 at 02:13):

Careful, ℂ ≃ₗᵢ[ℝ] ℂ is a group but ℂ itself is not a group!

#### Heather Macbeth (Mar 22 2021 at 02:13):

Because 0 is not invertible.

oh right! oups

#### Heather Macbeth (Mar 22 2021 at 02:19):

Instead of the lemma docs#mul_left_inv (for groups only), you want to use the lemma docs#inv_mul_cancel.

#### François Sunatori (Mar 22 2021 at 02:22):

Ok nice and then I need to supply a proof that a ≠ 0

#### François Sunatori (Mar 23 2021 at 00:06):

I'm now running into an awkward situation..

I have

⇑f z = a * z ∨ ⇑f z = a * ⇑conj z


and would like to get to

a⁻¹ * ⇑f z = a⁻¹ * (a * z) ∨ a⁻¹ * ⇑f z = a⁻¹ * (a * ⇑conj z)


When I use rw ← mul_right_inj' H3 where (H3 : a⁻¹ ≠ 0), I'm able to get

a⁻¹ * ⇑f z = 1 * z ∨ ⇑f z = a * ⇑conj z


and then I try to use rw ← mul_right_inj' H3 @(f z) @(a * conj z) to act on the other equality
but I get the error

function expected at
mul_right_inj' H3
term has type
a⁻¹ * ?m_1 = a⁻¹ * ?m_2 ↔ ?m_1 = ?m_2


#### François Sunatori (Mar 23 2021 at 00:08):

I was trying to use the @ to pass the parameters to implicit arguments {b c}

#### Scott Morrison (Mar 23 2021 at 00:14):

The @ has to go on the mul_right_inj'

#### Scott Morrison (Mar 23 2021 at 00:15):

You can also use conv in this situation to "zoom in" on the subexpression you want to rewrite. The proof is sometimes easier to follow this way.

#### François Sunatori (Mar 23 2021 at 00:21):

Thanks for the tips @Scott Morrison , how would I use conv? Would I use it with rw or on its own?

#### Scott Morrison (Mar 23 2021 at 00:21):

Something like conv at h { congr, skip, rw p }.

#### Scott Morrison (Mar 23 2021 at 00:22):

This says: "look at h, split into subexpressions, skip over the first one, rewrite using p in the second one".

#### François Sunatori (Mar 23 2021 at 00:26):

nice, I just tried it.. yup it's much easier to follow like this! Thanks for the new tool!

#### François Sunatori (Mar 24 2021 at 00:45):

I'm trying to use

apply (mul_left_cancel 2 (h z).re z.re) H_left


and am getting the error:

invalid pre-numeral, universe level must be > 0


when I did my first pass on the proof, I wrote this lemma

lemma reals_mul_left_cancel (a b c : ℝ) : a * b = a * c → b = c := sorry


and applied it like this

apply (mul_left_cancel 2 (h z).re z.re) H_left


so that I could move on.
But now I'm cleaning up the proof and would like to know what the error invalid pre-numeral, universe level must be > 0 means and how I can solve it.
Thanks!

#### Yakov Pechersky (Mar 24 2021 at 01:09):

Can you share the full lemma statement and attempted proof?

#### François Sunatori (Mar 24 2021 at 01:13):

it's for this lemma in particular (it's rather long and I'm working on making it shorter but here's the part I'm having an issue with):

import analysis.complex.basic
import data.complex.exponential
import data.real.sqrt
import analysis.normed_space.linear_isometry

open complex

local notation | x | := complex.abs x

lemma linear_isometry_complex' (z : ℂ) (h : ℂ →ₗᵢ[ℝ] ℂ) :
h 0 = 0 → h 1 = 1 → ((h z = z) ∨ (h z = conj z))
begin
...
have Hre : (h z).re = z.re := by {
rw ext_iff at H,
iterate 2 { rw add_re at H },
iterate 2 { rw add_im at H },
iterate 2 { rw conj_re at H },
iterate 2 { rw conj_im at H },
iterate 2 { rw add_neg_self at H },
iterate 2 { rw add_self_eq at H },
cases H,
rw eq_comm at H_left,
ring at H_left,
apply (reals_mul_left_cancel 2 (h z).re z.re) H_left,   <-------
},
...
end


#### Yakov Pechersky (Mar 24 2021 at 01:20):

what's H here? just the statement

#### François Sunatori (Mar 24 2021 at 01:24):

oh sorry, yes it's

H : z + ⇑conj z = ⇑h z + ⇑conj (⇑h z)


#### Yakov Pechersky (Mar 24 2021 at 01:34):

This works for me, so something is different than what you shared:

import data.buffer.parser.basic
import analysis.complex.basic
import data.complex.exponential
import data.real.sqrt
import analysis.normed_space.linear_isometry

open complex

lemma reals_mul_left_cancel (a b c : ℝ) : a * b = a * c → b = c := sorry

example (z : ℂ) (h : ℂ →ₗ[ℝ] ℂ) (h0 : h 0 = 0) (h1 : h 1 = 1) (H : z + z.conj = h z + (h z).conj) :
(h z).re = z.re :=
begin
rw ext_iff at H,
iterate 2 { rw add_re at H },
iterate 2 { rw add_im at H },
iterate 2 { rw conj_re at H },
iterate 2 { rw conj_im at H },
iterate 2 { rw add_neg_self at H },
rw ←two_mul at H,
rw ←two_mul at H,
cases H,
rw eq_comm at H_left,
ring_nf at H_left,
apply (reals_mul_left_cancel 2 (h z).re z.re) H_left,
end


#### François Sunatori (Mar 24 2021 at 01:44):

yes it works but I would like to get rid of

lemma reals_mul_left_cancel (a b c : ℝ) : a * b = a * c → b = c := sorry


and use

apply (mul_left_cancel 2 (h z).re z.re) H_left


#### Eric Rodriguez (Mar 24 2021 at 02:03):

The reason you're getting the cryptic pre-numeral error is because mul_left_cancel has the arguments implicit so you're feeding it numbers when it expects something completely different; you'll see the same error if you change your lemma to use {a b c : ℝ}. You could just linarith [H_left] to get around it if you don't like using that lemma, or maybe people that know a lot more than me know how to give Lean more hints so that it would understand, say, apply mul_left_cancel H_left.

#### François Sunatori (Mar 24 2021 at 02:09):

Oh great, thanks @Eric Rodriguez ! I'll stick to linarith [H_left]. I haven't used much automation in my proofs yet. Does the [H_left]mean: try linarith lemmas with H_left as a parameter?

#### Eric Rodriguez (Mar 24 2021 at 02:10):

as far as I understand! I'm still learning so I'm sure the wiser ones will know far better :b

#### François Sunatori (Mar 27 2021 at 17:39):

I'm working on readying this lemma for a PR. I'm wondering:

• in which file it should be or should it be in its own file (e.g. analysis/complex/isometry.lean)?
• I have another lemma that I used in the proof of linear_isometry_complex for now it's called linear_isometry_complex'. How should I name it?
• I'll try to go through the documentation style (https://leanprover-community.github.io/contribute/doc.html) and rename some variables and if it will be in its own file I guess I'll need to add a file header.
• anything else I should know about the process?

thanks!

#### Johan Commelin (Mar 27 2021 at 17:40):

François Sunatori said:

• I have another lemma that I used in the proof of linear_isometry_complex for now it's called linear_isometry_complex'. How should I name it?

That depends a lot on the statement

#### Johan Commelin (Mar 27 2021 at 17:40):

If it is reusable, it should be moved to the file where it belongs, and follow the naming convention

#### Johan Commelin (Mar 27 2021 at 17:40):

If it's really a one-off helper lemma, we typically append _aux or something like that.

#### François Sunatori (Mar 27 2021 at 17:43):

I think it's more of a one-off helper lemma in this case so I'll add _aux

#### François Sunatori (Mar 27 2021 at 17:47):

How about the linear_isometry_complex lemma itself? in which file would it make most sense to add it?

ok, thanks :)

#### François Sunatori (Mar 28 2021 at 01:01):

I think I would be ready to open a PR for this addition. This is a first for me and I look forward to getting some feedback. I would like to have write access for a non-master branch. My GitHub username is frankymacster. Thanks!

@maintainers

#### Scott Morrison (Mar 28 2021 at 09:24):

@François Sunatori, invitation sent! (Sorry, everyone must be enjoying their weekend, usually we're fast on these. :-)

#### François Sunatori (Mar 28 2021 at 14:20):

Thanks! No worries, I expected that since I asked on a Saturday night ;)

#### François Sunatori (Mar 29 2021 at 03:53):

Hi, I'm trying to use conv on the following expression

(∀ (z : ℂ), a⁻¹ * ⇑f z = z) ∨ ∀ (z : ℂ), a⁻¹ * ⇑f z = ⇑conj z


by doing:

        conv {
congr,
intro z    <--------
},


but intro z gives the error

unknown identifier 'z'


How come I can't use intro in conv? Is there some other way to deal with a situation like

(∀ (z : ℂ), a⁻¹ * ⇑f z = z) ∨ ∀ (z : ℂ), a⁻¹ * ⇑f z = ⇑conj z


to affect change to a⁻¹ * ⇑f z = z for example?
Thanks!

#### Bryan Gin-ge Chen (Mar 29 2021 at 03:55):

Use funext to rewrite under binders in conv. See the docs.

#### François Sunatori (Mar 29 2021 at 04:03):

Thanks! I tried replacing intro z with funext

       conv {
congr,
funext
},


but the goal didn't change... the goal is

∀ (z : ℂ), ⇑f z = a * z


before and after funext

#### Bryan Gin-ge Chen (Mar 29 2021 at 04:09):

Ah, I guess funext only works on lambdas. Maybe you can try to get inside using find?

#### Alex J. Best (Mar 29 2021 at 04:12):

conv in .. should work?
e.g.

import tactic
lemma a (a b : ℕ) : (∀ (c : ℕ), a * b = c) ∨ ∀ (c : ℕ), a = b * c :=
begin
conv in (_ = _) {
}
end


PS it'll be easier to help if you can make a #mwe like I did here for people to try their suggestions

#### François Sunatori (Mar 29 2021 at 04:16):

great, both find (f _ = _) and conv in (_ = _) worked! (I think I'll opt for conv in (_ = _) since it gave less lines). Thanks to you both :)

#### Heather Macbeth (Mar 29 2021 at 04:17):

Alex J. Best said:

PS it'll be easier to help if you can make a #mwe like I did here for people to try their suggestions

One nice thing about a #mwe is that anyone can open it instantly in the web editor (using the tool in the top right corner of the code snippet) to play with it.

#### François Sunatori (Mar 29 2021 at 04:21):

Oh I didn't know that it opened the web editor! ok I'll try to do that next time, I guess it will make communicating things easier!

#### François Sunatori (Mar 31 2021 at 01:56):

I'm trying to generalize the expression (f z).re = z.re to ∀ (z : ℂ), (f z).re = z.re like so:

import analysis.complex.basic

open complex

lemma add_self_eq (a : ℝ) : a + a = a * 2 := by ring

lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) : ∀ (z : ℂ), (f z).re = z.re := by {
conv at h₃ {
find (_ = _) {
rw ext_iff,
rw conj_re, rw conj_re,
rw conj_im, rw conj_im,
congr,
skip,
-- refl,
-- trivial,
},
},
sorry,
}


I tried to use refl and trivial inside conv at h3 (and thought that it would work since I saw it used in https://leanprover-community.github.io/extras/conv.html) but am getting this error:

type mismatch at application
conv.istep 19 6 19 6 refl
term
refl
has type
∀ (a : ?m_1), ?m_2 a a : Prop
but is expected to have type
conv ?m_1 : Type


am I missing something here? or should I be trying a different tactic?
Thanks!

#### Yakov Pechersky (Mar 31 2021 at 02:16):

One way to generalize it is just to say:

lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) (z : ℂ) : (f z).re = z.re :=
begin
(show (2 : ℝ) ≠ 0, by simp [two_ne_zero'])] using (h₃ z).symm
end


#### François Sunatori (Mar 31 2021 at 02:23):

oh nice, however an extra detail is that (∀ z : ℂ) : (f z).re = z.re is a hypothesis in the lemma I'm working on. Will this work in that case?

#### Yakov Pechersky (Mar 31 2021 at 02:25):

I'm not sure what you mean. All I did was move the ∀ (z : ℂ) to the left of the colon in  lemma name args *here* : statement := proof

#### Yakov Pechersky (Mar 31 2021 at 02:25):

And you'll be able to use it. Take a look:

#### Yakov Pechersky (Mar 31 2021 at 02:26):

import analysis.complex.basic

open complex

lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) (z : ℂ) : (f z).re = z.re :=
begin
(show (2 : ℝ) ≠ 0, by simp [two_ne_zero'])] using (h₃ z).symm
end

#check hf_re
/-
hf_re :
∀ (f : ℂ →ₗᵢ[ℝ] ℂ),
(∀ (z : ℂ), z + ⇑conj z = ⇑f z + ⇑conj (⇑f z)) → ∀ (z : ℂ), (⇑f z).re = z.re
-/


#### Yakov Pechersky (Mar 31 2021 at 02:26):

As you can see, I placed the z to the left of the colon, and the lemma, as Lean sees it, still has the universal quantifier.

#### François Sunatori (Mar 31 2021 at 02:30):

ok thanks :) I'll see how I can use it in my lemma!

#### Greg Price (Mar 31 2021 at 02:57):

François Sunatori said:

I tried to use refl and trivial inside conv at h3 (and thought that it would work since I saw it used in https://leanprover-community.github.io/extras/conv.html)

Once arrived at the relevant target, we can use rw as in normal mode. Note that Lean tries to solves the current goal if it became x = x (in the strict syntactical sense, definitional equality is not enough: one needs to conclude by refl or trivial in this case).

It sounds like it's saying you can use refl or trivial inside the conv block, but I think what it actually means is just that in that case you need to say refl or trivial after the conv is over.

#### Greg Price (Mar 31 2021 at 03:02):

Putting the z : ℂ before the colon is a good way to write the proof, but perhaps it's informative to see another way you could more directly do what you were trying to do above:

lemma hf_re (f : ℂ →ₗᵢ[ℝ] ℂ) (h₃ : ∀ z, z + conj z = f z + conj (f z)) : ∀ (z : ℂ), (f z).re = z.re := by {
intro z,
have h₄, from h₃ z,
/-
f : ℂ →ₗᵢ[ℝ] ℂ,
h₃ : ∀ (z : ℂ), z + ⇑conj z = ⇑f z + ⇑conj (⇑f z),
z : ℂ,
h₄ : z + ⇑conj z = ⇑f z + ⇑conj (⇑f z)
⊢ (⇑f z).re = z.re
-/
sorry,
}


#### François Sunatori (Mar 31 2021 at 03:21):

oh right, I haven't thought of doing that! thanks for the trick :)

#### François Sunatori (Mar 31 2021 at 03:24):

Greg Price said:

Putting the z : ℂ before the colon is a good way to write the proof

Is there a preferred style for mathlib in terms of having

• z : ℂ before the colon vs
• ∀ (z : ℂ) after the colon
?

#### Heather Macbeth (Mar 31 2021 at 03:26):

Yes, the former! It avoids one intros step.

#### Heather Macbeth (Mar 31 2021 at 03:27):

And I might guess (not sure, though) that it's less sensitive to ordering of hypotheses in things like library_search.

#### François Sunatori (Mar 31 2021 at 03:34):

thanks! I'll work on cleaning up my code to follow that more and maybe also split some parts out as smaller lemmas (I get the feeling my proofs were too long when I compare with other ones in mathlib)

#### François Sunatori (Mar 31 2021 at 03:36):

Is there some rule of thumb or a style preference on when a code block should stay in a have inside a proof vs when it should be moved out?

#### Yury G. Kudryashov (Mar 31 2021 at 03:37):

#mwe? What are the two options (it's OK to use foo instead of a real example)?

#### François Sunatori (Mar 31 2021 at 03:49):

actually I was asking more as a general question if there's a general way or heuristic to determine when a proof should be split into smaller lemmas (for one I'm guessing if it can be reused elsewhere it's a good idea to move it out as its own lemma, but would there be other reasons?), but here's how I had it:
the "main" lemma to prove

lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z))


an auxiliary lemma that I'm using in the proof of the one above

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) :
f 0 = 0 → f 1 = 1 → ((∀ z, f z = z) ∨ (∀ z, f z = conj z))


but the proof I had for linear_isometry_complex_aux is almost 100 lines.. (maybe I didn't use the shortest path to get to it or I haven't used enough simplification tactics) but I'm asking because I'm guessing that at some point too many lines may not be preferable in the mathlib library.

#### Yury G. Kudryashov (Mar 31 2021 at 03:52):

In this case it looks like the aux lemma is an important particular case, and it can be used separately, so it should be a separate lemma.

#### Yury G. Kudryashov (Mar 31 2021 at 03:53):

"To split or not to split" is a matter of taste. I'm not sure what's more readable: a long proof with many named haves or a series of short lemmas.

#### Yury G. Kudryashov (Mar 31 2021 at 03:54):

Sure, if one of haves is a useful lemma, then it should be formulated separately. Otherwise it's OK to have long proofs.

#### Yakov Pechersky (Mar 31 2021 at 03:55):

The proof for the aux lemma, in my mind, is something like

show that the real parts must match up (you've done this, 2 lines)
show that I maps to either I or -I
every z is a linear combination of a + b * I, so  the properties you've proved so far transfer


#### Yakov Pechersky (Mar 31 2021 at 03:55):

And the first two can be their own lemmas, I think (?)

#### François Sunatori (Mar 31 2021 at 03:56):

ok yea I like that split. I'll try it that way

#### François Sunatori (Mar 31 2021 at 03:56):

thanks @Yury G. Kudryashov and @Yakov Pechersky !

#### Yakov Pechersky (Mar 31 2021 at 03:57):

Haven't done complex analysis in a long time, so my assumptions about what's easy or what implies what might be wrong here.

#### François Sunatori (Mar 31 2021 at 04:18):

so actually the way I had it for the linear_isometry_complex_aux (at a high level) was this way:

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0 : ∀ z, |f z| = |z| := sorry,
have hf1 : ∀ z, |f z - f 1| = |z - 1| := sorry,
have h : ∀ z, conj (f z - 1) * (f z - 1) = conj (z - 1) * (z - 1) := sorry,
have h₃ : ∀ z, z + conj z = f z + conj (f z) := sorry,
have hf_re : ∀ z, (f z).re = z.re := sorry,
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
...
}


since the last 2 (hf_re and hf_im) are rather general I think I'll move them to their own lemmas and maybe the other cases would stay in the proof. I don't know how conventional it is to split a proof up this way in terms of the haves but it felt easier to follow for me when I did the original write up.

#### Heather Macbeth (Mar 31 2021 at 04:21):

To tweak the statement a little further, how about

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₁ : f 1 = 1) :
f = linear_isometry.id ∨ f = conj_li


You don't need h₀, it's true automatically.

#### François Sunatori (Mar 31 2021 at 04:24):

ok sure! it looks more concise!

#### Heather Macbeth (Mar 31 2021 at 04:30):

Yakov Pechersky said:

The proof for the aux lemma, in my mind, is something like

show that the real parts must match up (you've done this, 2 lines)
show that I maps to either I or -I
every z is a linear combination of a + b * I, so  the properties you've proved so far transfer


I noticed a lemma that might help carrying out Yakov's idea: docs#is_basis.ext

#### Heather Macbeth (Mar 31 2021 at 04:31):

applied to docs#complex.is_basis_one_I

#### Yakov Pechersky (Mar 31 2021 at 04:32):

With a fin_cases somewhere in there

#### Scott Morrison (Mar 31 2021 at 06:11):

Heather Macbeth said:

And I might guess (not sure, though) that it's less sensitive to ordering of hypotheses in things like library_search.

library_search (and indeed many tactics) can't tell the difference between arguments before vs after the colon.

#### François Sunatori (Apr 03 2021 at 14:21):

Hi, I'm continuing on the following lemma:

import analysis.complex.basic
import data.complex.exponential
import data.real.sqrt
import analysis.normed_space.linear_isometry

open complex

local notation | x | := complex.abs x

lemma hf_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h₁ :  ∀ z, |f z| = |z|) (h₂ : ∀ z, (f z).re = z.re) (z : ℂ) :
(f z).im = z.im ∨ (f z).im = -z.im := by {
conv at h₁ {
find (_ = _) {
simp [complex.abs],
rw [real.sqrt_inj, norm_sq_apply (f z), norm_sq_apply z, h₂, add_left_cancel_iff,
mul_self_eq_mul_self_iff],
-- exact norm_sq_nonneg (f z),
},
},
}


When I apply rw real.sqrt_inj, 2 more subgoals appear and I'm not sure within a conv how I can do a swap.
Is it doable? or do I need to go at this a different way?
Thanks!
(I'm using conv at h₁ because of the  ∀ z)

#### Kevin Buzzard (Apr 03 2021 at 14:58):

Maybe this is easier?

lemma hf_im {f : ℂ →ₗᵢ[ℝ] ℂ} (h₁ :  ∀ z, |f z| = |z|) (h₂ : ∀ z, (f z).re = z.re) (z : ℂ) :
(f z).im = z.im ∨ (f z).im = -z.im :=
begin
specialize h₁ z,
simp [complex.abs] at h₁,
rw [real.sqrt_inj, norm_sq_apply (f z), norm_sq_apply z, h₂, add_left_cancel_iff,
mul_self_eq_mul_self_iff] at h₁,
...


#### François Sunatori (Apr 03 2021 at 15:07):

I hadn't used specialize yet. Thanks! it's much easier this way :)

#### François Sunatori (Apr 04 2021 at 02:54):

Hi, I managed to write up the proofs for all the haves here:

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0 : ∀ z, |f z| = |z| := sorry,
have hf1 : ∀ z, |f z - f 1| = |z - 1| := sorry,
have h : ∀ z, conj (f z - 1) * (f z - 1) = conj (z - 1) * (z - 1) := sorry,
have h₃ : ∀ z, z + conj z = f z + conj (f z) := sorry,
have hf_re : ∀ z, (f z).re = z.re := sorry,
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
sorry
}


what is left is the last sorry.

I'm trying to get (∀ z, f z = z) ∨ (∀ z, f z = conj z) from hf_re and hf_im.

After doing

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0' : ∀ z, |f z| = |z| := sorry,
have hf1' : ∀ z, |f z - 1| = |z - 1| := sorry,
have h₃' : ∀ z, f z + conj (f z) = z + conj z := sorry,
have hf_re' : ∀ z, (f z).re = z.re := sorry,
have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
conv {
congr,
find (_ = _) {
rw ext_iff,
},
},
conv {
congr,
skip,
find (_ = _) {
rw ext_iff,
rw conj_re,
rw conj_im,
},
},


I end up with

(∀ (z : ℂ), (⇑f z).re = z.re ∧ (⇑f z).im = z.im) ∨ ∀ (z : ℂ), (⇑f z).re = z.re ∧ (⇑f z).im = -z.im


I tried a few things but wasn't able to get to

(∀ (z : ℂ), (⇑f z).re = z.re) ∧ (∀ (z : ℂ), (⇑f z).im = z.im ∨ (⇑f z).im = -z.im)


the closest I got was

(∀ (x : ℂ), (⇑f x).re = x.re) ∧ ∀ (x : ℂ), (∀ (x : ℂ), (⇑f x).im = x.im) ∨ (⇑f x).im = -x.im


but I still have a ∀ (x : ℂ) too many (it's redundant but I don't know how to get rid of it).. Is there a way to simplify this expression to

(∀ (z : ℂ), (⇑f z).re = z.re) ∧ (∀ (z : ℂ), (⇑f z).im = z.im ∨ (⇑f z).im = -z.im)


or am I taking a difficult path?
Thanks!

#### Heather Macbeth (Apr 04 2021 at 05:25):

It is worthwhile to try to carry through your own method, and probably someone will be able to help you with the details ... but I wanted to check that you also saw the advice from me and Yakov Pechersky above,
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear_isometry_complex/near/232534975
about a different method using docs#is_basis.ext.

#### Damiano Testa (Apr 04 2021 at 05:32):

I am on mobile, so I may be misunderstanding the issue, but you could try and_distrib (or something similar) to split/unsplit and-or statements.

#### François Sunatori (Apr 04 2021 at 05:44):

@Heather Macbeth thanks, yes I had seen your and Yakov Pechersky's advice but I wasn't sure yet how to approach it that way so I wanted to try a first go at it with the tools that I already know and then on a second pass maybe try that advice. But maybe if it turns out that the path I'm taking is giving me too much trouble I might jump directly to trying docs#is_basis.ext.

#### Damiano Testa (Apr 04 2021 at 06:39):

Ok, this allows you to use some of your assumptions, but leaves still a tangled mess of foralls/ors!

  rw [forall_and_distrib, forall_and_distrib, ← and_or_distrib_left, ← forall_or_distrib_left],
refine ⟨hf_re', _⟩,


#### Damiano Testa (Apr 04 2021 at 06:39):

I am actually not even sure if what you want to prove is true...

#### Greg Price (Apr 04 2021 at 08:25):

I think this might take you in a helpful direction:

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
specialize hf_im I,
cases hf_im,
{
left,
-- f: ℂ →ₗᵢ[ℝ] ℂ
-- h: ⇑f 1 = 1
-- hf_I : (⇑f I).im = I.im
-- ⊢ ∀ (z : ℂ), ⇑f z = z
sorry
},
{
right,
-- ...
-- hf_I : (⇑f I).im = -I.im
-- ⊢ ∀ (z : ℂ), ⇑f z = ⇑conj z
sorry
},
}


#### François Sunatori (Apr 04 2021 at 15:56):

@Greg Price the problem I get with using specialize hf_im I is that I still need to prove

∀ (z : ℂ), ⇑f z = ⇑conj z


but now the hypothesis I would like to use (∀ z, (f z).im = z.im ∨ (f z).im) is specialized at I.

#### Kevin Buzzard (Apr 04 2021 at 16:04):

then you can do have hf_im_I := hf_im I, or just cases hf_im I

#### François Sunatori (Apr 08 2021 at 02:14):

My proof was getting more and more complicated to follow, so I'm starting to look into the docs#is_basis.ext direction.
I'm not sure how to start though...

I'm guessing that

• I'll want to use is_basis.ext with is_basis_one_I as one of its arguments.
• I need to supply 2 linear maps in order to show with is_basis.ext that they correspond everywhere, so I would use f as one of the linear maps and the other would be the identity map in once case and the conj map in the other?

or will I be using one of these as the last argument to is_basis.ext

have hf_re' : ∀ z, (f z).re = z.re := sorry
have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry


?

Also I'm unsure how I'll be using fin_cases.. maybe the path will be clearer to me once I know how to call is_basis.ext..

Thanks again for all the help!

#### Heather Macbeth (Apr 08 2021 at 02:56):

François Sunatori said:

I'm guessing that

• I'll want to use is_basis.ext with is_basis_one_I as one of its arguments.
• I need to supply 2 linear maps in order to show with is_basis.ext that they correspond everywhere, so I would use f as one of the linear maps and the other would be the identity map in once case and the conj map in the other?

This sounds good!

#### Heather Macbeth (Apr 08 2021 at 02:57):

François Sunatori said:

or will I be using one of these as the last argument to is_basis.ext

have hf_re' : ∀ z, (f z).re = z.re := sorry
have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry


I don't think you should have to consider real and imaginary parts separately. But feel free to show us the setup if this seems to be forced on you.

#### François Sunatori (Apr 08 2021 at 03:10):

ok thanks for helping point the way..
so I'll try using is_basis.ext is_basis_one_I <a proposition involving f and id>

<a proposition involving f and id> needs to be of type (h : ∀i, f (v i) = g (v i)) where i : ι and ι : Type*
is the i used to parametrize the dimension of the vector space having v as an element?

#### François Sunatori (Apr 17 2021 at 02:52):

I'm still unsure how to move forward at this point...

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0 : ∀ z, |f z| = |z| := sorry,
have hf1 : ∀ z, |f z - f 1| = |z - 1| := sorry,
have h : ∀ z, conj (f z - 1) * (f z - 1) = conj (z - 1) * (z - 1) := sorry,
have h₃ : ∀ z, z + conj z = f z + conj (f z) := sorry,
have hf_re : ∀ z, (f z).re = z.re := sorry,
have hf_im : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := sorry,
sorry
}


(all but the last sorry have been proven)

I haven't found how to apply is_basis.ext and is_basis_one_I here.
it looks like Lean expects the next argument to be of type ∀ (i : fin 1.succ), ⇑?m_4 (![1, I] i) = ⇑?m_5 (![1, I] i)

I have a few questions here:

• what does ! mean?
• what is the i of type fin 1.succ?
• def fin (n : ℕ) := {i : ℕ // i < n} so it's a natural number that is smaller than 1.succ?
Where can I get this number from my current setup?

Thanks

#### François Sunatori (Apr 17 2021 at 03:00):

Ok actually for !
I found "The notation ![a, b, ...] expands to vec_cons a (vec_cons b ...)"
so I'm guessing ![1, I] is just the way that Lean represents vectors.

#### François Sunatori (Apr 17 2021 at 03:52):

ok so my understanding is that i is the index of the length of the vector ![1, I] which in this case is 1.succ

#### François Sunatori (Apr 17 2021 at 04:12):

I tried as a test to add hypothesis h4 (that would have the expected type for the 2nd argument of is_basis.ext

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) :
(∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
have hf0' : ∀ z, |f z| = |z| := hf0,
have hf1' : ∀ z, |f z - 1| = |z - 1| := hf1 h,
have h₃' : ∀ z, f z + conj (f z) = z + conj z := h₃ hf1',
have hf_re' : ∀ z, (f z).re = z.re := hf_re h₃',
have hf_im' : ∀ z, (f z).im = z.im ∨ (f z).im = -z.im := hf_im hf0 hf_re',
have h2 : ∀ z, f z = z := sorry,
have h3 : ∀ z, f z = conj z := sorry,
have h4 : ∀ (i : fin 1.succ), f (![1, I] i) = id (![1, I] i) := sorry,
exact is_basis.ext is_basis_one_I h4,


However I get the error

invalid field notation, type is not of the form (C ...) where C is a constant
1
has type
?m_1


when mousing over 1.succ.
it seems to me that fin n is a dependent type depending on a natural number.
when I change it to 2 I don't get the error anymore, but I now get

type mismatch at application
is_basis_one_I.ext h4
term
h4
has type
∀ (i : fin 2), ⇑f (![1, I] i) = id (![1, I] i)
but is expected to have type
∀ (i : fin 1.succ), ⇑?m_4 (![1, I] i) = ⇑?m_5 (![1, I] i)


How can I get ∀ (i : fin 1.succ), ⇑f (![1, I] i) = id (![1, I] i) to work here?

#### Johan Commelin (Apr 17 2021 at 05:26):

@François Sunatori Right ![a,b,c,x,y,z] is just notation for the vector (a,b,c,x,y,z) in 6-dim space.
And i : fin 1.succ means some term of type fin 1.succ where 1.succ : nat is just 2. So i = 0 or i = 1.
In total ![1, I] i means the ith component of the vector (1,I). So this is 1 if i = 0 and I if i = 1.

#### Ruben Van de Velde (Apr 17 2021 at 09:20):

Unpolished but sorry-free:

#### François Sunatori (Apr 17 2021 at 10:17):

@Ruben Van de Velde oh that's quite a bit more than what I was asking for, but maybe I can go over it and try to learn from it and I may ask a few questions about some sections just so that I can learn and compare with what I had. Thanks

#### François Sunatori (Apr 18 2021 at 17:46):

I'm now working on changing the initial statement to

lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li


I defined rotation like so

import analysis.complex.basic
import data.complex.exponential
import analysis.normed_space.linear_isometry

open complex

local notation | x | := complex.abs x

def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a * z,
map_smul' := by {
intros m x,
simp,
rw ← mul_assoc a m x,
rw mul_comm a m,
exact mul_assoc ↑m a x,
},
norm_map' := by {
intro x,
simp,
rw ha,
rw one_mul,
},
}


but am getting the error

definition 'rotation' is noncomputable, it depends on 'complex.normed_field'


I'm not sure what this error means.
I thought I was not exposing normed_field and tried using open complex.normed_field but that gives the error invalid namespace name 'complex.normed_field'.
Am I missing something here?

Thanks :)

#### Hanting Zhang (Apr 18 2021 at 17:50):

Add noncomputable def ... to the beginning

#### François Sunatori (Apr 18 2021 at 17:53):

@Hanting Zhang thanks!
I just saw in https://leanprover.github.io/theorem_proving_in_lean/axioms_and_computation.html

The standard library also defines a choice principle that is entirely antithetical to a computational interpretation, since it magically produces “data” from a proposition asserting its existence. Its use is essential to some classical constructions, and users can import it when needed. But expressions that use this construction to produce data do not have computational content, and in Lean we are required to mark such definitions as noncomputable to flag that fact.

#### François Sunatori (Apr 18 2021 at 17:54):

If I understand well, I need to use noncomputable def when I use a record type to use it as data?

#### Hanting Zhang (Apr 18 2021 at 17:57):

I'm not sure what you mean by record type, but my understanding is that noncomputable means Lean can't produce bytecode for the data your working with. So you can't do #print ..., but otherwise everything else works as normal

#### Alex J. Best (Apr 18 2021 at 17:59):

It's only some types that are noncomputable, things like complex and real are some of them. If you just want to prove theorems the standard advice is to put the line noncomputable theory at the top of your file (below the imports), and lean will stop bothering you about

definition 'rotation' is noncomputable, it depends on 'complex.normed_field'


you don't really lose anything by doing this.

#### Kevin Buzzard (Apr 18 2021 at 18:46):

I remember as a beginner being really concerned/confused about what the ramifications of all this noncomputable stuff was, as I was trying to formalise random undergraduate maths from my intro to proof course, and it turned out some was computable and some was not. The thing which took a while to dawn on me was this: if you make noncomputable stuff, then #eval and #reduce might not work -- but if you just want to prove theorems you never use these things anyway, you just use theorem. So noncomputable doesn't matter at all. The majority of the perfectoid space repo was noncomputable, for example.

#### François Sunatori (Apr 18 2021 at 21:56):

I'm trying to get from

f = rotation ha ∨ f = (rotation ha).comp conj_li


to

((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z))


so that I can reuse the proof I have for

lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ a : ℂ, |a| = 1 ∧ ((∀ z, f z = a * z) ∨ (∀ z, f z = a * conj z))


This is what I have:

import analysis.complex.basic
import data.complex.exponential
import analysis.normed_space.linear_isometry

open complex

local notation | x | := complex.abs x

noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ to_fun := λ z, a * z,
map_smul' := by {
intros m x,
simp,
rw ← mul_assoc a m x,
rw mul_comm a m,
exact mul_assoc ↑m a x,
},
norm_map' := by {
intro x,
simp,
rw ha,
rw one_mul,
},
}

lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li := by {
let a := f 1,
use a,
split,
{
rw rotation,
left,
change f = λ z, a * z,
sorry,
},
{
sorry
}
}


Specifically for now, I'm trying to get from

f = rotation ha


to

∀ z, f z = a * z


I tried to use the come_on_lean tactic (to_fun := λ (z : ℂ), a * z because I want to get λ (z : ℂ), a * z "out" of rotation) to go from

f = rotation ha


to

f = λ z, a * z


but I get this error

type mismatch at application
f = λ (z : ℂ), a * z
term
λ (z : ℂ), a * z
has type
ℂ → ℂ
but is expected to have type
ℂ →ₗᵢ[ℝ] ℂ


Is there a way for me to isolate the to_fun from the rotation linear isometry in this case?

Thanks!

#### Hanting Zhang (Apr 18 2021 at 22:12):

Is this true or am I missing something? f doesn't need to be a rotation, but you are asserting that it is?

#### Eric Wieser (Apr 18 2021 at 22:16):

You want the proof that coe_fn is injective

#### Eric Wieser (Apr 18 2021 at 22:17):

Something like docs#linear_map.coe_injective, but for  →ₗᵢ[ℝ]. Edit: ah, docs#linear_isometry.coe_fn_injective

#### François Sunatori (Apr 18 2021 at 22:18):

@Hanting Zhang sorry, here I'm assuming |a| = 1 so it a = e^iθ and I'm not considering translations

#### Eric Wieser (Apr 18 2021 at 22:20):

Oh, actually just tactic#ext should do the trick

#### Hanting Zhang (Apr 18 2021 at 22:21):

Oh nevermind, I missed the little ₗᵢ subscript, sorry!

#### François Sunatori (Apr 18 2021 at 22:21):

@Eric Wieser Thanks! I'll look into docs#linear_isometry.coe_fn_injective. By the way, I've been seeing coe a lot and I think it has to do with ⇑ but I still don't really understand what it means... Could you enlighten me or point me to a doc about it? Thank you!

#### Eric Wieser (Apr 18 2021 at 22:27):

I don't know what come_on_lean refers to, but the trick is to add a helper lemma as soon as you've made the definition:

noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ norm_map' := λ z, by simp [ha],
to_linear_map := algebra.lmul ℝ ℂ a, }

@[simp] lemma rotation_apply {a : ℂ} (ha : |a| = 1) (z : ℂ) : rotation ha z = a * z := rfl


#### François Sunatori (Apr 18 2021 at 22:29):

come_on_lean refers to the comment
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/linear_isometry_complex/near/231253906

#### Eric Wieser (Apr 18 2021 at 22:29):

Then you can get back to doing maths rather than fighting lean with:

lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li :=
begin
refine ⟨f 1, _, _⟩,
{ sorry, },
{ left,
ext1,
rw rotation_apply,
sorry },
end


#### François Sunatori (Apr 18 2021 at 22:31):

Eric Wieser said:

I don't know what come_on_lean refers to, but the trick is to add a helper lemma as soon as you've made the definition:

noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ norm_map' := λ z, by simp [ha],
to_linear_map := algebra.lmul ℝ ℂ a, }

@[simp] lemma rotation_apply {a : ℂ} (ha : |a| = 1) (z : ℂ) : rotation ha z = a * z := rfl


wow that's much simpler than what I had written.. I hope I can write concisely like that at some point

#### Eric Wieser (Apr 18 2021 at 22:32):

The trick there was knowing that docs#algebra.lmul already existed

#### Eric Wieser (Apr 18 2021 at 22:32):

But all you actually needed to get out of your struggle is that rotation_apply lemma

#### Eric Wieser (Apr 18 2021 at 22:33):

When you define a bundled map some_func, you almost never want to rw some_func; you usually want to define an _apply lemma like I do there

#### François Sunatori (Apr 18 2021 at 22:34):

ok yes, I recall seeing some _apply lemmas where there was just a rfl as proof.
I'll keep in mind that I better add those when I have a def for a function inside a record

#### Eric Wieser (Apr 18 2021 at 22:35):

Sometimes its more useful to define coe_some_func instead of some_func_apply, especially if you didn't actually end up using a λ to define the function:

@[simp] lemma coe_rotation {a : ℂ} (ha : |a| = 1) :
⇑(rotation ha) = algebra.lmul ℝ ℂ a := rfl


#### François Sunatori (Apr 18 2021 at 22:45):

ok so, when I see coe_ and _apply I can assume they are used for a similar purpose? The one of getting a "field" out of a record.

#### François Sunatori (Apr 18 2021 at 22:46):

and is the ⇑ linked to coe (coercion)?

#### Eric Wieser (Apr 18 2021 at 22:47):

Strictly ⇑ is docs#coe_fn

#### Eric Wieser (Apr 18 2021 at 22:48):

↑ is docs#coe, ↥ is docs#coe_sort. Lots of lemma names are pretty lax about the difference, especially since sometimes ↑ ends up meaning one of the other arrows

#### François Sunatori (Apr 18 2021 at 22:49):

ah ok, great! thanks.. it's getting clearer to me :)

#### François Sunatori (Apr 19 2021 at 01:05):

I managed to get a little further by adding conj_li_apply:

import analysis.complex.basic
import data.complex.exponential
import analysis.normed_space.linear_isometry

noncomputable theory

open complex

local notation | x | := complex.abs x

noncomputable def rotation {a : ℂ} (ha : |a| = 1) : ℂ →ₗᵢ[ℝ] ℂ :=
{ norm_map' := λ z, by simp [ha],
to_linear_map := algebra.lmul ℝ ℂ a, }

@[simp] lemma rotation_apply {a : ℂ} (ha : |a| = 1) (z : ℂ) : rotation ha z = a * z := rfl

lemma linear_isometry_complex (f : ℂ →ₗᵢ[ℝ] ℂ) :
∃ (a : ℂ) (ha : |a| = 1), f = rotation ha ∨ f = (rotation ha).comp conj_li :=
begin
let a := f 1,
refine ⟨a, _, _⟩,
{
change ∥a∥ = 1,
simp only [a],
rw linear_isometry.norm_map,
simp,
},
{
conv {
congr,
},

-- left,
-- ext1 z,
-- rw rotation_apply,

-- right,
-- ext1 z,
-- norm_num,
},
end


Now I need to use conv followed by congr to change the 2 sides of the ∨ in f = rotation _ ∨ f = (rotation _).comp conj_li.
I would like to apply the commented out sections to the 2 sides of the ∨, but I don't know how to use ext1 in conversion tactic mode. What should I be using once in conv?

Thanks!

#### François Sunatori (Apr 19 2021 at 01:33):

I looked for all instances of conv in mathlib but haven't seen an example of an ext being used in a conv block.. and I couldn't find something doing the equivalent of an ext either..
Is it possible that it can't be used in a conv block and that I should approach this from a different direction?

#### Alex J. Best (Apr 19 2021 at 01:49):

Does funext work in this context?

#### Eric Rodriguez (Apr 19 2021 at 01:50):

ext wouldn't work in conv i don't think, as presumably it'd have to write it as (∀ z, <stuff> ∨ ∀ z, <stuff> whilst ext immediately intros. not sure how feasible it is but maybe just do the work in some haves and then rw

#### Eric Rodriguez (Apr 19 2021 at 01:50):

just tried it alex, it basically seems to be a noop

#### François Sunatori (Apr 19 2021 at 01:58):

right, no funext didn't work.. I'll try with some haves then. Thanks!

#### Eric Wieser (Apr 19 2021 at 07:36):

Ideally at this point you'd use the maths proof to decide whether the left or right of the or is true

Last updated: May 19 2021 at 02:10 UTC