OAI/NumberTheory/JointDickman/Analysis/MellinSieveRemainder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.primeProduct_dvd_iff line 12

   Distinct definitions of this name: OAI/NumberTheory/JointDickman/Arithmetic/DivisorProductMean.lean:13 (different declaration text), OAI/NumberTheory/JointDickman/Arithmetic/SmoothInclusionExclusion.lean:25 (different declaration text). Qualify references as OAI.JointDickman.primeProduct_dvd_iff@path.

2. lemma OAI.JointDickman.primeDivisorEvents_subset_iff line 35
3. def OAI.JointDickman.mellinSieveDiscreteKernel line 45
4. def OAI.JointDickman.mellinSieveSquareWeight line 48
5. lemma OAI.JointDickman.mellinSieveSquareWeight_nonneg line 52
6. lemma OAI.JointDickman.mellinSieveMain_div line 56
7. theorem OAI.JointDickman.mellin_sieve_remainder_bound line 71

   Source documentation

   Only the concrete scalar divisor-sum kernel discrepancy is needed for the weighted sieve remainder. No short-average premise is used.

   theorem mellin_sieve_remainder_bound {P D : Finset ℕ}
       (hD : D ⊆ P) (hprime : ∀ p ∈ D, p.Prime)
       (K : ℕ) (N : ℝ) (S : Finset ℝ) (b : ℝ → ℂ)
       {δ : ℝ} (hδ : 0 ≤ δ)
       (hkernel : ∀ t ∈ S, ∀ u ∈ S,
         ‖mellinSieveDiscreteKernel K (∏ p ∈ D, p) N (t-u) -
           mellinSieveMainKernel N (t-u)/((∏ p ∈ D, p : ℕ) : ℂ)‖ ≤ δ) :
       |sieveRemainder (fun n : Icc 1 K => primeDivisorEvents P n)
         (fun n => mellinSieveSquareWeight N S b n) (mellinSieveMain N S b)
         (fun p => 1/(p : ℝ)) D| ≤ δ*S.card*∑ t ∈ S, ‖b t‖^2 := by
   …

   Mentions: OAI.JointDickman.mellinSieveDiscreteKernel, OAI.JointDickman.mellinSieveMainKernel, OAI.JointDickman.sieveRemainder, OAI.JointDickman.primeDivisorEvents, OAI.JointDickman.mellinSieveSquareWeight, OAI.JointDickman.mellinSieveMain