PeriodicAverages.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Finite periodic averages and coprime residue factorization

Integer averages of a function on ZMod q converge to its uniform residue mean. The proof is the exact complete-block/remainder identity. The Chinese remainder equivalence then gives factorization for fixed coprime moduli.

def OAI.JointDickman.periodicAverage line 20
def OAI.JointDickman.residueMean line 23
def OAI.JointDickman.residueEquiv line 26
theorem OAI.JointDickman.residue_sum_eq_range line 32

theorem OAI.JointDickman.periodic_sum_blocks line 40

Source documentation

Complete blocks have exactly the same sum, with an unaltered final prefix. This equality also holds when the modulus is zero.

theorem periodic_sum_blocks {q : ℕ} (f : ZMod q → ℂ) (k r : ℕ) :
    (∑ n ∈ Finset.range (k * q + r), f (n : ZMod q)) =
      (k : ℂ) * (∑ n ∈ Finset.range q, f (n : ZMod q)) +
        ∑ n ∈ Finset.range r, f (n : ZMod q) := by
…

theorem OAI.JointDickman.periodic_sum_div_mod line 59
theorem OAI.JointDickman.prefix_centered_bound line 67
theorem OAI.JointDickman.periodicAverage_error line 112
Source documentation
The remainder error is at most one period times the uniform norm, divided by the averaging length.
```
theorem periodicAverage_error {q : ℕ} [NeZero q] (f : ZMod q → ℂ)
    {N : ℕ} (hN : 0 < N) :
    ‖periodicAverage f N - residueMean f‖ ≤ (q : ℝ) * ‖f‖ / N := by
…
```
Mentions: OAI.JointDickman.periodicAverage, OAI.JointDickman.residueMean
theorem OAI.JointDickman.periodicAverage_tendsto line 135

theorem OAI.JointDickman.residueMean_crt line 144

Source documentation

Chinese remaindering factors the exact uniform mean at coprime moduli.

theorem residueMean_crt {m q : ℕ} [NeZero m] [NeZero q]
    (hmq : m.Coprime q) (f : ZMod m → ℂ) (g : ZMod q → ℂ) :
    residueMean (fun a : ZMod (m * q) =>
      f ((ZMod.chineseRemainder hmq) a).1 * g ((ZMod.chineseRemainder hmq) a).2) =
      residueMean f * residueMean g := by
…

Mentions: OAI.JointDickman.residueMean

theorem OAI.JointDickman.coprime_residue_average_tendsto line 160

Source documentation

Integer averages of two fixed coprime residue tests factor in the limit.

theorem coprime_residue_average_tendsto {m q : ℕ} [NeZero m] [NeZero q]
    (hmq : m.Coprime q) (f : ZMod m → ℂ) (g : ZMod q → ℂ) :
    Tendsto (fun N : ℕ => (∑ n ∈ Finset.range N,
      f (n : ZMod m) * g (n : ZMod q)) / N)
      atTop (𝓝 (residueMean f * residueMean g)) := by
…

Mentions: OAI.JointDickman.residueMean