Height

Results named in Tau Ceti's TauCeti.NumberTheory.Height modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremEvertse's lower bound#

A nonzero algebraic number z ∈ ℂ of degree d satisfies den(z) ^ d * house(z) ^ (d - 1) * ‖z‖ ≥ 1.

TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm {z : ℂ} (hz : IsAlgebraic ℚ z)
  (hz0 : z ≠ 0) :
  1 ≤
    ↑(Algebra.natDenominator z) ^ (minpoly ℚ z).natDegree *
        TauCeti.house z ^ ((minpoly ℚ z).natDegree - 1) *
      ‖z‖
Lean

Formalized in Tau Ceti as TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm.

Other forms

Evertse's lower bound for the conjugates of an algebraic number. Formalized in Tau Ceti as TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm_of_mem_rootSet.

TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm_of_mem_rootSet.{u_1} {K : Type u_1}
  [Field K] [CharZero K] {z : K} {w : ℂ} (hz : IsAlgebraic ℚ z) (hz0 : z ≠ 0)
  (hw : w ∈ (minpoly ℚ z).rootSet ℂ) :
  1 ≤
    ↑(Algebra.natDenominator z) ^ (minpoly ℚ z).natDegree *
        TauCeti.house z ^ ((minpoly ℚ z).natDegree - 1) *
      ‖w‖
Sources
LeanTauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm · TauCeti.one_le_natDenominator_pow_mul_house_pow_mul_norm_of_mem_rootSet

TheoremLiouville's inequality in exponential form#

Let K be a number field of degree d, σ : K →+* ℂ, y ∈ K and m ≠ 0 an integer with m ^ N y an algebraic integer. If ‖σ y‖ ≤ exp A, ⌈y⌉ ≤ exp B and |m| ^ N ≤ exp C with C + A + (d - 1) (C + B) < 0, then y = 0.

NumberField.eq_zero_of_norm_le_exp_of_house_le_exp.{u_3} {K : Type u_3} [Field K] [NumberField K]
  (σ : K →+* ℂ) {y : K} {m : ℤ} (hm : m ≠ 0) {N : ℕ} (hint : IsIntegral ℤ (↑m ^ N * y)) {A B C : ℝ}
  (hσ : ‖σ y‖ ≤ Real.exp A) (hy : NumberField.house y ≤ Real.exp B) (hmC : |↑m| ^ N ≤ Real.exp C)
  (h : C + A + ↑(Module.finrank ℚ K - 1) * (C + B) < 0) : y = 0
Lean

Formalized in Tau Ceti as NumberField.eq_zero_of_norm_le_exp_of_house_le_exp.

Other forms

Liouville's inequality in a number field K of degree d. Formalized in Tau Ceti as NumberField.one_le_norm_mul_house_pow.

NumberField.one_le_norm_mul_house_pow.{u_3} {K : Type u_3} [Field K] [NumberField K] {x : K}
  (hx : IsIntegral ℤ x) (h0 : x ≠ 0) (σ : K →+* ℂ) :
  1 ≤ ‖σ x‖ * NumberField.house x ^ (Module.finrank ℚ K - 1)

Liouville's inequality for values of integer polynomials at a finite place. Formalized in Tau Ceti as IsDedekindDomain.HeightOneSpectrum.neg_log_valuation_aeval_mul_log_absNorm_le.

IsDedekindDomain.HeightOneSpectrum.neg_log_valuation_aeval_mul_log_absNorm_le.{u_1, u_2}
  {ι : Type u_1} [Fintype ι] {K : Type u_2} [Field K] [NumberField K]
  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) {P : MvPolynomial ι ℤ}
  {L : ι → ℕ} (hL : ∀ (i : ι), MvPolynomial.degreeOf i P ≤ L i) (x : ι → K) :
  -↑((IsDedekindDomain.HeightOneSpectrum.valuation K v) ((MvPolynomial.aeval x) P)).log *
      Real.log ↑(Ideal.absNorm v.asIdeal) ≤
    ↑(Module.finrank ℚ K) * Real.log (∑ s ∈ P.support, |↑(P.coeff s)|) +
      ∑ i, ↑(L i) * Height.logHeight₁ (x i)
Sources
LeanNumberField.eq_zero_of_norm_le_exp_of_house_le_exp · NumberField.one_le_norm_mul_house_pow · IsDedekindDomain.HeightOneSpectrum.neg_log_valuation_aeval_mul_log_absNorm_le
Uses 1 · Used by 2
Proof usesLiouville's inequality at a finite place
Used byLiouville's lower bound for Gelfond's values (Karatarakis–Wiedijk, §3) · The Gelfond–Schneider theorem for real numbers (Evertse, Theorem 4.21)

TheoremRoth's lemma in one variable, index form#

Let P ≠ 0 be placed in the coordinate i, with deg P ≤ r i. If r i * h(a i) ≥ s⁻¹ * (h(P) + [K : ℚ] * r i * log 2) for some s > 0, then the index of P at a with weights r is at most s. Heights are relative. Replacing log 2 by a larger constant, such as Pottmeyer's 4, only strengthens the hypothesis.

MvPolynomial.weightedIndex_toMvPolynomial_le.{u_1, u_2} {K : Type u_1} [Field K] [NumberField K]
  {σ : Type u_2} (r : σ → ℕ) (a : σ → K) (i : σ) {P : Polynomial K} (hP : P ≠ 0)
  (hr : P.natDegree ≤ r i) {s : ℝ} (hs : 0 < s)
  (h :
    s⁻¹ * (P.logHeight + ↑(Module.finrank ℚ K) * ↑(r i) * Real.log 2) ≤
      ↑(r i) * Height.logHeight₁ (a i)) :
  MvPolynomial.weightedIndex r a ((Polynomial.toMvPolynomial i) P) ≤ ENNReal.ofReal s
Lean

Formalized in Tau Ceti as MvPolynomial.weightedIndex_toMvPolynomial_le.

Other forms

Roth's lemma in one variable, multiplicity form. Formalized in Tau Ceti as Polynomial.rootMultiplicity_mul_logHeight₁_le.

Polynomial.rootMultiplicity_mul_logHeight₁_le.{u_1} {K : Type u_1} [Field K] [NumberField K]
  (P : Polynomial K) (β : K) :
  ↑(Polynomial.rootMultiplicity β P) * Height.logHeight₁ β ≤
    P.logHeight + ↑(Module.finrank ℚ K) * ↑P.natDegree * Real.log 2
Sources
LeanMvPolynomial.weightedIndex_toMvPolynomial_le · Polynomial.rootMultiplicity_mul_logHeight₁_le
Uses 1 · Used by 1
Statement usesMvPolynomial.weightedIndex
Used byRoth's lemma (Pottmeyer, Theorem 3.4.1)

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.