OAI/NumberTheory/JointDickman/Amplification/ArithmeticPeriod.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.auxiliarySquarePeriod line 11
2. theorem OAI.JointDickman.auxiliarySquarePeriod_pos line 14
3. instance OAI.JointDickman.(instance at line 18) line 18
4. theorem OAI.JointDickman.auxiliaryProduct_dvd_period line 21
5. theorem OAI.JointDickman.auxiliaryProduct_mul_prime_dvd_period line 25
6. theorem OAI.JointDickman.coefficientPrimeSet_quotient_modEq line 33
7. theorem OAI.JointDickman.arithmeticSubsetAmplification_modEq line 51
8. def OAI.JointDickman.residueAmplification line 75
9. theorem OAI.JointDickman.residueAmplification_natCast line 79
10. theorem OAI.JointDickman.arithmeticAmplification_mean_tendsto line 86

    Source documentation

    The ordinary mean has this exact finite residue mean as its limit.

    theorem arithmeticAmplification_mean_tendsto (B L : ℕ) (τ C : ℝ) (w : ℕ → ℕ → ℝ) :
        Filter.Tendsto (fun N : ℕ =>
          (∑ n ∈ range N, arithmeticSubsetAmplification B L τ C w n) / (N : ℝ))
          Filter.atTop (nhds ((∑ a : ZMod (auxiliarySquarePeriod B),
            residueAmplification B L τ C w a) / (auxiliarySquarePeriod B : ℝ))) := by
    …

    Mentions: OAI.JointDickman.arithmeticSubsetAmplification, OAI.JointDickman.auxiliarySquarePeriod, OAI.JointDickman.residueAmplification