English
If G is finite, and t is invariant under G, then the measure of t equals the cardinality of G times the measure of t ∩ s.
Русский
Если G конечна и t инвариантна относительно G, то μ(t) = |G| · μ(t ∩ s).
LaTeX
$$$$\\mu t = |G| \\cdot \\mu(t \\cap s).$$$$
Lean4
/-- Given a measure space with an action of a finite group `G`, the measure of any `G`-invariant set
is determined by the measure of its intersection with a fundamental domain for the action of `G`. -/
@[to_additive measure_eq_card_smul_of_vadd_ae_eq_self /-- Given a measure space with an action of a
finite additive group `G`, the measure of any `G`-invariant set is determined by the measure of
its intersection with a fundamental domain for the action of `G`. -/
]
theorem measure_eq_card_smul_of_smul_ae_eq_self [Finite G] (h : IsFundamentalDomain G s μ) (t : Set α)
(ht : ∀ g : G, (g • t : Set α) =ᵐ[μ] t) : μ t = Nat.card G • μ (t ∩ s) :=
by
haveI : Fintype G := Fintype.ofFinite G
rw [h.measure_eq_tsum]
replace ht : ∀ g : G, (g • t ∩ s : Set α) =ᵐ[μ] (t ∩ s : Set α) := fun g => ae_eq_set_inter (ht g) (ae_eq_refl s)
simp_rw [measure_congr (ht _), tsum_fintype, Finset.sum_const, Nat.card_eq_fintype_card, Finset.card_univ]
