OAI/NumberTheory/EgyptianFractions/MinorArcLogWindow.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.MinorArc.eventually_exists_minor_fraction_log_window line 13

   Source documentation

   The usual logarithmic major arcs leave only phases admitting an actual coprime rational approximation in the required real denominator window. The onset is uniform in the phase.

   theorem eventually_exists_minor_fraction_log_window (A : ℕ) :
       ∀ᶠ X : ℝ in atTop, ∀ x : ℝ, x ∈ Set.Icc (0 : ℝ) 1 →
         x ∉ ThreePrimeAnalysis.majorArcUnion ⌊Real.log X ^ A⌋₊
           (2 * Real.log X ^ A / X) →
         ∃ a : ℤ, ∃ q : ℕ,
           Real.log X ^ A ≤ (q : ℝ) ∧ (q : ℝ) ≤ X / Real.log X ^ A ∧
           0 < q ∧ IsCoprime a (q : ℤ) ∧
           |x - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2 := by
   …

   Mentions: OAI.Problem337.ThreePrimeAnalysis.majorArcUnion

2. theorem OAI.Problem337.MinorArc.eventually_minor_fraction_with_vaughan_budget line 37

   Source documentation

   A denominator supplied by the genuine Dirichlet minor-arc geometry also satisfies the full scalar Vaughan budget, uniformly in the phase. This does not assert an exponential-sum estimate.

   theorem eventually_minor_fraction_with_vaughan_budget
       (B D : ℕ) (C : ℝ) (hC : 0 ≤ C) :
       ∀ᶠ X : ℝ in atTop, ∀ x : ℝ, x ∈ Set.Icc (0 : ℝ) 1 →
         x ∉ ThreePrimeAnalysis.majorArcUnion
           ⌊Real.log X ^ (2 * (B + D + 2))⌋₊
           (2 * Real.log X ^ (2 * (B + D + 2)) / X) →
         ∃ a : ℤ, ∃ q : ℕ,
           Real.log X ^ (2 * (B + D + 2)) ≤ (q : ℝ) ∧
           (q : ℝ) ≤ X / Real.log X ^ (2 * (B + D + 2)) ∧
           0 < q ∧ IsCoprime a (q : ℤ) ∧
           |x - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2 ∧
           C * (X / Real.sqrt q + X ^ (4 / 5 : ℝ) + Real.sqrt (X * q)) *
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.ThreePrimeAnalysis.majorArcUnion