OAI/NumberTheory/EgyptianFractions/VaughanDyadicUniform.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.Vaughan.typeIILogScale line 12
2. lemma OAI.Problem337.Vaughan.one_le_typeIILogScale line 14
3. lemma OAI.Problem337.Vaughan.log_nat_le_typeIILogScale line 20
4. theorem OAI.Problem337.Vaughan.typeIIBlock_sq_le_normalized line 34

   Source documentation

   Uniform logarithmic normalization of the coefficient block estimate.

   theorem typeIIBlock_sq_le_normalized
       (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (N U V j : ℕ) (hqN : q ≤ N) (hM : 2 ^ j ≤ N) :
       ‖typeIIBlock N U V j (fun k => VaughanBilinear.phase (θ * k))‖ ^ 2 ≤
         (2 * ((2 ^ j : ℕ) : ℝ) * (typeIILogScale N) ^ 3) *
           ((2 * ((N / 2 ^ j : ℕ) : ℝ) / q + 1) *
             (2 * ((2 ^ j : ℕ) : ℝ) + 4 * (q : ℝ) * typeIILogScale N)) *
               (((N / 2 ^ j : ℕ) : ℝ) * (typeIILogScale N) ^ 2) := by
   …

   Mentions: OAI.Problem337.Vaughan.typeIIBlock, OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.Vaughan.typeIILogScale

5. theorem OAI.Problem337.Vaughan.typeIIBlock_sq_le_uniform line 75

   Source documentation

   Uniform actual Type II block bound, with no cancellation or energy premise.

   theorem typeIIBlock_sq_le_uniform
       (θ : ℝ) (a : ℤ) (q : ℕ) (hq : 0 < q)
       (hcop : IsCoprime a (q : ℤ))
       (happrox : |θ - (a : ℝ) / q| ≤ 1 / (q : ℝ) ^ 2)
       (N U V j : ℕ) (hqN : q ≤ N) (hU : 0 < U) (hV : 0 < V) :
       ‖typeIIBlock N U V j (fun k => VaughanBilinear.phase (θ * k))‖ ^ 2 ≤
         32 * (N : ℝ) * (typeIILogScale N) ^ 6 *
           ((N : ℝ) / q + (N : ℝ) / U + (N : ℝ) / V + q) := by
   …

   Mentions: OAI.Problem337.Vaughan.typeIIBlock, OAI.Problem337.VaughanBilinear.phase, OAI.Problem337.Vaughan.typeIILogScale