OAI/NumberTheory/EgyptianFractions/VaughanTypeINormalized.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.VaughanHyperbolic.hyperbolicCost_min_le line 10

   Source documentation

   A common logarithmic majorant for both actual Type I costs.

   theorem hyperbolicCost_min_le (N A q : ℕ) (hN : 1 ≤ N) (hq : 0 < q)
       (hqN : q ≤ N) :
       RealTypeI.hyperbolicCost N (min A N) q ≤
         8 * ((N : ℝ) / q + A + q) * (1 + Real.log (2 * (N : ℝ))) := by
   …

   Mentions: OAI.Problem337.RealTypeI.hyperbolicCost

2. lemma OAI.Problem337.VaughanHyperbolic.log_le_common line 43
3. theorem OAI.Problem337.VaughanHyperbolic.first_typeI_normalized_bound line 51

   Source documentation

   Uniform Type I bound in the parameters of the optimized Vaughan cutoff.

   theorem first_typeI_normalized_bound
       (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (N U : ℕ) (hN : 1 ≤ N) (hqN : q ≤ N) :
       ‖Vaughan.weightedSum (Finset.Ioc 0 N) (fun n => RealPhase.phase (α * n))
           (Vaughan.shortPart U (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log)‖ ≤
         16 * (1 + Real.log (2 * (N : ℝ))) ^ 2 * ((N : ℝ) / q + U + q) := by
   …

   Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.RealPhase.phase, OAI.Problem337.Vaughan.shortPart

4. theorem OAI.Problem337.VaughanHyperbolic.second_typeI_normalized_bound line 74

   Source documentation

   Uniform second Type I bound with the full product support retained.

   theorem second_typeI_normalized_bound
       (α : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |α - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (N U V : ℕ) (hN : 1 ≤ N) (hqN : q ≤ N) :
       ‖Vaughan.weightedSum (Finset.Ioc 0 N) (fun n => RealPhase.phase (α * n))
           (Vaughan.typeICoefficient U V * ζ)‖ ≤
         8 * (1 + Real.log (2 * (N : ℝ))) ^ 2 * ((N : ℝ) / q + U * V + q) := by
   …

   Mentions: OAI.Problem337.Vaughan.weightedSum, OAI.Problem337.RealPhase.phase, OAI.Problem337.Vaughan.typeICoefficient