Analytic part of the Lindemann-Weierstrass theorem

theorem LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv (p : Polynomial ℂ) (s : ℂ) (x : ℝ) : HasDerivAt (fun (x : ℝ) => -(Complex.exp (-(x • s)) * Polynomial.eval (x • s) (Polynomial.sumIDeriv p))) (s * (Complex.exp (-(x • s)) * Polynomial.eval (x • s) p)) x

theorem LindemannWeierstrass.integral_exp_mul_eval (p : Polynomial ℂ) (s : ℂ) : s * ∫ (x : ℝ) in 0..1, Complex.exp (-(x • s)) * Polynomial.eval (x • s) p = -(Complex.exp (-s) * Polynomial.eval s (Polynomial.sumIDeriv p)) + Polynomial.eval 0 (Polynomial.sumIDeriv p)

theorem LindemannWeierstrass.exp_polynomial_approx (f : Polynomial ℤ) (hf : Polynomial.eval 0 f ≠ 0) : ∃ (c : ℝ), ∀ p > (Polynomial.eval 0 f).natAbs, Nat.Prime p → ∃ (n : ℤ), ¬↑p ∣ n ∧ ∃ (gp : Polynomial ℤ), gp.natDegree ≤ p * f.natDegree - 1 ∧ ∀ {r : ℂ}, r ∈ f.aroots ℂ → ‖n • Complex.exp r - p • (Polynomial.aeval r) gp‖ ≤ c ^ p / ↑(p - 1).factorial

See equation (68), page 285 of [Jacobson, Basic Algebra I, 4.12][jacobson1974].

Given a polynomial f with integer coefficients, we can find a constant c : ℝ and for each prime p > |f₀|, nₚ : ℤ and gₚ : ℤ[X] such that

• p does not divide nₚ
• deg(gₚ) < p * deg(f)
• all complex roots r of f satisfy |nₚ * e ^ r - p * gₚ(r)| ≤ c ^ p / (p - 1)!

In the proof of Lindemann-Weierstrass, we will take f to be a polynomial whose complex roots are the algebraic numbers whose exponentials we want to prove to be linearly independent.

Note: Jacobson writes Nₚ for our nₚ and M for our c (modulo a constant factor).