English
There exists a positive real A such that, under a Liouville-type setup with a Lipschitz control and denominator bounds, a positive lower bound 1 ≤ d(a)(distα(jz a))·A holds for all z,a in the specified index sets.
Русский
Существует положительная константа A, обеспечивающая нижнюю границу в Liouville-типовой схеме с ограничениями по Lipschitz и делителям.
LaTeX
$$$\\exists A>0,\\; \\forall z,a,\\; 1\\le d(a)\\cdot\\bigl(dist(α, j(z,a))\\cdot A\\bigr).$$$
Lean4
/-- 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).
-/
theorem exp_polynomial_approx (f : ℤ[X]) (hf : f.eval 0 ≠ 0) :
∃ c,
∀ p > (eval 0 f).natAbs,
p.Prime →
∃ n : ℤ,
¬↑p ∣ n ∧
∃ gp : ℤ[X],
gp.natDegree ≤ p * f.natDegree - 1 ∧
∀ {r : ℂ}, r ∈ f.aroots ℂ → ‖n • exp r - p • aeval r gp‖ ≤ c ^ p / (p - 1)! :=
by
simp_rw [nsmul_eq_mul, zsmul_eq_mul]
choose c' c'0 Pp'_le using exp_polynomial_approx_aux f
use if h : ((f.aroots ℂ).map c').toFinset.Nonempty then ((f.aroots ℂ).map c').toFinset.max' h else 0
intro p p_gt prime_p
obtain ⟨gp', -, h'⟩ := eval_sumIDeriv_of_pos (X ^ (p - 1) * f ^ p) prime_p.pos
specialize h' 0 (by rw [C_0, sub_zero])
use f.eval 0 ^ p + p * gp'.eval 0
constructor
· rw [dvd_add_left (dvd_mul_right _ _)]
contrapose! p_gt with h
exact Nat.le_of_dvd (Int.natAbs_pos.mpr hf) (Int.natCast_dvd.mp (Int.Prime.dvd_pow' prime_p h))
obtain ⟨gp, gp'_le, h⟩ := aeval_sumIDeriv ℂ (X ^ (p - 1) * f ^ p) p
refine ⟨gp, ?_, ?_⟩
· refine gp'_le.trans ((tsub_le_tsub_right natDegree_mul_le p).trans ?_)
rw [natDegree_X_pow, natDegree_pow, tsub_add_eq_add_tsub prime_p.one_le, tsub_right_comm, add_tsub_cancel_left]
intro r hr
specialize h r _
· rw [mem_roots'] at hr
rw [Polynomial.map_mul, f.map_pow]
exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd (dvd_iff_isRoot.mpr hr.2) _) _
rw [nsmul_eq_mul] at h
have :
(↑(eval 0 f ^ p + p * eval 0 gp') * cexp r - p * (aeval r) gp) * (p - 1)! =
((eval 0 f ^ p * cexp r) * (p - 1)! + ↑(p * (p - 1)!) * (eval 0 gp' * cexp r - (aeval r) gp)) :=
by push_cast; ring
rw [le_div_iff₀ (Nat.cast_pos.mpr (Nat.factorial_pos _) : (0 : ℝ) < _), ← norm_natCast, ← norm_mul, this,
Nat.mul_factorial_pred prime_p.ne_zero, mul_sub, ← h]
have :
↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
(↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
((p - 1)! • ↑(eval 0 (f ^ p)) + p ! • ↑(eval 0 gp') : ℤ) * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) :=
by simp; ring
rw [this, ← h', mul_comm, ← eq_intCast (algebraMap ℤ ℂ), ← aeval_algebraMap_apply_eq_algebraMap_eval, map_zero,
aeval_sumIDeriv_eq_eval, aeval_sumIDeriv_eq_eval, ← P]
refine (Pp'_le r p prime_p.ne_zero).trans (pow_le_pow_left₀ (c'0 r) ?_ _)
have aux : c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset := by
simpa only [Multiset.mem_toFinset] using Multiset.mem_map_of_mem _ hr
have h : ((f.aroots ℂ).map c').toFinset.Nonempty := ⟨c' r, aux⟩
simpa only [h, ↓reduceDIte] using Finset.le_max' _ _ aux
