OAI/NumberTheory/JointDickman/Analysis/MellinSieveQuadratic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.mellinSieveMainKernel line 11
2. def OAI.JointDickman.mellinSieveMain line 14
3. lemma OAI.JointDickman.mellinSieveMain_nonneg line 19
4. lemma OAI.JointDickman.norm_mellinSieveMainKernel line 25
5. lemma OAI.JointDickman.mellinSieveMain_eq line 31
6. lemma OAI.JointDickman.mellinSieveMain_bound line 55
7. lemma OAI.JointDickman.mellin_quadratic_kernel_error line 75

   Source documentation

   The remainder of a finite quadratic form is bounded from its actual pairwise kernel discrepancies. The sample count is exposed explicitly.

   lemma mellin_quadratic_kernel_error (S : Finset ℝ) (b : ℝ → ℂ)
       (K L : ℝ → ℝ → ℂ) {δ : ℝ} (hδ : 0 ≤ δ)
       (herror : ∀ t ∈ S, ∀ u ∈ S, ‖K t u-L t u‖ ≤ δ) :
       |(∑ t ∈ S, ∑ u ∈ S, ((b t*conj (b u))*K t u).re) -
         (∑ t ∈ S, ∑ u ∈ S, ((b t*conj (b u))*L t u).re)| ≤
           δ*S.card*∑ t ∈ S, ‖b t‖^2 := by
   …