OAI/NumberTheory/JointDickman/Counting/CoefficientRegularityLoss.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.regularityRemainder line 12
2. theorem OAI.JointDickman.regularityRemainder_nonneg line 15
3. theorem OAI.JointDickman.regularityRemainder_tendsto line 19
4. def OAI.JointDickman.discardedCoefficientWeight line 36
5. theorem OAI.JointDickman.discardedCoefficientWeight_le line 40
6. theorem OAI.JointDickman.coefficient_regularity_loss line 61

   Source documentation

   The positive-slope rectangle form of manuscript (9). Its error sequence is independent of the tail cutoff, slope, and rectangle location.

   theorem coefficient_regularity_loss
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       {δ : ℝ} (hδ : 0 < δ) (hδ32 : δ ≤ 32) :
       ∃ K : ℝ, 0 < K ∧ ∀ (L : ℕ) (τ : ℝ), 0 < L → 0 < τ →
         ∃ ε : ℕ → ℝ, (∀ B, 0 ≤ ε B) ∧ Tendsto ε atTop (𝓝 0) ∧
           ∀ᶠ B : ℕ in atTop, ∀ (C : ℝ) (j l₁ r₁ l₂ r₂ : ℕ),
             0 ≤ C → j ≠ 0 → l₁ ≤ r₁ → l₂ ≤ r₂ →
             Real.exp (δ * B) ≤ (r₁ : ℝ) - l₁ → Real.exp (δ * B) ≤ (r₂ : ℝ) - l₂ →
             (∑ b ∈ Ico l₁ r₁, ∑ d ∈ Ico l₂ r₂, discardedCoefficientWeight B L j b d τ C) ≤
               K * ((r₁ : ℝ) - l₁) * ((r₂ : ℝ) - l₂) * singularFactor 24 j *
                 (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.discardedCoefficientWeight, OAI.JointDickman.singularFactor