OAI/NumberTheory/JointDickman/Amplification/ArithmeticProfilePreservation.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.amplificationPeriod line 11
2. def OAI.JointDickman.smoothResidueAmplification line 14
3. theorem OAI.JointDickman.smoothResidueAmplification_energy line 18
4. theorem OAI.JointDickman.smoothResidueAmplification_mean line 26
5. theorem OAI.JointDickman.smooth_arithmetic_profile_preservation line 33

   Source documentation

   The precise preservation statement, using the actual arithmetic weight. Only the previously cited sieve and Mertens inputs enter its moment bound.

   theorem smooth_arithmetic_profile_preservation
       (hFord : PublishedInputs.FordUpperSieveInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (W : ResidueProfile) (L : ℕ) (τ C : ℝ) (T : ℕ → ℕ)
       (hT : ∀ᶠ B : ℕ in atTop, 0 < T B ∧ (T B : ℝ) ≤ Real.exp ((1/10 : ℝ)*B)) :
       Tendsto (fun B => W.correlation (amplificationPeriod B)
         (smoothResidueAmplification B L τ C (T B)) - W.mean *
           (arithmeticAmplificationMoment B L τ C (amplificationSmoothWeight B (T B)) 1 : ℂ))
         atTop (nhds 0) := by
   …

   Mentions: OAI.JointDickman.PublishedInputs.FordUpperSieveInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.ResidueProfile, OAI.JointDickman.amplificationPeriod, OAI.JointDickman.smoothResidueAmplification, OAI.JointDickman.arithmeticAmplificationMoment, OAI.JointDickman.amplificationSmoothWeight