Analytic part of the Lindemann-Weierstrass theorem #
theorem
LindemannWeierstrass.exp_polynomial_approx
(f : Polynomial ℤ)
(hf : Polynomial.eval 0 f ≠ 0)
:
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 dividenₚ
deg(gₚ) < p * deg(f)
- all complex roots
r
off
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).