OAI/NumberTheory/JointDickman/Amplification/RationalArcSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.rational_separation line 11
2. theorem OAI.JointDickman.rationalArc_unique line 33
3. theorem OAI.JointDickman.majorArc_width_separation line 49
4. theorem OAI.JointDickman.majorArc_rational_unique line 72

   Source documentation

   At the manuscript's exponential scale a point belongs to at most one reduced rational arc, before passing to the lifted endpoint coordinate.

   theorem majorArc_rational_unique :
       ∀ᶠ B : ℕ in atTop, ∀ X : ℝ, 0 < X → (9/10 : ℝ)*B ≤ Real.log X →
         ∀ (θ : ℝ) (r s : ℚ), (r.den : ℝ) ≤ (B : ℝ)^12 →
         (s.den : ℝ) ≤ (B : ℝ)^12 → |θ-(r : ℝ)| ≤ (B : ℝ)^13/X →
         |θ-(s : ℝ)| ≤ (B : ℝ)^13/X → r = s := by
   …