OAI/NumberTheory/JointDickman/Probability/EmpiricalResidueProfile.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite residue coefficients of a bounded arithmetic correlation

  1. def OAI.JointDickman.empiricalResidueCoefficient line 12
  2. def OAI.JointDickman.empiricalResidueTest line 16
  3. theorem OAI.JointDickman.empiricalResidueCoefficient_test line 20
  4. theorem OAI.JointDickman.empiricalResidueCoefficient_norm_le line 45
  5. theorem OAI.JointDickman.empiricalResidueCoefficient_subsequence line 64

    Source documentation

    All residue coefficients converge simultaneously along one subsequence.

    theorem empiricalResidueCoefficient_subsequence (H : ℕ → ℕ → ℂ) {C : ℝ}
    (hC : 0 ≤ C) (hH : ∀ N n, ‖H N n‖ ≤ C) :
    ∃ (s : ℕ → ℕ), StrictMono s ∧
      ∃ V : (q : ℕ+) → ZMod (q : ℕ) → ℂ,
        ∀ q a, Tendsto (fun N => empiricalResidueCoefficient H (s N) q a) atTop (nhds (V q a)) := by
…

    Mentions: OAI.JointDickman.empiricalResidueCoefficient