ResidueQuotientMean.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform residue means descend to every divisor of the period

theorem OAI.JointDickman.periodic_mean_at_multiple line 11

Source documentation

A whole number of periods has exactly the uniform residue mean.

theorem periodic_mean_at_multiple {d q : ℕ} [NeZero d] (hq : 0 < q)
    (hd : d ∣ q) (F : ZMod d → ℝ) :
    (∑ n ∈ range q, F n) / (q : ℝ) = (∑ a : ZMod d, F a) / (d : ℝ) := by
…

theorem OAI.JointDickman.residue_quotient_mean line 31

Source documentation

Taking a representative and reducing modulo a divisor preserves the uniform law, with all fibers having equal size.

theorem residue_quotient_mean {d q : ℕ} [NeZero d] [NeZero q]
    (hd : d ∣ q) (F : ZMod d → ℝ) :
    (∑ a : ZMod q, F (a.val : ZMod d)) / (q : ℝ) =
      (∑ a : ZMod d, F a) / (d : ℝ) := by
…