English
If a group G acts ergodically on X with μ finite and inner regular, and s is null-measurable with a.s. invariance under all smuls, then s is ae-constant.
Русский
Пусть G действует эргодически на X с мерой μ, конечной и внутренне регулярной. Если s нуль-измеримо и сохраняется под действием всех скалярных умножений на a.e., то s — ae-константа.
LaTeX
$$$\forall G,X,μ\,[Group\,G]\,[MulAction\,G\ X]\ [IsFiniteMeasure\ μ]\ [μ.InnerRegular]\ {s: Set X}, NullMeasurableSet\ s\ μ \to (\forall g:\ G, (ae\, μ)\ EventuallyEq\ (instHSMul.hMul g\ s)\ s) \to \ Filter.EventuallyConst\ s\ (ae\ μ)$$$
Lean4
@[to_additive]
theorem aeconst_of_forall_smul_ae_eq (hm : NullMeasurableSet s μ) (h : ∀ g : G, g • s =ᵐ[μ] s) :
EventuallyConst s (ae μ) :=
aeconst_of_forall_preimage_smul_ae_eq G hm fun g ↦ by simpa only [preimage_smul] using h g⁻¹
