OAI/NumberTheory/EgyptianFractions/MinorArcVaughan.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Actual von Mangoldt cancellation outside the logarithmic major arcs. Both the rational approximation and the Vaughan estimate are discharged.

   theorem eventually_vonMangoldt_minor_arc_bound (D : ℕ) :
       ∀ᶠ N : ℕ in atTop, ∀ θ : ℝ, θ ∈ Set.Icc (0 : ℝ) 1 →
         θ ∉ ThreePrimeAnalysis.majorArcUnion
           ⌊Real.log N ^ (2 * (4 + D + 2))⌋₊
           (2 * Real.log N ^ (2 * (4 + D + 2)) / N) →
         ‖Vaughan.weightedSum (Finset.Ioc 0 N)
           (fun k => VaughanBilinear.phase (θ * k)) Λ‖ ≤
           (N : ℝ) / Real.log N ^ D := by
   …

   Mentions: OAI.Problem337.D, OAI.Problem337.ThreePrimeAnalysis.majorArcUnion, OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.VaughanBilinear.phase