WikiLeanRecent changes · Proposals · Flags · Stats · About

Diff — Diophantine approximation

Revision #1158 → #2454 · back to history

modifiedBest Diophantine approximation (first definition)6bf7d22d9c16
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grepping Mathlib for `bestApprox`/`best_approx` in a Diophantine-approximation sense returns nothing; only Legendre's converse (`Real.exists_rat_eq_convergent`) and Dirichlet's theorem live in `DiophantineApproximation/Basic.lean`.
status—not_formalized
modifiedBest Diophantine approximation (second definition)660e26cf23a1
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No `bestApprox`-style definition (variant with |qα − p| minimization) appears in Mathlib.
status—not_formalized
modifiedSecond-definition best approximation implies first640e55ae31f0
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Since neither notion of best Diophantine approximation is defined in Mathlib, the implication between them is not formalized either.
status—not_formalized
modifiedBest approximations via continued fractions6883137d700c
FieldFrom #1158To #2454
mathlib.decl—Real.exists_rat_eq_convergent
mathlib.match_kind—special_case
mathlib.module—Mathlib.NumberTheory.DiophantineApproximation.Basic
note—Mathlib formalizes Legendre's converse (`Real.exists_rat_eq_convergent`) — any rational with |ξ − q| < 1/(2q.den²) is a convergent — but does not state the general theorem that convergents enumerate the best approximations.
status—partial
modifiedBest approximations of ea8420df1ebd9
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The continued-fraction expansion of `Real.exp 1` and its list of best approximations are not developed in Mathlib.
status—not_formalized
modifiedBadly approximable number8ea108959d50
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep for `badlyApproximable` / `BadlyApproximable` in Mathlib returns no hits; the definition is absent.
status—not_formalized
modifiedCharacterization via bounded partial quotients9d9a07330986
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Without a `badlyApproximable` definition, the equivalence with boundedness of the partial quotients of the regular continued fraction is not formalized.
status—not_formalized
modifiedEquivalent characterization via Markov constant3ac17624c3be
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Neither the Markov constant of a real number nor this equivalence is present in Mathlib.
status—not_formalized
modifiedApproximation of a rational by another rationalfffe6aecefd6
FieldFrom #1158To #2454
anchor.snippetbecauseis a positive integer and is thus not lower than 1
mathlib.decl—Rat.finite_rat_abs_sub_lt_one_div_den_sq
mathlib.match_kind—special_case
mathlib.module—Mathlib.NumberTheory.DiophantineApproximation.Basic
note—The pigeonhole 'nonzero integer ⇒ ≥ 1' step underlies `Rat.finite_rat_abs_sub_lt_one_div_den_sq`, which realises the section's conclusion that a rational has only finitely many good rational approximations.
provenanceai-agent1ai-moderated
status—partial
modifiedLiouville's theorem on algebraic numbers60c4c7b3882b
FieldFrom #1158To #2454
mathlib.decl—Liouville.exists_pos_real_of_irrational_root
mathlib.match_kind—generalization
mathlib.module—Mathlib.NumberTheory.Transcendental.Liouville.Basic
note—`Liouville.exists_pos_real_of_irrational_root` gives, for irrational α that is a root of any nonzero f ∈ ℤ[X], an A>0 with 1 ≤ (b+1)^{deg f} · |α − a/(b+1)| · A — the essential Liouville inequality (bounding by any witness polynomial's degree rather than the minimal one).
status—formalized
modifiedLiouville constantb51575c32376
FieldFrom #1158To #2454
mathlib.decl—transcendental_liouvilleNumber
mathlib.match_kind—generalization
mathlib.module—Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
note—`liouvilleNumber m = ∑ 1/m^{i!}` is defined and `transcendental_liouvilleNumber` proves it is transcendental for every integer m ≥ 2, covering Liouville's classical m = 10 (and m = 2) constant.
status—formalized
modifiedThue–Siegel–Roth theoremc23ab45a038c
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Thue–Siegel–Roth theorem is only mentioned in a docstring comment of `LiouvilleWith.lean` and is not proved in Mathlib.
status—not_formalized
modifiedSchmidt's simultaneous approximation theorem1f8e0c5e3772
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Schmidt's subspace / simultaneous approximation theorem is not in Mathlib.
status—not_formalized
modifiedFeldman's effective refinement of Baker's theorem090fffb1d777
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No results by Baker or Feldman on effective Diophantine approximation appear in Mathlib.
status—not_formalized
modifiedDirichlet's approximation theorem4cd6d73d1985
FieldFrom #1158To #2454
mathlib.decl—Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational
mathlib.match_kind—exact
mathlib.module—Mathlib.NumberTheory.DiophantineApproximation.Basic
note—`Real.infinite_rat_abs_sub_lt_one_div_den_sq_of_irrational` states that for irrational ξ the set {q : ℚ | |ξ − q| < 1/q.den²} is infinite, which is exactly the statement quoted; the underlying pigeonhole form is `Real.exists_int_int_abs_mul_sub_le`.
status—formalized
modifiedHurwitz's theoremb0721c466e45
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep for `Hurwitz` in Mathlib finds only Hurwitz zeta-related material; the Diophantine Hurwitz bound |α − p/q| < 1/(√5 q²) is absent.
status—not_formalized
modifiedBorel's three-convergents theorem38758330626a
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The statement that among any three consecutive convergents at least one satisfies |α − p/q| < 1/(√5 q²) is not in Mathlib.
status—not_formalized
modifiedEquivalent real numbers7e04fd5f954e
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The GL₂(ℤ)-action equivalence of real numbers has no dedicated definition in Mathlib.
status—not_formalized
modifiedSerret's theorem on equivalent irrationalsdc728177dd24
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The characterization of GL₂(ℤ)-equivalent irrationals via eventually-equal continued fraction tails is not formalized.
status—not_formalized
modifiedHurwitz sharpness via golden ratioc61b8bd870a2
FieldFrom #1158To #2454
anchor.snippetbe the golden ratiothere are only a finite number of rational numbers p / q such that
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The sharpness statement — for the golden ratio only finitely many p/q satisfy |φ − p/q| < 1/(c q²) once c > √5 — is not in Mathlib.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedImproved Hurwitz bound excluding golden-ratio classb14269a41a39
FieldFrom #1158To #2454
anchor.snippetFor every irrational numberwhich is not equivalent to
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The refined constant 1/(√8 q²) for numbers not equivalent to the golden ratio (start of the Lagrange spectrum) is not formalized.
provenanceai-agent1ai-moderated
status—not_formalized
modifiedψ-approximable real number2844b4581d1b
FieldFrom #1158To #2454
mathlib.decl—wellApproximable
mathlib.match_kind—generalization
mathlib.module—Mathlib.NumberTheory.WellApproximable
note—`wellApproximable`/`addWellApproximable` in `Mathlib.NumberTheory.WellApproximable` defines the limsup set of points within δₙ of order-n rationals in a (semi)normed group — a group-theoretic version of the ψ-approximable set — but there is no direct real-number definition.
status—partial
modifiedKhinchin's theorem69df6a71df87
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Grep finds no Khinchin/Khintchine theorem on metric Diophantine approximation in Mathlib; only Gallagher's ergodic theorem (`AddCircle.addWellApproximable_ae_empty_or_univ`) is present.
status—not_formalized
modifiedKoukoulopoulos–Maynard proof of Duffin–Schaeffer17386884db7a
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Koukoulopoulos–Maynard proof is explicitly noted as not included in `Mathlib.NumberTheory.WellApproximable`.
status—not_formalized
modifiedJarník–Besicovitch theoremd464eedf11a1
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The dim_H = 2/(1+β) formula for the set of β-approximable numbers is not in Mathlib.
status—not_formalized
modifiedJarník's theorem on badly approximable numbersd73976aabc27
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Since badly approximable numbers are not defined in Mathlib, the statement that their set has full Hausdorff dimension is absent.
status—not_formalized
modifiedSchmidt's incompressibility theorem9f027aecbf90
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Schmidt's winning-set / incompressibility theorem is not in Mathlib.
status—not_formalized
modifiedWeyl's equidistribution criterion69aefc2cabd2
FieldFrom #1158To #2454
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No formalization of Weyl's equidistribution criterion (equivalence between equidistribution mod 1 and vanishing exponential sums) is present in Mathlib.
status—not_formalized
addedVery well approximable numbersb0352378bbf7
addedLiouville numbers7defde08f4ba
addedWell approximable number6ecd31214125
addedDuffin–Schaeffer conjecture0edfc12b5a20
addedBeresnevich–Velani Hausdorff-measure equivalence924ddfb686a3
addedSchmidt's higher-dimensional generalization of Jarník's theorem81c05b768c98
addedLittlewood conjecturec040ca33ad79
addedLonely runner conjecture5b41a981c263
addedMargulis's proof of the Oppenheim conjecture8fea793732ad
addedKleinbock–Margulis proof of Baker–Sprindzhuk conjectures298b3616a739