English
If f is invariant under a countable group G, essSup f μ|s equals essSup f μ on the fundamental domain s.
Русский
Если f инвариантна по счетной группе G, essSup f μ|s равно essSup f μ на фундаментальной области s.
LaTeX
$$$$\\operatorname{essSup} f (\\mu|_s) = \\operatorname{essSup} f \\mu.$$$$
Lean4
/-- If `f` is invariant under the action of a countable group `G`, and `μ` is a `G`-invariant
measure with a fundamental domain `s`, then the `essSup` of `f` restricted to `s` is the same as
that of `f` on all of its domain. -/
@[to_additive /-- If `f` is invariant under the action of a countable additive group `G`, and `μ`
is a `G`-invariant measure with a fundamental domain `s`, then the `essSup` of `f` restricted to
`s` is the same as that of `f` on all of its domain. -/
]
theorem essSup_measure_restrict (hs : IsFundamentalDomain G s μ) {f : α → ℝ≥0∞}
(hf : ∀ γ : G, ∀ x : α, f (γ • x) = f x) : essSup f (μ.restrict s) = essSup f μ :=
by
refine le_antisymm (essSup_mono_measure' Measure.restrict_le_self) ?_
rw [essSup_eq_sInf (μ.restrict s) f, essSup_eq_sInf μ f]
refine sInf_le_sInf ?_
rintro a (ha : (μ.restrict s) {x : α | a < f x} = 0)
rw [Measure.restrict_apply₀' hs.nullMeasurableSet] at ha
refine measure_zero_of_invariant hs _ ?_ ha
intro γ
ext x
rw [mem_smul_set_iff_inv_smul_mem]
simp only [mem_setOf_eq, hf γ⁻¹ x]
