OAI/NumberTheory/EgyptianFractions/VaughanEstimate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem337.Vaughan.realPhase_eq_bilinear_phase line 10
2. lemma OAI.Problem337.Vaughan.optimized_typeI_scales line 14
3. theorem OAI.Problem337.Vaughan.vonMangoldt_sum_bound line 27

   Source documentation

   An explicit classical Vaughan estimate for the actual von Mangoldt exponential sum. The only analytic input is a reduced rational approximation; all Type I and Type II cancellation estimates have been proved above.

   theorem vonMangoldt_sum_bound
       (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (N : ℕ) (hqN : q ≤ N)
       (hpow : 2 ≤ (N : ℝ) ^ (2 / 5 : ℝ)) :
       ‖weightedSum (Finset.Ioc 0 N) (fun k => VaughanBilinear.phase (θ * k)) Λ‖ ≤
         200 * (typeIILogScale N) ^ 4 * approximationEnvelope N q := by
   …

   Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.Vaughan.typeIILogScale, OAI.Problem337.Vaughan.approximationEnvelope

4. theorem OAI.Problem337.Vaughan.vonMangoldt_sum_log_bound line 98

   Source documentation

   The ordinary logarithmic form of the classical Vaughan estimate.

   theorem vonMangoldt_sum_log_bound
       (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (N : ℕ) (hqN : q ≤ N)
       (hpow : 2 ≤ (N : ℝ) ^ (2 / 5 : ℝ)) (hlog : 1 ≤ Real.log N) :
       ‖weightedSum (Finset.Ioc 0 N) (fun k => VaughanBilinear.phase (θ * k)) Λ‖ ≤
         16200 * (Real.log N) ^ 4 * approximationEnvelope N q := by
   …

   Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.Vaughan.approximationEnvelope

5. theorem OAI.Problem337.Vaughan.eventually_vonMangoldt_sum_log_bound line 121

   Source documentation

   The estimate holds uniformly in every reduced approximation once the summation length is large, with an absolute explicit constant.

   theorem eventually_vonMangoldt_sum_log_bound :
       ∀ᶠ N : ℕ in atTop, ∀ (θ : ℝ) (a : ℤ) (q : ℕ), 0 < q →
         IsCoprime a (q : ℤ) → |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2 → q ≤ N →
         ‖weightedSum (Finset.Ioc 0 N) (fun k => VaughanBilinear.phase (θ * k)) Λ‖ ≤
           16200 * (Real.log N) ^ 4 * approximationEnvelope N q := by
   …

   Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.Vaughan.approximationEnvelope