Lindemann-Weierstrass theorem almost done

Stream: maths

[Yuyang Zhao]

Dear All,

I'm happy to tell everyone that I have formalized most of the Lindemann-Weierstrass theorem. The main theorem is here.

theorem linear_independent_exp
  (u : ι → ℂ) (hu : ∀ i, is_integral ℚ (u i)) (u_inj : function.injective u)
  (v : ι → ℂ) (hv : ∀ i, is_integral ℚ (v i))
  (h : ∑ i, v i * exp (u i) = 0) :
  v = 0

There are still some sorry in the code. Two of them are waiting for @Damiano Testa's work on is_domain for add_monoid_algebra. And the other two are fundamental theorem of symmetric polynomials. Symmetric polynomials are only used in the very last part of the proof, and I believe it can be replaced by some Galois theory, however, it seems to be the simplest way if we have sufficient infrastructures.

There is also a file e.lean in this repository, that is unrelated to this work. I just reused this repository.

If there is any way to improve my proof, please feel free to give suggestions.

[Damiano Testa]

That's great, congratulations!

I've broken one of the is_domain PR, but have not yet had time to figure out which instance I still need to provide to make it compile again. I'll try to do it soon, but I'm not sure how much time I'll have before late next week.

[Johan Commelin]

Have you considered using is_algebraic in your statement? It's trivially equivalent, of course, but it matches what people would usually write, I think.

[Ruben Van de Velde]

Nice, sounds like I can drop #15954 then :)

[Johan Commelin]

Isn't that a prerequisite? Or did @Yuyang Zhao do a completely new proof?

[Yuyang Zhao]

Johan Commelin said:

Isn't that a prerequisite? Or did Yuyang Zhao do a completely new proof?

My proof is independent. I think I knew about that PR very late, probably after I had finished the analytical part. I didn't check how many duplicates there are.

[Yuyang Zhao]

Johan Commelin said:

Have you considered using is_algebraic in your statement? It's trivially equivalent, of course, but it matches what people would usually write, I think.

I would add some variants of this statement.

[Yuyang Zhao]

Damiano Testa said:

That's great, congratulations!

I've broken one of the is_domain PR, but have not yet had time to figure out which instance I still need to provide to make it compile again. I'll try to do it soon, but I'm not sure how much time I'll have before late next week.

K s is a ℚ-vector space, so it's just ring equiv to is_domain (add_monoid_algebra (ι →₀ ℚ) F).

[Johan Commelin]

I see. So you have an independent proof of transcendence of e. Because that mathematical fact is still an input to your proof of Lindemann─Weierstrass, right?

[Yuyang Zhao]

No, it just doesn't need the proof of transcendence of e. I mean e.lean is previously written in this repository and has no relation to this proof.

[Johan Commelin]

Oooh, ok! :bulb:

[Junyan Xu]

I'm outlining in Lean the second proof in Wikipedia for the symmetric polynomial theorem, which essentially uses docs#finsupp.lex that Damiano introduced into mathlib recently (looks like we'll also need well-foundedness apart from linear order). The first thing I observed is that the sorry as stated seems to be wrong: we don't get an isomorphism for comm_semiring because for example x^2+y^2=(x+y)^2+(-2)xy, and -2 doesn't exist in ℕ. However I think @Yuyang Zhao only applies it to comm_rings, so it should be okay.

[Yuyang Zhao]

Thanks! I didn't check the conditions carefully and the assumption comm_semiring is too weak, but comm_ring is certainly enough.

[Ruben Van de Velde]

@Yuyang Zhao have you (or someone else) been working on the symmetric polynomial proof? Would be cool to get this finished

[Yuyang Zhao]

I don't know anyone who is working on the symmetric polynomial proof. This part of the theory is related to integer partitions or Young diagrams, and their APIs still seem inadequate. I think it might be better to discuss with other people who need these APIs.

[Junyan Xu]

I thought about the proof and opened #16772 (well-foundedness of lexicographic orders) with the proof as an motivation (the other motivation being this thread). (I proved a much more general result, but deducing what we actually need from the general result is arguably what we should do for mathlib.) However, one dependency #16777 of the well-foundedness result hasn't been merged yet, and I haven't returned to the symmetric polynomial proof. As far as I can see, it doesn't have to depend on Young diagrams, but it may be nice to make the connection.

[Junyan Xu]

Happy to announce that the fundamental theorem of symmetric polynomials has been done in #6593!

[Ruben Van de Velde]

Junyan Xu said:

Happy to announce that the fundamental theorem of symmetric polynomials have been done in #6593!

Have you looked at porting your mathlib3 PR for Lindemann-Weierstrass? If not, I might spend some time on that soonish

[Junyan Xu]

That was @Yuyang Zhao 's branch repo (~3.3k lines), not yet made into a PR AFAIK. Looking into porting is certainly welcome, but there's still a missing piece (see my comment) that should probably be done via docs#UniqueSums now.

[Ruben Van de Velde]

Whoops, sorry, names are hard for me. I'll take a look

[Ruben Van de Velde]

Some initial work at https://github.com/leanprover-community/mathlib4/compare/transcendental?expand=1

[Damiano Testa]

@Junyan Xu, contrary to my comment, I started porting the NoZeroDivisor instance: #6627.

The PR is just the back-end work. I have not actually golfed the NZD instance on Polynomials.

[Junyan Xu]

Oh thanks a lot @Damiano Testa ! But I thought your motivation of introducing docs#UniqueSums is to prove NoZeroDivisor in that generality, and then show a biordered (add_)monoid has unique products/sums? I will comment on your PR.

Re: the Lindemann-Weierstrass PR: I looked at the one file that was ported by Ruben, and my first impressions are that we should try to avoid the reliance on quotient.out, which shouldn't be hard, and that we could also avoid using HEq with an easier proof of minpoly.inj.

[Damiano Testa]

Junyan, you are absolutely right! :face_palm: I simply went ahead and re-PRed the earlier version. I'll update it, though not today!

[Ruben Van de Velde]

@Damiano Testa I was looking at using your PR in branch#transcendental, but am being hindered by not knowing what I'm doing :)

Would you be able to offer some guidance?

[Damiano Testa]

Ruben, sure! Except... can you be more specific on the kind of guidance?

[Ruben Van de Velde]

Concretely, I've got two sorries here: https://github.com/leanprover-community/mathlib4/blob/transcendental/Mathlib/Analysis/Transcendental.lean#L982 (can't really call it a "minimal" working example :))

[Damiano Testa]

Ah, ok, I'll take a look!

[Damiano Testa]

I'm trying to slowly get up to speed.

[Damiano Testa]

AddMonoidAlgebra (K s) (K s) seems to mean the AddMonoidAlgebra

• whose base ring is K s, a splitting field -- good, and
• whose grading (add)monoid is K s, the same field.

The latter seems like it should be something else...

[Damiano Testa]

Should maybe the second K s be some form of Nat or something similar?

[Damiano Testa]

(Summarizing, AddMonoidAlgebra R A means taking R-linear combinations of "monomials" indexes by A. So, common choices for A are Nat (and you get polynomials), \sigma -> Nat (and you get multivariate polynomials on a set of variables indexed by \sigma).)

[Damiano Testa]

As Lean confirms, what is there does type-check, but seems "wrong" to me...

[Damiano Testa]

Anyway, reading further, I see that this happens a lot in the file. So, let me stop questioning what the question is and try to fill in the sorries!

[Ruben Van de Velde]

(I'm trying to make lean 3 tell me where it's used, but it's in a bad mood today)

[Damiano Testa]

Ok, no worries. Here is a silly approach to break the first sorry into two:

import Mathlib.Analysis.Transcendental
import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
import Mathlib.Algebra.Group.UniqueProds

variable (s : Finset ℂ)

instance instIsDomain1 : NoZeroDivisors (AddMonoidAlgebra (K s) (K s)) := by
  let _ : LinearOrder (K s) := sorry
  let _ : CovariantClass (K s) (K s) (· + ·) (· < ·) := sorry
  apply AddMonoidAlgebra.NoZeroDivisors.biOrdered

[Damiano Testa]

(I created a new file, removing the sorries from the old one.)

[Damiano Testa]

I suspect that it will be easier to prove that K s satisfies UniqueSums, rather than going via an order, but the instance UniqueSums (K s) -> NoZeroDivisors (AddMonoidAlgebra (K s) (K s) is not even PRed.

[Damiano Testa]

I was going to do this in mathlib3, did not do it there (but PRed the relevant background from UniqueSums), then thought I had PRed it to mathlib4, but actually I PRed an older version that might be harder to use in this case.

[Damiano Testa]

Let's try and see if this works

import Mathlib.Analysis.Transcendental
import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
import Mathlib.Algebra.Group.UniqueProds

instance wanted {R A : Type*} [Semiring R] [NoZeroDivisors R] [AddMonoid A] [UniqueSums A] :
    NoZeroDivisors (AddMonoidAlgebra R A) := sorry

variable (s : Finset ℂ)

instance : UniqueSums (K s) := sorry

instance instIsDomain1 : NoZeroDivisors (AddMonoidAlgebra (K s) (K s)) := inferInstance

[Ruben Van de Velde]

This first one is used in one place: the prod_ne_zero_iff in https://github.com/negiizhao/transcendental/blob/master/src/lindemann.lean#L1281 , so strictly speaking it needs NoZeroDivisors rather than IsDomain

[Damiano Testa]

The difference between NoZeroDivisors and IsDomain is tiny, I would focus on NoZeroDivisors. Usually, IsDomain follows by increasing the typeclass assumptions on the base "ring" and deducing it from NoZeroDivisors.

[Damiano Testa]

I cannot remember the details, but essentially NoZeroDivisors applies to Semirings, while IsDomain uses a Ring, but they are otherwise identical.

[Damiano Testa]

I am almost certain that wanted is true and the proof is simply looking at the support and the "unique sum in there".

[Ruben Van de Velde]

I need to step out for a bit - thanks for looking in any case!

[Damiano Testa]

instance : UniqueSums (K s) := sorry

I have not really thought about, but I would argue informally that

• finite subsets of K s span, as an additive submodule, something of the form Nat ^ n;
• Nat ^ n satisfies UniqueSums
• therefore K s satisfies UniqueSums.

[Damiano Testa]

Ok, here is a proof of wanted:

import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
import Mathlib.Algebra.Group.UniqueProds

open Finsupp in
instance wanted {R A : Type*} [Semiring R] [NoZeroDivisors R] [AddMonoid A] [UniqueSums A] :
    NoZeroDivisors (AddMonoidAlgebra R A) where
  eq_zero_or_eq_zero_of_mul_eq_zero := fun {a b} c => by
    rcases eq_or_ne a 0 with (rfl | ha)
    · simp
    rcases eq_or_ne b 0 with (rfl | hb)
    · simp
    contrapose! c
    obtain ⟨da, a0, db, b0, h⟩ := UniqueSums.uniqueAdd_of_nonempty
      (support_nonempty_iff.mpr ha) (support_nonempty_iff.mpr hb)
    apply support_nonempty_iff.mp
    apply Set.nonempty_of_mem (x := da + db)
    apply mem_support_iff.mpr
    convert_to a da * b db ≠ 0
    · rw [AddMonoidAlgebra.mul_apply_add_eq_mul_of_forall_ne]
      intros m n ma nb H
      contrapose! H
      apply h ma nb H
    · apply mul_eq_zero.not.mpr ?_
      simp [not_or, mem_support_iff.mp a0, mem_support_iff.mp b0]

Note: I simply aimed to prove the result above -- golfing expected and welcome!

[Damiano Testa]

@Ruben Van de Velde I think that what is below proves the two sorries that you had:

import Mathlib.Analysis.Transcendental
import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
import Mathlib.Algebra.Group.UniqueProds
import Mathlib.Data.Finsupp.Lex
import Mathlib.Order.Extension.Linear

namespace UniqueProds

variable {G H : Type*} [Mul G] [Mul H]

@[to_additive]
theorem mulHom_image_of (f : G ≃* H) (uG : UniqueProds G) : UniqueProds H := by
  classical
  constructor
  intros A B A0 B0
  obtain ⟨a0, ha0, b0, hb0, h⟩ := uG.uniqueMul_of_nonempty
    (A0.image f.invFun) (B0.image f.invFun)
  refine ⟨f a0, ?_, f b0, ?_, ?_⟩
  · rw [← Finset.image_id (s := A), ← (MulEquiv.eq_symm_comp f f.invFun id).mp rfl]
    convert Finset.mem_image_of_mem f ha0
    ext
    simp only [MulEquiv.toEquiv_eq_coe, Equiv.invFun_as_coe, MulEquiv.coe_toEquiv_symm,
      MulEquiv.self_comp_symm, Finset.image_id, Finset.mem_image, exists_exists_and_eq_and,
      MulEquiv.apply_symm_apply, exists_eq_right]
  · rw [← Finset.image_id (s := B), ← (MulEquiv.eq_symm_comp f f.invFun id).mp rfl]
    convert Finset.mem_image_of_mem f hb0
    ext
    simp only [MulEquiv.toEquiv_eq_coe, Equiv.invFun_as_coe, MulEquiv.coe_toEquiv_symm,
      MulEquiv.self_comp_symm, Finset.image_id, Finset.mem_image, exists_exists_and_eq_and,
      MulEquiv.apply_symm_apply, exists_eq_right]
  · convert (UniqueMul.mulHom_image_iff (G := G) (H := H) f (EquivLike.injective f)).mpr h <;>
    · ext; simp

/-- `UniqueProd` is preserved under multiplicative equivalences. -/
@[to_additive "`UniqueSums` is preserved under additive equivalences."]
theorem mulHom_image_iff [DecidableEq H] (f : G ≃* H) :
    UniqueProds G ↔ UniqueProds H :=
⟨mulHom_image_of f, mulHom_image_of f.symm⟩

end UniqueProds

instance vs {L σ : Type*} [LinearOrder σ] [LinearOrder L] [AddGroup L]
    [ContravariantClass L L (· + ·) (· ≤ ·)]
    [CovariantClass L L (Function.swap (· + ·)) (· ≤ ·)] :
    UniqueSums (σ →₀ L) := show UniqueSums ((Lex (σ →₀ L))) from
  { uniqueAdd_of_nonempty := fun {A B} A0 B0 => by
      refine ⟨_, A.max'_mem A0, _, B.max'_mem B0, ?_⟩
      intros a b aA bB
      exact (add_eq_add_iff_eq_and_eq (A.le_max' a aA) (B.le_max' b bB)).mp }

open Finsupp in
instance wanted {R A : Type*} [Semiring R] [NoZeroDivisors R] [AddMonoid A] [UniqueSums A] :
    NoZeroDivisors (AddMonoidAlgebra R A) where
  eq_zero_or_eq_zero_of_mul_eq_zero := fun {a b} c => by
    rcases eq_or_ne a 0 with (rfl | ha)
    · simp
    rcases eq_or_ne b 0 with (rfl | hb)
    · simp
    contrapose! c
    obtain ⟨da, a0, db, b0, h⟩ := UniqueSums.uniqueAdd_of_nonempty
      (support_nonempty_iff.mpr ha) (support_nonempty_iff.mpr hb)
    apply support_nonempty_iff.mp
    apply Set.nonempty_of_mem (x := da + db)
    apply mem_support_iff.mpr
    convert_to a da * b db ≠ 0
    · rw [AddMonoidAlgebra.mul_apply_add_eq_mul_of_forall_ne]
      intros m n ma nb H
      contrapose! H
      apply h ma nb H
    · apply mul_eq_zero.not.mpr ?_
      simp [not_or, mem_support_iff.mp a0, mem_support_iff.mp b0]

variable (s : Finset ℂ)

instance {R : Type*} [AddCommGroup R] [Module ℚ R] :
    UniqueSums R := by
  let bas := Basis.ofVectorSpace ℚ R
  let r := bas.repr
  apply UniqueSums.addHom_image_of (G := ((Basis.ofVectorSpaceIndex ℚ R) →₀ ℚ)) r.symm
  let _ : PartialOrder (Basis.ofVectorSpaceIndex ℚ R) :=
  { le := (· = ·)
    le_refl := fun a ↦ rfl
    le_trans := fun a b c ab bc => Eq.trans ab bc
    le_antisymm := fun a b ab _ => ab }
  let _ : LinearOrder ((Basis.ofVectorSpaceIndex ℚ R)) := by
    show LinearOrder (LinearExtension (Basis.ofVectorSpaceIndex ℚ R))
    exact inferInstance
  exact inferInstance

instance instIsDomain1 : NoZeroDivisors (AddMonoidAlgebra (K s) (K s)) := inferInstance
instance instIsDomain2 : IsDomain (AddMonoidAlgebra ℚ (K s)) := IsDomain.mk

I made no effort to clean up: feel free to adapt as you see fit!

[Damiano Testa]

There is some awkwardness, since you choose an arbitrary linear order on a type to deduce UniqueSums. In some sense, this is expected: UniqueSums is not the "correct" hypothesis, it is just a sufficient one. I do not know what a better approach could be.

[Ruben Van de Velde]

Thanks!

[Maarten Derickx]

(deleted)

[Ruben Van de Velde]

(deleted)

[Damiano Testa]

I thought that I had proved mulHom_image_of with the assumption f : H →* G injective. That should be true and better!

[Ruben Van de Velde]

Still 15 or so errors in the mathport output and a few proofs timing out, but that'll be for tomorrow (unless someone feels like looking into it)

[Yuyang Zhao]

https://github.com/leanprover-community/mathlib4/blob/f3f8ba065f461a239bc798d69517f8231ee431f6/Mathlib/Analysis/Transcendental.lean#L1787 Eventually the Lindemann-Weierstrass theorem was ported to Lean4 and all sorrys were removed. Thank you everyone!

[Yuyang Zhao]

Some tactics such as simp only and simp_rw are very slow near the end of the file. This did not happen in lean3 IIRC.

[Ruben Van de Velde]

Do you want to make the pr? :)

[Damiano Testa]

I was thinking of taking care of PRing the NoZeroDivisors and IsDomain instances today.

[Damiano Testa]

(I'm just saying this, so you do not waste time with that part, which is essentially orthogonal to the actual result.)

[Damiano Testa]

#6723

[Ruben Van de Velde]

@Yuyang Zhao not sure if you noticed, but #6740 is delegated to you