Diophantine Approximation
Results named in Tau Ceti's TauCeti.NumberTheory.DiophantineApproximation modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.
TheoremDirichlet's lower bound for Mahler's exponent#
If ξ is not algebraic of degree at
most n, then w_n(ξ) ≥ n.
TauCeti.natCast_le_mahlerExponent {n : ℕ} {ξ : ℝ}
(hξ : ¬(IsAlgebraic ℚ ξ ∧ (minpoly ℚ ξ).natDegree ≤ n)) : ↑n ≤ TauCeti.mahlerExponent n ξ
Lean
Formalized in Tau Ceti as TauCeti.natCast_le_mahlerExponent.
Other forms
Dirichlet's lower bound for the linear-form exponent. Formalized in Tau Ceti as TauCeti.card_le_linearFormExponent.
TauCeti.card_le_linearFormExponent.{u_1} {ι : Type u_1} [Fintype ι] {θ : ι → ℝ}
(hθ : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i, ↑(x.2 i) * θ i = 0 → x = 0) :
↑(Fintype.card ι) ≤ TauCeti.linearFormExponent θ
Dirichlet's lower bound for the simultaneous exponent. Formalized in Tau Ceti as TauCeti.inv_card_le_simultaneousExponent.
TauCeti.inv_card_le_simultaneousExponent.{u_1} {ι : Type u_1} [Fintype ι] (θ : ι → ℝ) :
(↑(Fintype.card ι))⁻¹ ≤ TauCeti.simultaneousExponent θ
Sources
Uses 1
TheoremDirichlet's theorem, nearest-integer form#
For every real α, infinitely many natural
numbers q ≥ 1 satisfy q ‖q α‖ ≤ 1.
Real.infinite_setOf_mul_abs_mul_sub_round_le_one (α : ℝ) :
{q | 0 < q ∧ ↑q * |↑q * α - ↑(round (↑q * α))| ≤ 1}.Infinite
Lean
Formalized in Tau Ceti as Real.infinite_setOf_mul_abs_mul_sub_round_le_one.
Other forms
Dirichlet's theorem for linear forms, with general bounds. Formalized in Tau Ceti as Matrix.exists_int_abs_sum_mul_sub_le.
Matrix.exists_int_abs_sum_mul_sub_le.{u_1, u_2} {ι : Type u_1} {κ : Type u_2} [Fintype ι]
[Fintype κ] [Nonempty κ] (A : Matrix ι κ ℝ) {P δ : ℝ} (hP : 0 ≤ P) (hδ₀ : 0 ≤ δ) (hδ₁ : δ < 1)
(h : 1 ≤ P ^ Fintype.card κ * δ ^ Fintype.card ι) :
∃ y x, y ≠ 0 ∧ (∀ (j : κ), |↑(y j)| ≤ P) ∧ ∀ (i : ι), |∑ j, A i j * ↑(y j) - ↑(x i)| ≤ δ
Dirichlet's theorem for one linear form, infinitely many solutions. Formalized in Tau Ceti as TauCeti.dirichlet_linearForm_infinite.
TauCeti.dirichlet_linearForm_infinite.{u_2} {κ : Type u_2} [Fintype κ] [Nonempty κ] (α : κ → ℝ)
(hα : ∀ (y : κ → ℤ), (∃ k, ∑ j, α j * ↑(y j) = ↑k) → y = 0) :
{p | p.2 ≠ 0 ∧ |∑ j, α j * ↑(p.2 j) - ↑p.1| ≤ ‖p.2‖ ^ (-↑(Fintype.card κ))}.Infinite
Dirichlet's theorem for one linear form, infinitely many solutions. Formalized in Tau Ceti as TauCeti.infinite_linearFormApproximations_of_lt_card.
TauCeti.infinite_linearFormApproximations_of_lt_card.{u_1} {ι : Type u_1} [Fintype ι] [Nonempty ι]
{θ : ι → ℝ} (hθ : ∀ (x : ℤ × (ι → ℤ)), ↑x.1 + ∑ i, ↑(x.2 i) * θ i = 0 → x = 0) {w : ℝ}
(hw : w < ↑(Fintype.card ι)) : (TauCeti.linearFormApproximations θ w).Infinite
Dirichlet's theorem for systems of linear forms. Formalized in Tau Ceti as Matrix.dirichlet_linearForms.
Matrix.dirichlet_linearForms.{u_1, u_2} {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ]
[Nonempty ι] [Nonempty κ] (A : Matrix ι κ ℝ) {Q : ℝ} (hQ : 1 < Q) :
∃ y x,
y ≠ 0 ∧
(∀ (j : κ), |↑(y j)| ≤ Q) ∧
∀ (i : ι), |∑ j, A i j * ↑(y j) - ↑(x i)| ≤ Q ^ (-↑(Fintype.card κ) / ↑(Fintype.card ι))
Dirichlet's theorem for systems of linear forms, infinitely many solutions. Formalized in Tau Ceti as Matrix.dirichlet_linearForms_infinite.
Matrix.dirichlet_linearForms_infinite.{u_1, u_2} {ι : Type u_1} {κ : Type u_2} [Fintype ι]
[Fintype κ] [Nonempty κ] (A : Matrix ι κ ℝ)
(hA : ∀ (y : κ → ℤ), (∀ (i : ι), ∃ k, ∑ j, A i j * ↑(y j) = ↑k) → y = 0) :
{p |
p.1 ≠ 0 ∧
∀ (i : ι),
|∑ j, A i j * ↑(p.1 j) - ↑(p.2 i)| ≤
‖p.1‖ ^ (-↑(Fintype.card κ) / ↑(Fintype.card ι))}.Infinite
Dirichlet's theorem, infinitely many denominators. Formalized in Tau Ceti as TauCeti.infinite_simultaneousApproximationDenominators_inv_card.
TauCeti.infinite_simultaneousApproximationDenominators_inv_card.{u_1} {ι : Type u_1} [Fintype ι]
(θ : ι → ℝ) : (TauCeti.simultaneousApproximationDenominators θ (↑(Fintype.card ι))⁻¹).Infinite
Sources
Uses 1 · Used by 1
TheoremLiouville's bound for Mahler's exponent#
If ξ is a real algebraic number of degree D
over ℚ, then wₙ(ξ) ≤ D - 1 for every n.
IsAlgebraic.mahlerExponent_le {ξ : ℝ} (hξ : IsAlgebraic ℚ ξ) (n : ℕ) :
TauCeti.mahlerExponent n ξ ≤ ↑((minpoly ℚ ξ).natDegree - 1)
Uses 1
TheoremLiouville's inequality#
Let f ∈ ℤ[X] have degree d and a complex root α. Every
rational number ξ with f(ξ) ≠ 0 satisfies |ξ - α| ≥ (2 ^ (d - 1) M(f) H(ξ) ^ d)⁻¹, where
M(f) is the Mahler measure of f and H(ξ) the height of ξ.
Polynomial.inv_le_norm_ratCast_sub (f : Polynomial ℤ) {α : ℂ}
(hα : (Polynomial.map (Int.castRingHom ℂ) f).IsRoot α) {ξ : ℚ} (hξ : (Polynomial.aeval ξ) f ≠ 0) :
(2 ^ (f.natDegree - 1) * (Polynomial.map (Int.castRingHom ℂ) f).mahlerMeasure *
Height.mulHeight₁ ξ ^ f.natDegree)⁻¹ ≤
‖↑ξ - α‖
Lean
Formalized in Tau Ceti as Polynomial.inv_le_norm_ratCast_sub.
Other forms
Liouville's inequality for an algebraic number. Formalized in Tau Ceti as IsAlgebraic.inv_le_norm_ratCast_sub.
IsAlgebraic.inv_le_norm_ratCast_sub {α : ℂ} (hα : IsAlgebraic ℚ α) {ξ : ℚ} (hξ : ↑ξ ≠ α) :
(2 ^ ((minpoly ℚ α).natDegree - 1) *
(Polynomial.map (Int.castRingHom ℂ) (TauCeti.primitiveMinpoly α)).mahlerMeasure *
Height.mulHeight₁ ξ ^ (minpoly ℚ α).natDegree)⁻¹ ≤
‖↑ξ - α‖
Liouville's inequality for the value of an integer polynomial. Formalized in Tau Ceti as IsAlgebraic.exists_pos_le_norm_aeval_mul_supNorm_pow.
IsAlgebraic.exists_pos_le_norm_aeval_mul_supNorm_pow {ξ : ℂ} (hξ : IsAlgebraic ℚ ξ) (n : ℕ) :
∃ c > 0,
∀ (P : Polynomial ℤ),
P.natDegree ≤ n →
(Polynomial.aeval ξ) P ≠ 0 →
c ≤ ‖(Polynomial.aeval ξ) P‖ * P.supNorm ^ ((minpoly ℚ ξ).natDegree - 1)
Sources
Used by 1
TheoremLiouville's theorem in degree two#
An irrational root of a nonzero integer polynomial of
degree at most 2 is badly approximable.
Irrational.badlyApproximable_of_aeval_eq_zero {ξ : ℝ} (hξ : Irrational ξ) {f : Polynomial ℤ}
(hf : f ≠ 0) (hdeg : f.natDegree ≤ 2) (hroot : (Polynomial.aeval ξ) f = 0) :
TauCeti.BadlyApproximable ξ
Lean
Formalized in Tau Ceti as Irrational.badlyApproximable_of_aeval_eq_zero.
Other forms
Liouville's theorem in degree two. Formalized in Tau Ceti as TauCeti.badlyApproximable_of_natDegree_minpoly_eq_two.
TauCeti.badlyApproximable_of_natDegree_minpoly_eq_two {ξ : ℝ} (h : (minpoly ℚ ξ).natDegree = 2) :
TauCeti.BadlyApproximable ξ
Sources
TheoremThue's approximation theorem for real α#
Let α be a real algebraic number of degree
d ≥ 2 and let κ > d / 2 + 1. Then only finitely many rationals ξ satisfy
|ξ - α| ≤ H(ξ) ^ (-κ). This is a variant of Evertse, Theorem 6.9, rather than that statement
verbatim: every degree d ≥ 2 is allowed.
TauCeti.thue_approximation_real {α : ℝ} (hd : 2 ≤ (minpoly ℚ α).natDegree) {κ : ℝ}
(hκ : ↑(minpoly ℚ α).natDegree / 2 + 1 < κ) : {ξ | |↑ξ - α| ≤ Height.mulHeight₁ ξ ^ (-κ)}.Finite
Lean
Formalized in Tau Ceti as TauCeti.thue_approximation_real.
Other forms
Thue's approximation theorem, for complex α. Formalized in Tau Ceti as TauCeti.thue_approximation.
TauCeti.thue_approximation {α : ℂ} (hd : 2 ≤ (minpoly ℚ α).natDegree) {κ : ℝ}
(hκ : ↑(minpoly ℚ α).natDegree / 2 + 1 < κ) : {ξ | ‖↑ξ - α‖ ≤ Height.mulHeight₁ ξ ^ (-κ)}.Finite
Sources
Uses 1
TheoremThue's gap principle (Evertse, Theorem 6.14)#
Let α be a complex algebraic number of
degree d ≥ 2 and let κ > d / 2 + 1. There are constants C ≥ 1 and λ ≥ 1 such that for
all rationals ξ₁ and ξ with |ξ₁ - α| ≤ H(ξ₁) ^ (-κ), H(ξ₁) ≥ C and
|ξ - α| ≤ H(ξ) ^ (-κ), the heights satisfy H(ξ) ≤ H(ξ₁) ^ λ. The degree hypothesis
already forces α to be algebraic.
TauCeti.thue_gap_principle {α : ℂ} (hd : 2 ≤ (minpoly ℚ α).natDegree) {κ : ℝ}
(hκ : ↑(minpoly ℚ α).natDegree / 2 + 1 < κ) :
∃ C lam,
1 ≤ C ∧
1 ≤ lam ∧
∀ (ξ₁ ξ : ℚ),
‖↑ξ₁ - α‖ ≤ Height.mulHeight₁ ξ₁ ^ (-κ) →
C ≤ Height.mulHeight₁ ξ₁ →
‖↑ξ - α‖ ≤ Height.mulHeight₁ ξ ^ (-κ) →
Height.mulHeight₁ ξ ≤ Height.mulHeight₁ ξ₁ ^ lam
Uses 2 · Used by 1
Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.