Baker–Wüstholz theorem

2 fully proved1 ready to prove

Baker Wustholz

DefinitionThe Baker–Wüstholz constant#✓fully proved

For natural numbers \(n\) and \(d\), the Baker–Wüstholz constant is the real number \(C(n, d) = 18 \cdot (n + 1)! \cdot n^{n+1} \cdot (32 d)^{n+2} \cdot \log(2nd)\).

noncomputable def C (n d : ℕ) : ℝ :=
  18 * (n + 1).factorial * (n : ℝ) ^ (n + 1) *
    (32 * (d : ℝ)) ^ (n + 2) * Real.log (2 * n * d)

Used by 1

Used byBaker–Wüstholz theorem on linear forms in logarithms

DefinitionModified height#✓fully proved

Let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\) and let \(\varphi : K \to \mathbb{C}\) be a ring homomorphism. For \(\alpha \in K\), the modified height of \(\alpha\) with respect to \(\varphi\) is

\[h'(\alpha) = \max\left(h(\alpha), \frac{|\log \varphi(\alpha)|}{d}, \frac{1}{d}\right),\]

where \(\log\) is the principal branch of the complex logarithm (with \(\log 0 = 0\)) and \(h(\alpha)\) is the absolute logarithmic Weil height of \(\alpha\): \(\frac{1}{d}\) times the sum of \(\log \max(1, |\alpha|_v)\) over the places \(v\) of \(K\), with the absolute values normalized so that the product formula holds and each complex place counted twice.

noncomputable def modifiedHeight
    {K : Type*} [Field K] [NumberField K] (φ : K →+* ℂ) (α : K) : ℝ :=
  let d : ℝ := Module.finrank ℚ K
  max (Height.logHeight₁ α / d) (max (‖Complex.log (φ α)‖ / d) (1 / d))

Used by 1

Used byBaker–Wüstholz theorem on linear forms in logarithms

Baker–Wüstholz theorem

TheoremBaker–Wüstholz theorem on linear forms in logarithms#●ready to prove

Let \(n \ge 1\), let \(K\) be a number field of degree \(d = [K : \mathbb{Q}]\), let \(\varphi : K \to \mathbb{C}\) be a ring homomorphism, and let \(\alpha_1, \dots, \alpha_n\) be nonzero elements of \(K\). Let \(b_1, \dots, b_n\) be integers and let \(B \ge 2\) be a natural number with \(|b_i| \le B\) for every \(i\). With \(\log\) the principal branch of the complex logarithm, suppose that \(\Lambda = \sum_{i=1}^n b_i \log \varphi(\alpha_i)\) is nonzero. Then

\[\log |\Lambda| \ge -C(n, d) \max\left(\log B, \frac{1}{d}\right) \prod_{i=1}^n h'(\alpha_i),\]

where \(C(n, d)\) is the Baker–Wüstholz constant and \(h'\) is the modified height with respect to \(\varphi\).

public theorem_wanted 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))

noncomputable def C (n d : ℕ) : ℝ :=
  18 * (n + 1).factorial * (n : ℝ) ^ (n + 1) *
    (32 * (d : ℝ)) ^ (n + 2) * Real.log (2 * n * d)

WantedExt/NumberTheory/BakerWustholzWanted.lean:76

noncomputable def modifiedHeight
    {K : Type*} [Field K] [NumberField K] (φ : K →+* ℂ) (α : K) : ℝ :=
  let d : ℝ := Module.finrank ℚ K
  max (Height.logHeight₁ α / d) (max (‖Complex.log (φ α)‖ / d) (1 / d))

WantedExt/NumberTheory/BakerWustholzWanted.lean:82

Sources

A. Baker, G. Wüstholz, Logarithmic forms and group varieties, J. reine angew. Math. 442 (1993), 19-62. Problem bakerWustholz_linearForms_logs of the lean-eval benchmark.

Uses 2

Statement usesThe Baker–Wüstholz constant · Modified height

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.