CRTResidueAverage.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Exact independent residue averages from the Chinese remainder theorem

def OAI.Ostmann.crtUnitEquiv line 16

Source documentation

CRT on the actual unit residue classes, including prime-square moduli.

noncomputable def crtUnitEquiv {I : Type*} [Fintype I] (a : I → ℕ)
    (hc : Pairwise (fun i j => (a i).Coprime (a j))) :
    (ZMod (∏ i, a i))ˣ ≃* (∀ i, (ZMod (a i))ˣ) :=
…

theorem OAI.Ostmann.crtUnitEquiv_apply line 21

theorem OAI.Ostmann.crt_unit_average line 32

Source documentation

Uniform CRT unit residues factor exactly into independent local uniform unit residues; no equidistribution hypothesis is used in this finite step.

theorem crt_unit_average {I : Type*} [Fintype I] [DecidableEq I]
    (a : I → ℕ) [∀ i, NeZero (a i)] [NeZero (∏ i, a i)]
    (hc : Pairwise (fun i j => (a i).Coprime (a j)))
    (f : ∀ i, (ZMod (a i))ˣ → ℝ) :
    (Fintype.card (ZMod (∏ i, a i))ˣ : ℝ)⁻¹ *
      (∑ u : (ZMod (∏ i, a i))ˣ, ∏ i, f i (crtUnitEquiv a hc u i)) =
    ∏ i, (Fintype.card (ZMod (a i))ˣ : ℝ)⁻¹ * ∑ u : (ZMod (a i))ˣ, f i u := by
…

Mentions: OAI.Ostmann.crtUnitEquiv