linear_isometry_complex

Stream: maths

[François Sunatori]

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]

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]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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]

thanks for the tips :)

[François Sunatori]

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

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

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

[Kevin Buzzard]

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]

Bubbing should send a linear map to a linear map

[Heather Macbeth]

@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]

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]

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]

So, in your constructor, you'll have

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

[François Sunatori]

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]

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

[Kevin Buzzard]

@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]

@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]

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,
      map_add' := by {
        intros x y,
        rw linear_isometry.map_add,
        rw mul_add,
      },
      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]

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]

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]

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]

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

[Heather Macbeth]

Thus,

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

[Heather Macbeth]

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]

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]

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]

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]

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]

have is for proofs, let is for data.

[François Sunatori]

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]

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

[François Sunatori]

no...

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

gives

simplify tactic failed to simplify

[Heather Macbeth]

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

[François Sunatori]

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]

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]

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]

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

[François Sunatori]

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

[François Sunatori]

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?

[Heather Macbeth]

Seems plausible!

[François Sunatori]

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]

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]

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]

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

[Heather Macbeth]

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]

(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]

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]

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]

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

[Heather Macbeth]

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

[Heather Macbeth]

Because 0 is not invertible.

[François Sunatori]

oh right! oups

[Heather Macbeth]

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

[François Sunatori]

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

[François Sunatori]

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]

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

[Scott Morrison]

The @ has to go on the mul_right_inj'

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[François Sunatori]

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

[François Sunatori]

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]

Can you share the full lemma statement and attempted proof?

[François Sunatori]

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]

what's H here? just the statement

[François Sunatori]

oh sorry, yes it's

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

[Yakov Pechersky]

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]

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

instead

[Eric Rodriguez]

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]

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]

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

[François Sunatori]

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]

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]

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

[Johan Commelin]

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

[François Sunatori]

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

[François Sunatori]

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

[Johan Commelin]

your suggestion sounded good

[François Sunatori]

ok, thanks :)

[François Sunatori]

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!

[Kevin Buzzard]

@maintainers

[Scott Morrison]

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

[François Sunatori]

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

[François Sunatori]

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]

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

[François Sunatori]

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]

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

[Alex J. Best]

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]

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]

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]

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]

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 add_re, rw add_re,
      rw add_im, rw add_im,
      rw conj_re, rw conj_re,
      rw conj_im, rw conj_im,
      rw add_neg_self, rw add_neg_self,
      rw add_self_eq, rw add_self_eq,
      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]

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
  simpa [ext_iff, add_re, add_im, conj_re, conj_im, ←two_mul,
         (show (2 : ℝ) ≠ 0, by simp [two_ne_zero'])] using (h₃ z).symm
end

[François Sunatori]

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]

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]

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

[Yakov Pechersky]

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
  simpa [ext_iff, add_re, add_im, conj_re, conj_im, ←two_mul,
         (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]

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]

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

[Greg Price]

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)

I think the docs may be unclear about this. That page says (modulo formatting):

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]

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]

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

[François Sunatori]

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]

Yes, the former! It avoids one intros step.

[Heather Macbeth]

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

[François Sunatori]

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]

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]

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

[François Sunatori]

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]

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]

"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]

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]

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]

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

[François Sunatori]

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

[François Sunatori]

thanks @Yury G. Kudryashov and @Yakov Pechersky !

[Yakov Pechersky]

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]

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]

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]

ok sure! it looks more concise!

[Heather Macbeth]

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]

applied to docs#complex.is_basis_one_I

[Yakov Pechersky]

With a fin_cases somewhere in there

[Scott Morrison]

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]

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]

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]

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

[François Sunatori]

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]

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]

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]

@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]

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]

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

[Greg Price]

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]

@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]

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

[François Sunatori]

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]

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]

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]

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]

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]

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]

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]

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]

@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]

Unpolished but sorry-free:

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

@[simp]
lemma linear_isometry.id_apply (z : ℂ) : (linear_isometry.id : ℂ →ₗᵢ[ℝ] ℂ) z = z := rfl

@[simp]
lemma linear_isometry.id_to_linear_map : (linear_isometry.id.to_linear_map : ℂ →ₗ[ℝ] ℂ) = linear_map.id := rfl

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

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₁,
  rwa [real.sqrt_inj (norm_sq_nonneg _) (norm_sq_nonneg _), norm_sq_apply (f z), norm_sq_apply z,
    h₂, add_left_cancel_iff, mul_self_eq_mul_self_iff] at h₁,
end

lemma linear_isometry.l0 {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : ∥f z - 1∥ = ∥z - 1∥ := begin
  rw ←linear_isometry.norm_map f (z - 1),
  rw linear_isometry.map_sub,
  rw h,
end

lemma linear_isometry.l1 {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : z + conj z = f z + conj (f z) :=
begin
  have := linear_isometry.l0 h z,
  apply_fun λ x, x ^ 2 at this,
  simp only [norm_eq_abs, ←norm_sq_eq_abs] at this,
  rw [←of_real_inj, ←mul_conj, ←mul_conj] at this,
  rw [conj.map_sub, conj.map_sub] at this,
  simp only [sub_mul, mul_sub, one_mul, mul_one] at this,
  rw [mul_conj, norm_sq_eq_abs, ←norm_eq_abs, linear_isometry.norm_map] at this,
  rw [mul_conj, norm_sq_eq_abs, ←norm_eq_abs] at this,
  simp only [sub_sub, sub_right_inj, mul_one, of_real_pow, ring_hom.map_one, norm_eq_abs] at this,
  simp only [add_sub, sub_left_inj] at this,
  rw [add_comm, ←this, add_comm],
end
lemma linear_isometry.re {f : ℂ →ₗᵢ[ℝ] ℂ} (h : f 1 = 1) (z : ℂ) : (f z).re = z.re := begin
  apply hf_re,
  intro z,
  apply linear_isometry.l1 h,
end

lemma linear_isometry_complex_aux (f : ℂ →ₗᵢ[ℝ] ℂ) (h : f 1 = 1) :
  (∀ z, f z = z) ∨ (∀ z, f z = conj z) := by {
  have h0 : f I = I ∨ f I = -I,
  { have : |f I| = 1,
    { rw [←norm_eq_abs, linear_isometry.norm_map, norm_eq_abs, abs_I] },
    simp only [ext_iff, ←and_or_distrib_left, neg_re, I_re, neg_im, neg_zero],
    split,
    { rw ←I_re,
      rw linear_isometry.re h },
    { apply hf_im,
      { intro z, rw [←norm_eq_abs, ←norm_eq_abs, linear_isometry.norm_map] },
      { intro z, rw linear_isometry.re h, } } },
  refine or.imp (λ h1, _) (λ h1 z, _) h0,
  { suffices : f.to_linear_map = linear_isometry.id.to_linear_map,
    { simp [this, ←linear_isometry.coe_to_linear_map, linear_map.id_apply] },
    apply is_basis.ext is_basis_one_I,
    intro i,
    fin_cases i,
    { simp [h] },
    { -- I expected `simp [h1]` to work. Not sure why it didn't.
      simp only [matrix.head_cons, linear_isometry.coe_to_linear_map,
        linear_isometry.id_to_linear_map, linear_map.id_coe, id.def, matrix.cons_val_one],
      exact h1, } },
  { suffices : f.to_linear_map = conj_li.to_linear_map,
    { rw [←linear_isometry.coe_to_linear_map, this],
      simp only [linear_isometry.coe_to_linear_map],
      -- should have a simp lemma that does this
      refl },
    apply is_basis.ext is_basis_one_I,
    intro i,
    fin_cases i,
    { simp only [h, linear_isometry.coe_to_linear_map, matrix.cons_val_zero],
      change 1 = conj 1, -- simp lemma
      ext; simp },
    { -- I expected `simp [h1]` to work. Not sure why it didn't.
      simp only [matrix.head_cons, linear_isometry.coe_to_linear_map,
        linear_isometry.id_to_linear_map, linear_map.id_coe, id.def, matrix.cons_val_one],
      change f I = conj I,
      rw conj_I,
      exact h1, } },
}

[François Sunatori]

@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]

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_add' := λ x y, mul_add a x y,
    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]

Add noncomputable def ... to the beginning

[François Sunatori]

@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]

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

[Hanting Zhang]

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]

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]

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]

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_add' := λ x y, mul_add a x y,
    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]

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]

You want the proof that coe_fn is injective

[Eric Wieser]

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

[François Sunatori]

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

[Eric Wieser]

Oh, actually just tactic#ext should do the trick

[Hanting Zhang]

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

[François Sunatori]

@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]

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]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

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

[Eric Wieser]

But that can often lead simp in a direction that's unhelpful

[François Sunatori]

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]

and is the ⇑ linked to coe (coercion)?

[Eric Wieser]

Strictly ⇑ is docs#coe_fn

[Eric Wieser]

↑ 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]

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

[François Sunatori]

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]

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]

Does funext work in this context?

[Eric Rodriguez]

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]

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

[François Sunatori]

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

[Eric Wieser]

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