OAI/NumberTheory/JointDickman/Amplification/IndependentRegularityLoss.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.regularCoefficientWeight_le line 13
2. theorem OAI.JointDickman.coefficient_truncation_loss_nonneg line 20
3. theorem OAI.JointDickman.independent_truncation_loss_pointwise line 24
4. theorem OAI.JointDickman.independent_truncation_loss_sum line 33
5. theorem OAI.JointDickman.independent_coefficient_regularity_loss line 53

   Source documentation

   The independent two-variable assertion of the manuscript's regularity-loss lemma: the loss is bounded by the area, uniformly in the tail cutoff. The two inputs are the cited upper sieve and reciprocal-prime Mertens estimate.

   theorem independent_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 : ℝ) (u v x y : ℕ), 0 ≤ C → u ≤ v → x ≤ y →
             Real.exp (δ * B) ≤ (v : ℝ) - u → Real.exp (δ * B) ≤ (y : ℝ) - x →
             (∑ a ∈ Ico u v, ∑ b ∈ Ico x y, (coefficientWeight B a * coefficientWeight B b -
               regularCoefficientWeight B L τ C a * regularCoefficientWeight B L τ C b)) ≤
               K * ((v : ℝ) - u) * ((y : ℝ) - x) * (ε B + Real.exp (-(1 / 10 : ℝ) * C)) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.coefficientWeight, OAI.JointDickman.regularCoefficientWeight