OAI/NumberTheory/JointDickman/Probability/ResidueProfileLimits.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.empiricalResidueCoefficient_density_bound line 12

   Source documentation

   A sharper coefficient bound retains the density of the residue class.

   theorem empiricalResidueCoefficient_density_bound (H : ℕ → ℕ → ℂ) {C : ℝ}
       (hH : ∀ N n, ‖H N n‖ ≤ C) (N : ℕ) (q : ℕ+) (a : ZMod (q : ℕ)) :
       ‖empiricalResidueCoefficient H N q a‖ ≤
         (q : ℕ) * C * ((∑ n ∈ range N,
           if (n : ZMod (q : ℕ)) = a then (1 : ℝ) else 0) / (N : ℝ)) := by
   …

   Mentions: OAI.JointDickman.empiricalResidueCoefficient

2. theorem OAI.JointDickman.residueCoefficient_limit_bound line 31
3. theorem OAI.JointDickman.residueCoefficient_test_limit line 49
4. theorem OAI.JointDickman.residueLift_natCast line 61
5. theorem OAI.JointDickman.residueCoefficient_limit_compatible line 67
6. theorem OAI.JointDickman.exists_residueProfile line 83

   Source documentation

   Compactness produces the full profile, including its compatibility and uniform energy bound; neither property is an additional analytic input.

   theorem exists_residueProfile (H : ℕ → ℕ → ℂ) {C : ℝ}
       (hC : 0 ≤ C) (hH : ∀ N n, ‖H N n‖ ≤ C) :
       ∃ (s : ℕ → ℕ), StrictMono s ∧ ∃ W : ResidueProfile,
         (∀ q a, ‖W.value q a‖ ≤ C) ∧
         ∀ (q : ℕ+) (f : ZMod (q : ℕ) → ℂ),
           Tendsto (fun N => empiricalResidueTest H (s N) f) atTop
             (nhds (residueMean (fun a => W.value q a * f a))) := by
   …

   Mentions: OAI.JointDickman.ResidueProfile, OAI.JointDickman.empiricalResidueTest, OAI.JointDickman.residueMean