English
If an ergodic action by a group on a measure space yields that a subset is invariant under all actions up to a.e. equality, then the subset is ae-constant with respect to the measure.
Русский
Если группа действует эргодически и множество почти сохраняется под действием группы, тогда множество имеет константность почти во всех точках относительно меры.
LaTeX
$$$\forall G,\alpha,\mu: \text{ergodic action},\ s:\ Set\,\alpha,\ NullMeasurableSet\ s\ \mu \to (\forall g:\ G, (g\cdot\,)^{{-1}}'s =^\mathrm{a.e.}_\mu s) \to \ EventuallyConst\ s\ (ae\mu)$$$
Lean4
@[to_additive]
theorem aeconst_of_forall_preimage_smul_ae_eq [SMul G α] [ErgodicSMul G α μ] {s : Set α} (hm : NullMeasurableSet s μ)
(h : ∀ g : G, (g • ·) ⁻¹' s =ᵐ[μ] s) : EventuallyConst s (ae μ) :=
by
rcases hm with ⟨t, htm, hst⟩
refine .congr ?_ hst.symm
refine ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq htm fun g : G ↦ ?_
refine .trans (.trans ?_ (h g)) hst
exact tendsto_smul_ae _ _ hst.symm
