The auxiliary values of the Lindemann–Weierstrass theorem

Let x = ∑ δ_γ' [γ'] be a formal exponential sum over a field K, with support S of cardinality t, and let f = auxPoly S l p γ be the auxiliary polynomial of Hermite's proof of the Lindemann–Weierstrass theorem. The auxiliary value is auxValue x l p γ = -∑_{γ' ∈ S} δ_γ' (sumIDeriv f)(γ'), an element of K.

In Hermite's proof it is an algebraic integer, nonzero for large primes p, whose conjugates are small once ∑ δ_γ' exp γ' = 0. This file proves these four properties.

• algebraMap_auxValue_eq_sum_hermiteIntegral: if ∑ δ_γ' exp γ' = 0, then the image of auxValue x l p γ in ℂ is ∑ δ_γ' F_f(γ'), where F_f is Hermite's integral.
• auxValue_galConj: conjugating x by an automorphism τ conjugates its auxiliary values, auxValue (galConj τ x) l p (τ γ) = τ (auxValue x l p γ). In particular τ permutes the auxiliary values of a Galois-invariant sum.
• exists_auxValue_eq, isIntegral_auxValue: if the coefficients δ_γ' and the numbers l γ' are algebraic integers and γ ∈ S, then auxValue x l p γ is -δ_γ A ^ p modulo p times the algebraic integers, where A = l ^ t ∏_{γ' ∈ S, γ' ≠ γ} (γ - γ'); in particular it is an algebraic integer.
• auxValue_ne_zero: under the same hypotheses and l ≠ 0, over a number field, auxValue x l p γ ≠ 0 for every prime p with |N(δ_γ A)| < p.
• norm_auxValue_le, eventually_norm_auxValue_lt_one: if ∑ δ_γ' exp γ' = 0, then the auxiliary values are bounded by C c ^ p / (p - 1)!, so that they all have absolute value less than 1 for large p.

The polynomial estimate behind the bound is norm_eval_auxPoly_le.

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 4, §4.2, the proof of Theorem 4.11 and Lemmas 4.12, 4.14 and 4.15.

noncomputable def TauCeti.LindemannWeierstrass.auxValue {K : Type u_1} [Field K] [DecidableEq K] (x : AddMonoidAlgebra K K) (l p : ℕ) (γ : K) : K

The auxiliary value -∑_{γ' ∈ S} δ_γ' (sumIDeriv f)(γ') of Hermite's proof of the Lindemann–Weierstrass theorem, for the formal exponential sum x = ∑ δ_γ' [γ'] with support S and the auxiliary polynomial f = auxPoly S l p γ.

theorem TauCeti.LindemannWeierstrass.auxValue_def {K : Type u_1} [Field K] [DecidableEq K] (x : AddMonoidAlgebra K K) (l p : ℕ) (γ : K) : auxValue x l p γ = -∑ γ' ∈ x.coeff.support, x.coeff γ' * Polynomial.eval γ' (Polynomial.sumIDeriv (auxPoly x.coeff.support l p γ))

The defining formula of auxValue x l p γ.

@[simp]

theorem TauCeti.LindemannWeierstrass.auxValue_zero {K : Type u_1} [Field K] [DecidableEq K] (l p : ℕ) (γ : K) : auxValue 0 l p γ = 0

The auxiliary values of the zero sum vanish.

theorem TauCeti.LindemannWeierstrass.auxValue_galConj {K : Type u_1} [Field K] [DecidableEq K] {F : Type u_2} [CommSemiring F] [Algebra F K] (τ : K ≃ₐ[F] K) (x : AddMonoidAlgebra K K) (l p : ℕ) (γ : K) : auxValue ((galConj τ) x) l p (τ γ) = τ (auxValue x l p γ)

Conjugating a formal exponential sum by an automorphism τ conjugates its auxiliary values: auxValue (galConj τ x) l p (τ γ) = τ (auxValue x l p γ).

theorem TauCeti.LindemannWeierstrass.exists_auxValue_eq {K : Type u_1} [Field K] [DecidableEq K] [CharZero K] {x : AddMonoidAlgebra K K} {l p : ℕ} {γ : K} (hγ : γ ∈ x.coeff.support) (hp : p ≠ 0) (hx : ∀ (γ' : K), IsIntegral ℤ (x.coeff γ')) (hl : ∀ γ' ∈ x.coeff.support, IsIntegral ℤ (↑l * γ')) : ∃ (w : K), IsIntegral ℤ w ∧ auxValue x l p γ = -(x.coeff γ * (↑l ^ x.coeff.support.card * ∏ γ' ∈ x.coeff.support.erase γ, (γ - γ')) ^ p + ↑p * w)

If the coefficients of x and the numbers l γ' for γ' in the support S of x are algebraic integers, γ ∈ S and p ≠ 0, then auxValue x l p γ = -(δ_γ A ^ p + p w) for an algebraic integer w, where A = l ^ t ∏_{γ' ∈ S, γ' ≠ γ} (γ - γ').

theorem TauCeti.LindemannWeierstrass.isIntegral_auxValue {K : Type u_1} [Field K] [DecidableEq K] [CharZero K] {x : AddMonoidAlgebra K K} {l p : ℕ} {γ : K} (hγ : γ ∈ x.coeff.support) (hx : ∀ (γ' : K), IsIntegral ℤ (x.coeff γ')) (hl : ∀ γ' ∈ x.coeff.support, IsIntegral ℤ (↑l * γ')) : IsIntegral ℤ (auxValue x l p γ)

If the coefficients of x and the numbers l γ' for γ' in the support of x are algebraic integers, then the auxiliary value auxValue x l p γ at a point γ of the support is an algebraic integer.

theorem TauCeti.LindemannWeierstrass.auxValue_ne_zero {K : Type u_1} [Field K] [DecidableEq K] [CharZero K] [NumberField K] {x : AddMonoidAlgebra K K} {l p : ℕ} {γ : K} (hγ : γ ∈ x.coeff.support) (hx : ∀ (γ' : K), IsIntegral ℤ (x.coeff γ')) (hl₀ : l ≠ 0) (hl : ∀ γ' ∈ x.coeff.support, IsIntegral ℤ (↑l * γ')) (hp : Nat.Prime p) (hpN : |(Algebra.norm ℚ) (x.coeff γ * (↑l ^ x.coeff.support.card * ∏ γ' ∈ x.coeff.support.erase γ, (γ - γ')))| < ↑p) : auxValue x l p γ ≠ 0

Nonvanishing of the auxiliary values. Let K be a number field, let the coefficients of x and the numbers l γ' for γ' in the support S of x be algebraic integers, l ≠ 0 and γ ∈ S. Then auxValue x l p γ ≠ 0 for every prime p exceeding |N(δ_γ A)|, where A = l ^ t ∏_{γ' ∈ S, γ' ≠ γ} (γ - γ') and N is the norm from K to ℚ.

theorem TauCeti.LindemannWeierstrass.norm_eval_auxPoly_le {𝕜 : Type u_1} [RCLike 𝕜] [DecidableEq 𝕜] {S : Finset 𝕜} (l p : ℕ) {γ : 𝕜} (hγ : γ ∈ S) {R : ℝ} (hS : ∀ γ' ∈ S, ‖γ'‖ ≤ R) {u : 𝕜} (hu : ‖u‖ ≤ R) : ‖Polynomial.eval u (auxPoly S l p γ)‖ ≤ (↑l * (2 * R + 1)) ^ (S.card * p) / ↑(p - 1).factorial

The size of the auxiliary polynomial. If γ ∈ S and all the points of S have absolute value at most R, then |auxPoly S l p γ (u)| ≤ (l (2 R + 1)) ^ (t p) / (p - 1)! for every u with |u| ≤ R, where t is the cardinality of S.

theorem TauCeti.LindemannWeierstrass.algebraMap_auxValue_eq_sum_hermiteIntegral {K : Type u_1} [Field K] [DecidableEq K] [Algebra K ℂ] {x : AddMonoidAlgebra K K} (hx : (expEval K) x = 0) (l p : ℕ) (γ : K) : (algebraMap K ℂ) (auxValue x l p γ) = ∑ γ' ∈ x.coeff.support, (algebraMap K ℂ) (x.coeff γ') * (Polynomial.map (algebraMap K ℂ) (auxPoly x.coeff.support l p γ)).hermiteIntegral ((algebraMap K ℂ) γ')

Hermite's analytic expression for the auxiliary values. If the formal exponential sum x = ∑ δ_γ' [γ'] with support S satisfies ∑ δ_γ' exp γ' = 0, then the image of auxValue x l p γ in ℂ is ∑_{γ' ∈ S} δ_γ' F_f(γ'), where F_f is Hermite's integral of f = auxPoly S l p γ.

theorem TauCeti.LindemannWeierstrass.norm_auxValue_le {K : Type u_1} [Field K] [DecidableEq K] [Algebra K ℂ] {x : AddMonoidAlgebra K K} (hx : (expEval K) x = 0) (l p : ℕ) {γ : K} (hγ : γ ∈ x.coeff.support) {R : ℝ} (hR : ∀ γ' ∈ x.coeff.support, ‖(algebraMap K ℂ) γ'‖ ≤ R) : ‖(algebraMap K ℂ) (auxValue x l p γ)‖ ≤ (∑ γ' ∈ x.coeff.support, ‖(algebraMap K ℂ) (x.coeff γ')‖) * R * Real.exp R * ((↑l * (2 * R + 1)) ^ (x.coeff.support.card * p) / ↑(p - 1).factorial)

The size of the auxiliary values. If the formal exponential sum x = ∑ δ_γ' [γ'] with support S satisfies ∑ δ_γ' exp γ' = 0, γ ∈ S and all the points of S have absolute value at most R, then |auxValue x l p γ| ≤ (∑ |δ_γ'|) R exp(R) (l (2 R + 1)) ^ (t p) / (p - 1)!, where t is the cardinality of S.

theorem TauCeti.LindemannWeierstrass.eventually_norm_auxValue_lt_one {K : Type u_1} [Field K] [DecidableEq K] [Algebra K ℂ] {x : AddMonoidAlgebra K K} (hx : (expEval K) x = 0) (l : ℕ) : ∀ᶠ (p : ℕ) in Filter.atTop, ∀ γ ∈ x.coeff.support, ‖(algebraMap K ℂ) (auxValue x l p γ)‖ < 1

If the formal exponential sum x satisfies ∑ δ_γ' exp γ' = 0, then for all large p the auxiliary values auxValue x l p γ at the points γ of the support of x have absolute value less than 1.

Examples