The auxiliary polynomials of the Lindemann–Weierstrass theorem

For a finite set S of t elements of a field K, natural numbers l and p, and γ ∈ K, auxPoly S l p γ is the polynomial f = l ^ (t p) / (p - 1)! * (X - γ) ^ (p - 1) * ∏_{γ' ∈ S, γ' ≠ γ} (X - γ') ^ p. In Hermite's proof of the Lindemann–Weierstrass theorem S is the support of a vanishing exponential sum ∑ δ_γ' exp γ' with algebraic δ_γ' and γ', l is a common denominator of the exponents and p is a large prime. The number ∑_γ' δ_γ' (sumIDeriv f)(γ') is then a nonzero algebraic integer all of whose conjugates have absolute value less than one, which is impossible.

This file proves the algebraic half of that argument: the values of the derivatives of f at the points of S. With A = l ^ t ∏_{γ' ∈ S, γ' ≠ γ} (γ - γ'),

• eval_iterate_derivative_auxPoly_self: f⁽ᵖ⁻¹⁾(γ) = A ^ p;
• eval_iterate_derivative_auxPoly_self_of_lt, eval_iterate_derivative_auxPoly_of_ne: all other derivatives of order < p vanish at the points of S;
• isIntegral_eval_iterate_derivative_auxPoly_div: if l γ' is an algebraic integer for every γ' ∈ S and γ ∈ S, then for j ≥ p the value f⁽ʲ⁾(z) / p is an algebraic integer whenever l z is;
• exists_eval_sumIDeriv_auxPoly_eq: consequently (sumIDeriv f)(γ') is A ^ p at γ' = γ, and 0 at the other points of S, up to p times an algebraic integer.

We also record the degree t p - 1 of f (natDegree_auxPoly) and the compatibility of auxPoly with field homomorphisms (auxPoly_map), used to conjugate it by Galois automorphisms.

References

• J.-H. Evertse, Diophantine Approximation (2019), ch. 4, §4.2, the proof of Theorem 4.11 and Lemma 4.13.

noncomputable def TauCeti.LindemannWeierstrass.auxPoly {K : Type u_1} [Field K] [DecidableEq K] (S : Finset K) (l p : ℕ) (γ : K) : Polynomial K

The auxiliary polynomial l ^ (t p) / (p - 1)! * (X - γ) ^ (p - 1) * ∏ (X - γ') ^ p of Hermite's proof of the Lindemann–Weierstrass theorem, where t is the cardinality of S and the product runs over the elements γ' ≠ γ of S.

theorem TauCeti.LindemannWeierstrass.auxPoly_def {K : Type u_1} [Field K] [DecidableEq K] (S : Finset K) (l p : ℕ) (γ : K) : auxPoly S l p γ = Polynomial.C (↑l ^ (S.card * p) / ↑(p - 1).factorial) * (Polynomial.X - Polynomial.C γ) ^ (p - 1) * ∏ γ' ∈ S.erase γ, (Polynomial.X - Polynomial.C γ') ^ p

The defining formula of auxPoly S l p γ.

@[simp]

theorem TauCeti.LindemannWeierstrass.auxPoly_map {K : Type u_1} [Field K] [DecidableEq K] {L : Type u_2} [Field L] [DecidableEq L] (φ : K →+* L) (S : Finset K) (l p : ℕ) (γ : K) : Polynomial.map φ (auxPoly S l p γ) = auxPoly (Finset.image (⇑φ) S) l p (φ γ)

Applying a field homomorphism to the coefficients of auxPoly S l p γ replaces S and γ by their images.

theorem TauCeti.LindemannWeierstrass.natDegree_auxPoly {K : Type u_1} [Field K] [DecidableEq K] [CharZero K] {S : Finset K} {l p : ℕ} {γ : K} (hγ : γ ∈ S) (hl : l ≠ 0) : (auxPoly S l p γ).natDegree = S.card * p - 1

For γ ∈ S and nonzero l, the polynomial auxPoly S l p γ has natural degree t p - 1, where t is the cardinality of S. This includes p = 0, when the polynomial is 1.

theorem TauCeti.LindemannWeierstrass.eval_iterate_derivative_auxPoly_self {K : Type u_1} [Field K] [DecidableEq K] [CharZero K] (S : Finset K) (l p : ℕ) (γ : K) : Polynomial.eval γ ((⇑Polynomial.derivative)^[p - 1] (auxPoly S l p γ)) = (↑l ^ S.card * ∏ γ' ∈ S.erase γ, (γ - γ')) ^ p

The (p - 1)-st derivative of auxPoly S l p γ at γ is (l ^ t ∏_{γ' ∈ S, γ' ≠ γ} (γ - γ')) ^ p.

theorem TauCeti.LindemannWeierstrass.eval_iterate_derivative_auxPoly_self_of_lt {K : Type u_1} [Field K] [DecidableEq K] (S : Finset K) (l : ℕ) {p j : ℕ} (γ : K) (hj : j < p - 1) : Polynomial.eval γ ((⇑Polynomial.derivative)^[j] (auxPoly S l p γ)) = 0

The derivatives of auxPoly S l p γ of order less than p - 1 vanish at γ.

theorem TauCeti.LindemannWeierstrass.eval_iterate_derivative_auxPoly_of_ne {K : Type u_1} [Field K] [DecidableEq K] {S : Finset K} (l : ℕ) {p j : ℕ} {γ γ' : K} (hγ' : γ' ∈ S) (hne : γ' ≠ γ) (hj : j < p) : Polynomial.eval γ' ((⇑Polynomial.derivative)^[j] (auxPoly S l p γ)) = 0

The derivatives of auxPoly S l p γ of order less than p vanish at every point of S other than γ.

theorem TauCeti.LindemannWeierstrass.isIntegral_eval_iterate_derivative_auxPoly_div {K : Type u_1} [Field K] [DecidableEq K] [CharZero K] {S : Finset K} {l p : ℕ} {γ : K} (hγ : γ ∈ S) (hS : ∀ γ' ∈ S, IsIntegral ℤ (↑l * γ')) {z : K} (hz : IsIntegral ℤ (↑l * z)) {j : ℕ} (hj : p ≤ j) : IsIntegral ℤ (Polynomial.eval z ((⇑Polynomial.derivative)^[j] (auxPoly S l p γ)) / ↑p)

If γ ∈ S and l γ' is an algebraic integer for every γ' ∈ S, then for j ≥ p the j-th derivative of auxPoly S l p γ takes values in p times the algebraic integers at every z for which l z is an algebraic integer.

theorem TauCeti.LindemannWeierstrass.exists_eval_sumIDeriv_auxPoly_eq {K : Type u_1} [Field K] [DecidableEq K] [CharZero K] {S : Finset K} {l p : ℕ} {γ : K} (hγ : γ ∈ S) (hp : p ≠ 0) (hS : ∀ γ' ∈ S, IsIntegral ℤ (↑l * γ')) {γ' : K} (hγ' : γ' ∈ S) : ∃ (y : K), IsIntegral ℤ y ∧ Polynomial.eval γ' (Polynomial.sumIDeriv (auxPoly S l p γ)) = (if γ' = γ then (↑l ^ S.card * ∏ γ'' ∈ S.erase γ, (γ - γ'')) ^ p else 0) + ↑p * y

If γ ∈ S, p ≠ 0 and l γ' is an algebraic integer for every γ' ∈ S, then at every point γ' of S the sum of all derivatives of auxPoly S l p γ is, up to p times an algebraic integer, equal to (l ^ t ∏_{γ'' ∈ S, γ'' ≠ γ} (γ - γ'')) ^ p if γ' = γ and to 0 otherwise.

Examples