Theorems · Theorem · number theory

LindemannWeierstrass.exp_polynomial_approx

∀ (f : Polynomial ℤ),
  Polynomial.eval 0 f ≠ 0 →
    ∃ c,
      ∀ p > (Polynomial.eval 0 f).natAbs,
        Nat.Prime p →
          ∃ n,
            ¬↑p ∣ n ∧
              ∃ gp,
                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).

Defined in

Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Cited by

0 results in Mathlib

Foundations

Depth 273 from the axioms · uses propext, Classical.choice, Quot.sound