Diophantine approximation and transcendence

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremRoth's theorem (Roth, 1955)#

If α is a real algebraic number and κ > 2, then only finitely many rational numbers ξ satisfy |ξ - α| ≤ H(ξ) ^ (-κ), where H is the multiplicative height on ℚ.

IsAlgebraic.finite_setOfPred_abs_sub_le_mulHeight₁_rpow_neg {α : ℝ} (hα : IsAlgebraic ℚ α) {κ : ℝ}
  (hκ : 2 < κ) : {ξ | |↑ξ - α| ≤ Height.mulHeight₁ ξ ^ (-κ)}.Finite

Lean

Formalized in Tau Ceti as IsAlgebraic.finite_setOfPred_abs_sub_le_mulHeight₁_rpow_neg.

Other forms

Roth's theorem as a lower bound (Evertse, Theorem 6.2). Formalized in Tau Ceti as IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_abs_sub.

IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_abs_sub {α : ℝ} (hα : IsAlgebraic ℚ α) {κ : ℝ}
  (hκ : 2 < κ) : ∃ c, 0 < c ∧ ∀ (ξ : ℚ), ↑ξ ≠ α → c * Height.mulHeight₁ ξ ^ (-κ) ≤ |↑ξ - α|

Roth's theorem. Formalized in Tau Ceti as IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_norm_sub.

IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_norm_sub {α : ℂ} (hα : IsAlgebraic ℚ α) {κ : ℝ}
  (hκ : 2 < κ) : ∃ c, 0 < c ∧ ∀ (ξ : ℚ), ↑ξ ≠ α → c * Height.mulHeight₁ ξ ^ (-κ) ≤ ‖↑ξ - α‖

Roth's theorem in terms of Liouville exponents. Formalized in Tau Ceti as IsAlgebraic.not_liouvilleWith.

IsAlgebraic.not_liouvilleWith {α : ℝ} (hα : IsAlgebraic ℚ α) {p : ℝ} (hp : 2 < p) :
  ¬LiouvilleWith p α

Roth's theorem for a linear form. Formalized in Tau Ceti as IsAlgebraic.exists_pos_mul_max_abs_rpow_le_norm_sub_mul.

IsAlgebraic.exists_pos_mul_max_abs_rpow_le_norm_sub_mul {α : ℂ} (hα : IsAlgebraic ℚ α) {κ : ℝ}
  (hκ : 2 < κ) :
  ∃ c, 0 < c ∧ ∀ (x y : ℤ), ↑x - α * ↑y ≠ 0 → c * max |↑x| |↑y| ^ (1 - κ) ≤ ‖↑x - α * ↑y‖

Sources

• Tau Ceti documentation: IsAlgebraic.finite_setOfPred_abs_sub_le_mulHeight₁_rpow_neg
• Source of IsAlgebraic.finite_setOfPred_abs_sub_le_mulHeight₁_rpow_neg in TauCeti/NumberTheory/DiophantineApproximation/Roth/Theorem.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanIsAlgebraic.finite_setOfPred_abs_sub_le_mulHeight₁_rpow_neg · IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_abs_sub · IsAlgebraic.exists_pos_mul_mulHeight₁_rpow_neg_le_norm_sub · IsAlgebraic.not_liouvilleWith · IsAlgebraic.exists_pos_mul_max_abs_rpow_le_norm_sub_mul

Uses 3 · Used by 2

Proof usesMvPolynomial.weightedIndex · Roth's auxiliary polynomial (Pottmeyer, Theorem 2.6.5) · Roth's lemma (Pottmeyer, Theorem 3.4.1)

Used byIsAlgebraic.irrationalityExponent_eq_two · The Thue–Roth inequality for binary forms (Evertse, Theorem 6.3)

TheoremIsAlgebraic.irrationalityExponent_eq_two#

The irrationality exponent of a real algebraic irrational number is two.

IsAlgebraic.irrationalityExponent_eq_two {α : ℝ} (hα : IsAlgebraic ℚ α) (hirr : Irrational α) :
  TauCeti.irrationalityExponent α = 2

Lean

Formalized in Tau Ceti as IsAlgebraic.irrationalityExponent_eq_two.

Sources

• Tau Ceti documentation: IsAlgebraic.irrationalityExponent_eq_two
• Source of IsAlgebraic.irrationalityExponent_eq_two in TauCeti/NumberTheory/DiophantineApproximation/Roth/Theorem.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanIsAlgebraic.irrationalityExponent_eq_two

Uses 1

Proof usesRoth's theorem (Roth, 1955)

TheoremThe Lindemann–Weierstrass theorem, in Baker's form#

The exponentials of pairwise distinct algebraic numbers are linearly independent over the field integralClosure ℚ ℂ of algebraic numbers.

TauCeti.linearIndependent_exp.{u_1} {ι : Type u_1} (u : ι → ↥(integralClosure ℚ ℂ))
  (u_inj : Function.Injective u) :
  LinearIndependent ↥(integralClosure ℚ ℂ) fun i => Complex.exp ↑(u i)

Informally uses

• The Lindemann–Weierstrass theorem, algebraic independence form

Lean

Formalized in Tau Ceti as TauCeti.linearIndependent_exp.

Sources

• Tau Ceti documentation: TauCeti.linearIndependent_exp
• Source of TauCeti.linearIndependent_exp in TauCeti/NumberTheory/Transcendental/Lindemann/Theorem.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanTauCeti.linearIndependent_exp

Used by 1

Used byThe Lindemann–Weierstrass theorem, algebraic independence form

TheoremThe Lindemann–Weierstrass theorem, algebraic independence form#

If the algebraic numbers u i are linearly independent over ℕ (equivalently, over ℚ), then their exponentials are algebraically independent over the field integralClosure ℚ ℂ of algebraic numbers.

TauCeti.algebraicIndependent_exp.{u_1} {ι : Type u_1} (u : ι → ↥(integralClosure ℚ ℂ))
  (hu : LinearIndependent ℕ u) :
  AlgebraicIndependent ↥(integralClosure ℚ ℂ) fun i => Complex.exp ↑(u i)

Lean

Formalized in Tau Ceti as TauCeti.algebraicIndependent_exp.

Other forms

The Lindemann–Weierstrass theorem over a Galois number field. Formalized in Tau Ceti as TauCeti.LindemannWeierstrass.expEval_injective.

TauCeti.LindemannWeierstrass.expEval_injective.{u_1} {K : Type u_1} [Field K] [NumberField K]
  [IsGalois ℚ K] [Algebra K ℂ] : Function.Injective ⇑(TauCeti.LindemannWeierstrass.expEval K)

The Lindemann–Weierstrass theorem over a Galois number field, linear independence form. Formalized in Tau Ceti as TauCeti.LindemannWeierstrass.linearIndependent_exp_algebraMap.

TauCeti.LindemannWeierstrass.linearIndependent_exp_algebraMap.{u_1} {K : Type u_1} [Field K]
  [NumberField K] [IsGalois ℚ K] [Algebra K ℂ] :
  LinearIndependent K fun γ => Complex.exp ((algebraMap K ℂ) γ)

Sources

• Tau Ceti documentation: TauCeti.algebraicIndependent_exp
• Source of TauCeti.algebraicIndependent_exp in TauCeti/NumberTheory/Transcendental/Lindemann/Theorem.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanTauCeti.algebraicIndependent_exp · TauCeti.LindemannWeierstrass.expEval_injective · TauCeti.LindemannWeierstrass.linearIndependent_exp_algebraMap

Uses 2

Proof usesThe Lindemann–Weierstrass theorem, in Baker's form · The weak Lindemann–Weierstrass theorem

TheoremThe Thue–Roth inequality for binary forms (Evertse, Theorem 6.3)#

Let F ∈ ℤ[X₀, X₁] be a binary form of degree d with no squared linear factor over ℂ, and let κ > 2. Then there is c > 0 with |F(x, y)| ≥ c max(|x|, |y|) ^ (d - κ) for all integers x, y with F(x, y) ≠ 0. The proof is ineffective: it gives no value of c.

MvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval {F : MvPolynomial (Fin 2) ℤ}
  {d : ℕ} (hF : F.IsHomogeneous d)
  (hsq :
    ∀ (a b : ℂ),
      (a, b) ≠ (0, 0) →
        ¬(MvPolynomial.C a * MvPolynomial.X 0 + MvPolynomial.C b * MvPolynomial.X 1) ^ 2 ∣
            (MvPolynomial.map (Int.castRingHom ℂ)) F)
  {κ : ℝ} (hκ : 2 < κ) :
  ∃ c,
    0 < c ∧
      ∀ (x y : ℤ),
        (MvPolynomial.eval ![x, y]) F ≠ 0 →
          c * max |↑x| |↑y| ^ (↑d - κ) ≤ |↑((MvPolynomial.eval ![x, y]) F)|

Lean

Formalized in Tau Ceti as MvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval.

Sources

• Tau Ceti documentation: MvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval
• Source of MvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval in TauCeti/NumberTheory/DiophantineApproximation/Roth/BinaryForm.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanMvPolynomial.IsHomogeneous.exists_pos_mul_max_abs_rpow_le_abs_eval

Uses 2 · Used by 1

Proof usesCramer's rule bound · Roth's theorem (Roth, 1955)

Used byThe Thue inequality (Evertse, Corollary 6.4)

TheoremKronecker's approximation theorem#

If 1 and the real numbers αᵢ satisfy no nontrivial integer relation, that is, if they are linearly independent over ℚ, then for every θ ∈ ℝ^ι and ε > 0 there are infinitely many integer pairs (x, y), x ∈ ℤ^ι, y ∈ ℤ, with |y αᵢ - xᵢ - θᵢ| ≤ ε for every i.

TauCeti.kronecker_approximation.{u_1} {ι : Type u_1} [Fintype ι] {α : ι → ℝ}
  (hα : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i, ↑(x.2 i) * α i = 0 → x = 0) (θ : ι → ℝ) {ε : ℝ}
  (hε : 0 < ε) : {p | ∀ (i : ι), |α i * ↑p.2 - ↑(p.1 i) - θ i| ≤ ε}.Infinite

Lean

Formalized in Tau Ceti as TauCeti.kronecker_approximation.

Other forms

Kronecker's approximation theorem with positive multipliers. Formalized in Tau Ceti as TauCeti.kronecker_approximation_nat.

TauCeti.kronecker_approximation_nat.{u_1} {ι : Type u_1} [Fintype ι] {α : ι → ℝ}
  (hα : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i, ↑(x.2 i) * α i = 0 → x = 0) (θ : ι → ℝ) {ε : ℝ}
  (hε : 0 < ε) : {n | ∃ x, ∀ (i : ι), |α i * ↑n - ↑(x i) - θ i| ≤ ε}.Infinite

Sources

• Tau Ceti documentation: TauCeti.kronecker_approximation
• Source of TauCeti.kronecker_approximation in TauCeti/NumberTheory/DiophantineApproximation/Kronecker.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanTauCeti.kronecker_approximation · TauCeti.kronecker_approximation_nat

Uses 1

Proof usesKronecker's theorem, density form

TheoremThe one-factor estimate#

Let K be a nonarchimedean local field of characteristic zero, that is, a finite extension of ℚ_[p]. For every fixed α ∈ K there is a constant C, depending on α and K, such that

v_K(α ^ b - 1) ≤ C (1 + log max(1, |b|)) for every integer b with α ^ b ≠ 1.

TauCeti.exists_log_normalizedValuationWithZero_zpow_sub_one_le.{u_1} {K : Type u_1} [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [CharZero K] (α : K) :
  ∃ C,
    ∀ (b : ℤ),
      α ^ b ≠ 1 →
        ↑((TauCeti.normalizedValuationWithZero K) (α ^ b - 1)).log ≤ C * (1 + Real.log (max 1 |↑b|))

Lean

Formalized in Tau Ceti as TauCeti.exists_log_normalizedValuationWithZero_zpow_sub_one_le.

Sources

• Tau Ceti documentation: TauCeti.exists_log_normalizedValuationWithZero_zpow_sub_one_le
• Source of TauCeti.exists_log_normalizedValuationWithZero_zpow_sub_one_le in TauCeti/NumberTheory/LocalField/UnitFiltration/Pow/SubOne.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanTauCeti.exists_log_normalizedValuationWithZero_zpow_sub_one_le

Uses 1

Proof usesThe one-factor estimate, explicit form

TheoremThe one-factor estimate, explicit form#

Let x ∈ Kˣ have a power x ^ M ≠ 1 in a positive-depth step U(K,i), and let b be an integer with (|b| : K) ≠ 0 such that v_K(ℓ) < (ℓ - 1) * i for every prime ℓ ∣ b. Then

v_K(x ^ b - 1) ≤ v_K(x ^ M - 1) + v_K(|b|).

TauCeti.log_normalizedValuationWithZero_zpow_sub_one_le.{u_1} {K : Type u_1} [Field K]
  [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {x : Kˣ} {M i : ℕ}
  (hi0 : i ≠ 0) (hM : x ^ M ∈ TauCeti.unitFiltration K i) (hM1 : x ^ M ≠ 1) {b : ℤ}
  (hb : ↑b.natAbs ≠ 0)
  (hi :
    ∀ (ℓ : ℕ),
      Nat.Prime ℓ →
        ∀ (hℓK : ↑ℓ ≠ 0), ℓ ∣ b.natAbs → TauCeti.natCastValuation K ℓ hℓK < (ℓ - 1) * i) :
  ((TauCeti.normalizedValuationWithZero K) (↑x ^ b - 1)).log ≤
    ((TauCeti.normalizedValuationWithZero K) (↑x ^ M - 1)).log +
      ↑(TauCeti.natCastValuation K b.natAbs hb)

Lean

Formalized in Tau Ceti as TauCeti.log_normalizedValuationWithZero_zpow_sub_one_le.

Sources

• Tau Ceti documentation: TauCeti.log_normalizedValuationWithZero_zpow_sub_one_le
• Source of TauCeti.log_normalizedValuationWithZero_zpow_sub_one_le in TauCeti/NumberTheory/LocalField/UnitFiltration/Pow/SubOne.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanTauCeti.log_normalizedValuationWithZero_zpow_sub_one_le

Used by 1

Used byThe one-factor estimate

DefinitionTauCeti.mahlerMeasure#

The Mahler measure M(x) of x: the Mahler measure of its primitive minimal polynomial F_x, mapped to ℂ[X]. For algebraic x this is a₀ ∏ max(1, |x⁽ⁱ⁾|) over the complex conjugates of x (mahlerMeasure_eq_leadingCoeff_mul_prod); for transcendental x it is 1.

TauCeti.mahlerMeasure.{u_1} {F : Type u_1} [Field F] [CharZero F] (x : F) : ℝ

Lean

Formalized in Tau Ceti as TauCeti.mahlerMeasure.

Sources

• Tau Ceti documentation: TauCeti.mahlerMeasure
• Source of TauCeti.mahlerMeasure in TauCeti/NumberTheory/Height/MahlerMeasure.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanTauCeti.mahlerMeasure

Used by 2

Used byNorthcott's theorem for the naive height, with Evertse's count · Kronecker's theorem for projective tuples

DefinitionMvPolynomial.weightedIndex#

The weighted index is the least reciprocal-weighted order of a nonzero Hasse jet; the infimum of the empty set is ⊤.

MvPolynomial.weightedIndex.{u_1, u_2} {σ : Type u_1} {R : Type u_2} [CommSemiring R] (r : σ → ℕ)
  (a : σ → R) (P : MvPolynomial σ R) : ENNReal

Lean

Formalized in Tau Ceti as MvPolynomial.weightedIndex.

Sources

• Tau Ceti documentation: MvPolynomial.weightedIndex
• Source of MvPolynomial.weightedIndex in TauCeti/RingTheory/MvPolynomial/WeightedIndex.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanMvPolynomial.weightedIndex

Used by 4

Used byRoth's auxiliary polynomial (Pottmeyer, Theorem 2.6.5) · Roth's lemma (Pottmeyer, Theorem 3.4.1) · Roth's theorem (Roth, 1955) · Roth's lemma in one variable, index form

DefinitionThe structure of the rational S-units#

If S consists of primes, the map x ↦ (sign x, (v_p(x))_{p ∈ S}) is an isomorphism from the rational S-units to ℤˣ × Multiplicative (S → ℤ); its inverse sends (ε, z) to ε ∏_{p ∈ S} p ^ z_p (TauCeti.coe_sUnitsRatMulEquiv_symm_apply).

TauCeti.sUnitsRatMulEquiv {S : Finset ℕ} (hS : ∀ p ∈ S, Nat.Prime p) :
  ↥({v | ↑(Rat.HeightOneSpectrum.primesEquiv v) ∈ S}.unit ℚ) ≃* ℤˣ × Multiplicative (↥S → ℤ)

Lean

Formalized in Tau Ceti as TauCeti.sUnitsRatMulEquiv.

Sources

• Tau Ceti documentation: TauCeti.sUnitsRatMulEquiv
• Source of TauCeti.sUnitsRatMulEquiv in TauCeti/NumberTheory/NumberField/SUnits/Rat/Structure.lean
• Tau Ceti roadmap status: Diophantine approximation and transcendence

LeanTauCeti.sUnitsRatMulEquiv

TheoremHermite's estimate#

if C bounds ‖f‖ on the closed disc of radius ‖z‖, then ‖F_f(z)‖ ≤ ‖z‖ exp ‖z‖ C.

Polynomial.norm_hermiteIntegral_le {f : Polynomial ℂ} {z : ℂ} {C : ℝ}
  (hC : ∀ (u : ℂ), ‖u‖ ≤ ‖z‖ → ‖Polynomial.eval u f‖ ≤ C) :
  ‖f.hermiteIntegral z‖ ≤ ‖z‖ * Real.exp ‖z‖ * C

Lean

Formalized in Tau Ceti as Polynomial.norm_hermiteIntegral_le.

Sources

• Tau Ceti documentation: Polynomial.norm_hermiteIntegral_le
• Source of Polynomial.norm_hermiteIntegral_le in TauCeti/NumberTheory/Transcendental/Lindemann/HermiteIntegral.lean

LeanPolynomial.norm_hermiteIntegral_le

Used by 1

Used byThe weak Lindemann–Weierstrass theorem

TheoremHermite's identity#

integration by parts evaluates Hermite's integral as F_f(z) = exp z * (sumIDeriv f)(0) - (sumIDeriv f)(z).

Polynomial.hermiteIntegral_eq_sumIDeriv (f : Polynomial ℂ) (z : ℂ) :
  f.hermiteIntegral z =
    Complex.exp z * Polynomial.eval 0 (Polynomial.sumIDeriv f) -
      Polynomial.eval z (Polynomial.sumIDeriv f)

Lean

Formalized in Tau Ceti as Polynomial.hermiteIntegral_eq_sumIDeriv.

Sources

• Tau Ceti documentation: Polynomial.hermiteIntegral_eq_sumIDeriv
• Source of Polynomial.hermiteIntegral_eq_sumIDeriv in TauCeti/NumberTheory/Transcendental/Lindemann/HermiteIntegral.lean

LeanPolynomial.hermiteIntegral_eq_sumIDeriv

Used by 1

Used byThe weak Lindemann–Weierstrass theorem

TheoremKronecker's theorem, density form#

If 1 and the real numbers αᵢ satisfy no nontrivial integer relation, that is, if they are linearly independent over ℚ, then the points (y αᵢ - xᵢ)ᵢ, for y ∈ ℤ and x ∈ ℤ^ι, are dense in ℝ^ι.

TauCeti.denseRange_mul_sub_intCast.{u_1} {ι : Type u_1} [Fintype ι] {α : ι → ℝ}
  (hα : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i, ↑(x.2 i) * α i = 0 → x = 0) :
  DenseRange fun p i => α i * ↑p.2 - ↑(p.1 i)

Lean

Formalized in Tau Ceti as TauCeti.denseRange_mul_sub_intCast.

Sources

• Tau Ceti documentation: TauCeti.denseRange_mul_sub_intCast
• Source of TauCeti.denseRange_mul_sub_intCast in TauCeti/NumberTheory/DiophantineApproximation/Kronecker.lean

LeanTauCeti.denseRange_mul_sub_intCast

Used by 1

Used byKronecker's approximation theorem

TheoremRoth's auxiliary polynomial (Pottmeyer, Theorem 2.6.5)#

Let α be an algebraic number of degree d in a field of characteristic zero, and let b ≥ 1 be an integer such that b α is integral over ℤ. Let ε ≥ 0 and let ι be a finite set of n variables with 2 d ≤ exp (ε² n / 2). For all positive integers rᵢ, i ∈ ι, there is a nonzero P ∈ ℤ[Xᵢ : i ∈ ι] with deg_{Xᵢ} P ≤ rᵢ, whose index at (α, …, α) with weights r is at least (n / 2) (1 - ε), and whose coefficients have absolute value at most (12 b max(1, ⌈α⌉)) ^ (∑ᵢ rᵢ), where ⌈α⌉ is the house of α.

TauCeti.exists_roth_auxiliary_polynomial.{u_2, u_3} {ι : Type u_2} [Fintype ι] {F : Type u_3}
  [Field F] [CharZero F] {α : F} {b : ℕ} (hb : 0 < b) (hbα : IsIntegral ℤ (↑b * α)) {ε : ℝ}
  (hε : 0 ≤ ε) (hn : 2 * ↑(minpoly ℚ α).natDegree ≤ Real.exp (ε ^ 2 * ↑(Fintype.card ι) / 2))
  {r : ι → ℕ} (hr : ∀ (i : ι), r i ≠ 0) :
  ∃ P,
    P ≠ 0 ∧
      (∀ (i : ι), MvPolynomial.degreeOf i P ≤ r i) ∧
        ENNReal.ofReal (↑(Fintype.card ι) / 2 * (1 - ε)) ≤
            MvPolynomial.weightedIndex r (fun x => α) ((MvPolynomial.map (Int.castRingHom F)) P) ∧
          ∀ (m : ι →₀ ℕ), |↑(P.coeff m)| ≤ (12 * ↑b * max 1 (TauCeti.house α)) ^ ∑ i, r i

Lean

Formalized in Tau Ceti as TauCeti.exists_roth_auxiliary_polynomial.

Sources

• Tau Ceti documentation: TauCeti.exists_roth_auxiliary_polynomial
• Source of TauCeti.exists_roth_auxiliary_polynomial in TauCeti/NumberTheory/DiophantineApproximation/Roth/Auxiliary.lean

LeanTauCeti.exists_roth_auxiliary_polynomial

Uses 3 · Used by 1

Statement usesMvPolynomial.weightedIndex

Proof usesHoeffding's lemma on the grid {0, 1 / r, …, 1} · Siegel's lemma over a number field, with rational integer unknowns (Evertse, Theorem 3.20)

Used byRoth's theorem (Roth, 1955)

TheoremRoth's lemma (Pottmeyer, Theorem 3.4.1)#

Let P ≠ 0 be a polynomial in n ≥ 1 variables over a number field K, with partial degrees deg_{Xᵢ} P ≤ rᵢ for positive weights rᵢ satisfying rᵢ₊₁ ≤ σ rᵢ, where 0 < σ ≤ 1 / 2. If σ⁻¹ (h(P) + 4 n r₀ [K : ℚ]) ≤ rᵢ h(βᵢ) for every i, then the index of P at β with weights r is at most 2 n σ ^ (1 / 2 ^ (n - 1)). Heights are relative logarithmic heights.

TauCeti.weightedIndex_le_of_logHeight_le.{u_1} {K : Type u_1} [Field K] [NumberField K] {n : ℕ}
  [NeZero n] {P : MvPolynomial (Fin n) K} (hP : P ≠ 0) {r : Fin n → ℕ} (hr : ∀ (i : Fin n), 0 < r i)
  (hdeg : ∀ (i : Fin n), MvPolynomial.degreeOf i P ≤ r i) {σ : ℝ} (hσ₀ : 0 < σ) (hσ : σ ≤ 1 / 2)
  (hratio : ∀ (i j : Fin n), ↑j = ↑i + 1 → ↑(r j) ≤ σ * ↑(r i)) (β : Fin n → K)
  (hβ :
    ∀ (i : Fin n),
      σ⁻¹ * (P.logHeight + 4 * ↑n * ↑(r 0) * ↑(Module.finrank ℚ K)) ≤
        ↑(r i) * Height.logHeight₁ (β i)) :
  MvPolynomial.weightedIndex r β P ≤ ENNReal.ofReal (2 * ↑n * σ ^ (1 / 2 ^ (n - 1)))

Lean

Formalized in Tau Ceti as TauCeti.weightedIndex_le_of_logHeight_le.

Sources

• Tau Ceti documentation: TauCeti.weightedIndex_le_of_logHeight_le
• Source of TauCeti.weightedIndex_le_of_logHeight_le in TauCeti/NumberTheory/DiophantineApproximation/Roth/IndexEstimate.lean

LeanTauCeti.weightedIndex_le_of_logHeight_le

Uses 2 · Used by 1

Statement usesMvPolynomial.weightedIndex

Proof usesRoth's lemma in one variable, index form

Used byRoth's theorem (Roth, 1955)

TheoremThe Thue inequality (Evertse, Corollary 6.4)#

Let F ∈ ℤ[X₀, X₁] be a binary form such that F(X, 1) has at least three distinct complex zeros. Then for every bound B, the inequality 0 < |F(x, y)| ≤ B has only finitely many integer solutions. Like Roth's theorem, the proof is ineffective.

MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le_of_three_le_card_roots
  {F : MvPolynomial (Fin 2) ℤ} {d : ℕ} (hF : F.IsHomogeneous d)
  (hroots :
    3 ≤
      (Polynomial.map (Int.castRingHom ℂ)
              ((MvPolynomial.aeval ![Polynomial.X, 1]) F)).roots.toFinset.card)
  (B : ℤ) :
  {p | (MvPolynomial.eval ![p.1, p.2]) F ≠ 0 ∧ |(MvPolynomial.eval ![p.1, p.2]) F| ≤ B}.Finite

Lean

Formalized in Tau Ceti as MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le_of_three_le_card_roots.

Other forms

The Thue inequality for square-free binary forms (Evertse, Corollary 6.4, square-free case). Formalized in Tau Ceti as MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le.

MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le {F : MvPolynomial (Fin 2) ℤ} {d : ℕ}
  (hF : F.IsHomogeneous d)
  (hsq :
    ∀ (a b : ℂ),
      (a, b) ≠ (0, 0) →
        ¬(MvPolynomial.C a * MvPolynomial.X 0 + MvPolynomial.C b * MvPolynomial.X 1) ^ 2 ∣
            (MvPolynomial.map (Int.castRingHom ℂ)) F)
  (hd : 3 ≤ d) (B : ℤ) :
  {p | (MvPolynomial.eval ![p.1, p.2]) F ≠ 0 ∧ |(MvPolynomial.eval ![p.1, p.2]) F| ≤ B}.Finite

Sources

• Tau Ceti documentation: MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le_of_three_le_card_roots
• Source of MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le_of_three_le_card_roots in TauCeti/NumberTheory/DiophantineApproximation/Roth/BinaryForm.lean

LeanMvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le_of_three_le_card_roots · MvPolynomial.IsHomogeneous.finite_setOf_eval_ne_zero_and_abs_le

Uses 1 · Used by 1

Proof usesThe Thue–Roth inequality for binary forms (Evertse, Theorem 6.3)

Used byThue's theorem (Thue 1909; Evertse, Corollary 6.4)

TheoremThue's theorem (Thue 1909; Evertse, Corollary 6.4)#

Let F ∈ ℤ[X₀, X₁] be a binary form such that F(X, 1) has at least three distinct complex zeros, and let m ≠ 0. Then the Thue equation F(x, y) = m has only finitely many integer solutions. Like Roth's theorem, the proof is ineffective.

MvPolynomial.IsHomogeneous.finite_setOf_eval_eq_of_three_le_card_roots {F : MvPolynomial (Fin 2) ℤ}
  {d : ℕ} (hF : F.IsHomogeneous d)
  (hroots :
    3 ≤
      (Polynomial.map (Int.castRingHom ℂ)
              ((MvPolynomial.aeval ![Polynomial.X, 1]) F)).roots.toFinset.card)
  {m : ℤ} (hm : m ≠ 0) : {p | (MvPolynomial.eval ![p.1, p.2]) F = m}.Finite

Lean

Formalized in Tau Ceti as MvPolynomial.IsHomogeneous.finite_setOf_eval_eq_of_three_le_card_roots.

Other forms

Thue's theorem for square-free binary forms (Evertse, Corollary 6.4, square-free case). Formalized in Tau Ceti as MvPolynomial.IsHomogeneous.finite_setOf_eval_eq.

MvPolynomial.IsHomogeneous.finite_setOf_eval_eq {F : MvPolynomial (Fin 2) ℤ} {d : ℕ}
  (hF : F.IsHomogeneous d)
  (hsq :
    ∀ (a b : ℂ),
      (a, b) ≠ (0, 0) →
        ¬(MvPolynomial.C a * MvPolynomial.X 0 + MvPolynomial.C b * MvPolynomial.X 1) ^ 2 ∣
            (MvPolynomial.map (Int.castRingHom ℂ)) F)
  (hd : 3 ≤ d) {m : ℤ} (hm : m ≠ 0) : {p | (MvPolynomial.eval ![p.1, p.2]) F = m}.Finite

Sources

• Tau Ceti documentation: MvPolynomial.IsHomogeneous.finite_setOf_eval_eq_of_three_le_card_roots
• Source of MvPolynomial.IsHomogeneous.finite_setOf_eval_eq_of_three_le_card_roots in TauCeti/NumberTheory/DiophantineApproximation/Roth/BinaryForm.lean

LeanMvPolynomial.IsHomogeneous.finite_setOf_eval_eq_of_three_le_card_roots · MvPolynomial.IsHomogeneous.finite_setOf_eval_eq

Uses 1

Proof usesThe Thue inequality (Evertse, Corollary 6.4)

TheoremThe weak Lindemann–Weierstrass theorem#

Let K be a number field, Galois over ℚ and embedded in ℂ. If a nonzero formal exponential sum x = ∑ δ_γ [γ] ∈ K[K] is fixed by the conjugation galConj τ for every τ ∈ Gal(K/ℚ), then ∑ δ_γ exp γ ≠ 0.

TauCeti.LindemannWeierstrass.expEval_ne_zero_of_forall_galConj_eq.{u_1} {K : Type u_1} [Field K]
  [NumberField K] [IsGalois ℚ K] [Algebra K ℂ] {x : AddMonoidAlgebra K K} (hx : x ≠ 0)
  (hfix : ∀ (τ : Gal(K/ℚ)), (TauCeti.LindemannWeierstrass.galConj τ) x = x) :
  (TauCeti.LindemannWeierstrass.expEval K) x ≠ 0

Lean

Formalized in Tau Ceti as TauCeti.LindemannWeierstrass.expEval_ne_zero_of_forall_galConj_eq.

Sources

• Tau Ceti documentation: TauCeti.LindemannWeierstrass.expEval_ne_zero_of_forall_galConj_eq
• Source of TauCeti.LindemannWeierstrass.expEval_ne_zero_of_forall_galConj_eq in TauCeti/NumberTheory/Transcendental/Lindemann/Galois.lean

LeanTauCeti.LindemannWeierstrass.expEval_ne_zero_of_forall_galConj_eq

Uses 2 · Used by 1

Proof usesHermite's estimate · Hermite's identity

Used byThe Lindemann–Weierstrass theorem, algebraic independence form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.