sum_restrict_of_ac — Mathlib

English

For a fundamental domain h, the sum of μ.restrict (g • s) over g ∈ G equals μ: sum_g μ|_{g•s} = μ.

Русский

Для фундаментальной области h сумма μ ограниченная на каждый перенос g•s равна μ: сумма по g ∈ G μ|_{g•s} = μ.

LaTeX

$$$\\sum_{g\\in G} μ\\restriction (g\\cdot s) = μ$$$

Lean4

@[to_additive]
theorem sum_restrict_of_ac (h : IsFundamentalDomain G s μ) (hν : ν ≪ μ) : (sum fun g : G => ν.restrict (g • s)) = ν :=
  by
  rw [← restrict_iUnion_ae (h.aedisjoint.mono fun i j h => hν h) fun g => (h.nullMeasurableSet_smul g).mono_ac hν,
    restrict_congr_set (hν h.iUnion_smul_ae_eq), restrict_univ]

Похожие утверждения