English
If f is invariant under G and hs ht are fundamental domains, then f is aestronglyMeasurable with respect to μ restricted to s if and only if it is with respect to μ restricted to t.
Русский
Если f инвариантна по G и hs ht — фундаментальные области, то f измеримо относительно μ|s тогда и только тогда относительно μ|t.
LaTeX
$$$$\\text{AEStronglyMeasurable}(f, \\mu|_s) \\iff \\text{AEStronglyMeasurable}(f, \\mu|_t).$$$$
Lean4
/-- If the action of a countable group `G` admits an invariant measure `μ` with a fundamental domain
`s`, then every null-measurable set `t` such that the sets `g • t ∩ s` are pairwise a.e.-disjoint
has measure at most `μ s`. -/
@[to_additive /-- If the additive action of a countable group `G` admits an invariant measure `μ`
with a fundamental domain `s`, then every null-measurable set `t` such that the sets `g +ᵥ t ∩ s`
are pairwise a.e.-disjoint has measure at most `μ s`. -/
]
theorem measure_le_of_pairwise_disjoint (hs : IsFundamentalDomain G s μ) (ht : NullMeasurableSet t μ)
(hd : Pairwise (AEDisjoint μ on fun g : G => g • t ∩ s)) : μ t ≤ μ s :=
calc
μ t = ∑' g : G, μ (g • t ∩ s) := hs.measure_eq_tsum t
_ = μ (⋃ g : G, g • t ∩ s) := (Eq.symm <| measure_iUnion₀ hd fun _ => (ht.smul _).inter hs.nullMeasurableSet)
_ ≤ μ s := measure_mono (iUnion_subset fun _ => inter_subset_right)
