OAI/NumberTheory/EgyptianFractions/OptimizedSelbergError.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.SelbergOptimal.optimalWeight_primeFactor_mass_le line 14

   Source documentation

   The actual optimal weights have a logarithmically bounded weighted mass. This uses the sharp coefficient bound, not the crude inverse-density estimate.

   theorem optimalWeight_primeFactor_mass_le (s : BoundingSieve) {z : ℕ} (hz : 1 ≤ z) :
       (∑ d ∈ s.prodPrimes.divisors, |optimalWeight s z d| *
         (2 : ℝ) ^ d.primeFactors.card) ≤ (z : ℝ) * (1 + Real.log z) ^ 2 := by
   …

   Mentions: OAI.Problem337.SelbergOptimal.optimalWeight

2. theorem OAI.Problem337.SelbergOptimal.errSum_optimalWeight_le_log line 45

   Source documentation

   A dimension-two local remainder envelope gives an explicit logarithmic error for the constructed optimal Selberg weights.

   theorem errSum_optimalWeight_le_log (s : BoundingSieve) {z : ℕ} (hz : 1 ≤ z)
       (hrem : ∀ a ∈ s.prodPrimes.divisors, ∀ b ∈ s.prodPrimes.divisors,
         |s.rem (Nat.lcm a b)| ≤
           (2 : ℝ) ^ a.primeFactors.card * (2 : ℝ) ^ b.primeFactors.card) :
       s.errSum (BoundingSieve.lambdaSquared (optimalWeight s z)) ≤
         (z : ℝ) ^ 2 * (1 + Real.log z) ^ 4 := by
   …

   Mentions: OAI.Problem337.SelbergOptimal.optimalWeight

3. theorem OAI.Problem337.SelbergOptimal.siftedSum_le_log_error line 62

   Source documentation

   Fully optimized finite Selberg inequality with explicit logarithmic error.

   theorem siftedSum_le_log_error (s : BoundingSieve) {z : ℕ} (hz : 1 ≤ z)
       (hrem : ∀ a ∈ s.prodPrimes.divisors, ∀ b ∈ s.prodPrimes.divisors,
         |s.rem (Nat.lcm a b)| ≤
           (2 : ℝ) ^ a.primeFactors.card * (2 : ℝ) ^ b.primeFactors.card) :
       s.siftedSum ≤ s.totalMass / normalizer s z +
         (z : ℝ) ^ 2 * (1 + Real.log z) ^ 4 :=
   …

   Mentions: OAI.Problem337.SelbergOptimal.normalizer