English
If the preimages under a dense family of smul-actions preserve a set up to a.e. equality, then the set is ae-constant.
Русский
Если множество почти сохраняется под действием скалярного умножения на элементы из плотного множества групп, то оно ae-константно.
LaTeX
$$$\text{aeconst\_of\_dense\_setOf\_preimage\_smul\_ae}\ (S)\ (hsm) (hd)$$$
Lean4
/-- Let `M` act continuously on an R₁ topological space `X`.
Let `μ` be a finite inner regular measure on `X` which is ergodic with respect to this action.
If a null measurable set `s` is a.e. equal
to its preimages under the action of a dense set of elements of `M`,
then it is either null or conull. -/
@[to_additive /-- Let `M` act continuously on an R₁ topological space `X`.
Let `μ` be a finite inner regular measure on `X` which is ergodic with respect to this action.
If a null measurable set `s` is a.e. equal
to its preimages under the action of a dense set of elements of `M`,
then it is either null or conull. -/
]
theorem aeconst_of_dense_setOf_preimage_smul_ae (hsm : NullMeasurableSet s μ)
(hd : Dense {g : M | (g • ·) ⁻¹' s =ᵐ[μ] s}) : EventuallyConst s (ae μ) :=
by
borelize M
refine aeconst_of_forall_preimage_smul_ae_eq M hsm ?_
rwa [dense_iff_closure_eq, IsClosed.closure_eq, eq_univ_iff_forall] at hd
let f : C(M × X, X) := ⟨(· • ·).uncurry, continuous_smul⟩
exact isClosed_setOf_preimage_ae_eq f.curry.continuous (measurePreserving_smul · μ) _ hsm (measure_ne_top _ _)
