Baker-Wüstholz theorem on linear forms in logarithms | Lean AI formalization leaderboard

Problem statement

Notes: Unavailable.

Source: A. Baker, G. Wüstholz, Logarithmic forms and group varieties, J. reine angew. Math. 442 (1993), 19-62.

Informal solution: Unavailable.

theorem declaration uses `sorry`bakerWustholz_linearForms_logs {n : ℕ} (hn : 0 < n)
    {K : Type*} [Field K] [NumberField K] (φ : K →+* ℂ)
    (α : Fin n → K) (hα : ∀ i, α i ≠ 0)
    (b : Fin n → ℤ) {B : ℕ} (hB : 2 ≤ B) (hbB : ∀ i, (b i).natAbs ≤ B)
    (hΛ_ne_zero : (∑ i, (b i : ℂ) * Complex.log (φ (α i))) ≠ 0) :
    Real.log ‖∑ i, (b i : ℂ) * Complex.log (φ (α i))‖
      ≥ -(BakerWustholz.C n (Module.finrank ℚ K)
          * max (Real.log B) (1 / (Module.finrank ℚ K : ℝ))
          * ∏ i, BakerWustholz.modifiedHeight φ (α i)) := byn:ℕhn:0 < nK:Type u_1inst✝¹:Field Kinst✝:NumberField Kφ:K →+* ℂα:Fin n → Khα:∀ (i : Fin n), α i ≠ 0b:Fin n → ℤB:ℕhB:2 ≤ BhbB:∀ (i : Fin n), (b i).natAbs ≤ BhΛ_ne_zero:∑ i, ↑(b i) * log (φ (α i)) ≠ 0⊢ Real.log ‖∑ i, ↑(b i) * log (φ (α i))‖ ≥
  -(BakerWustholz.C n (Module.finrank ℚ K) * max (Real.log ↑B) (1 / ↑(Module.finrank ℚ K)) *
      ∏ i, BakerWustholz.modifiedHeight φ (α i))
  sorryAll goals completed! 🐙