OAI/NumberTheory/JointDickman/Amplification/SubsequenceAmplifiedProfile.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.JointDickman.empiricalResidueCoefficient_subsequence_along line 12

   Source documentation

   Countable residue compactness can be taken inside any given sequence.

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

   Mentions: OAI.JointDickman.empiricalResidueCoefficient

2. theorem OAI.JointDickman.exists_arithmetic_amplification_profile_along line 30

   Source documentation

   The profile is constructed on a further subsequence of the originally chosen scales. The correlation limit and every amplification test survive.

   theorem exists_arithmetic_amplification_profile_along (H : ℕ → ℕ → ℂ) {C : ℝ}
       (hC : 0 ≤ C) (hH : ∀ N n, ‖H N n‖ ≤ C) (r : ℕ → ℕ) (hr : StrictMono r)
       {β : ℂ} (hmean : Tendsto (fun N => (∑ n ∈ range (r N), H (r N) n)/(r N : ℂ))
         atTop (nhds β)) :
       ∃ (s : ℕ → ℕ), StrictMono s ∧ ∃ W : ResidueProfile, W.mean = β ∧
         ∀ (B L : ℕ) (τ C' : ℝ) (T : ℕ),
           Tendsto (fun N => (∑ n ∈ range (r (s N)), H (r (s N)) n *
             (arithmeticSubsetAmplification B L τ C' (amplificationSmoothWeight B T) n : ℂ)) /
               (r (s N) : ℂ)) atTop
             (nhds (W.correlation (amplificationPeriod B) (smoothResidueAmplification B L τ C' T))) := by
   …

   Mentions: OAI.JointDickman.ResidueProfile, OAI.JointDickman.arithmeticSubsetAmplification, OAI.JointDickman.amplificationSmoothWeight, OAI.JointDickman.amplificationPeriod, OAI.JointDickman.smoothResidueAmplification