English
For a family of measure-preserving maps f_z, the set { z | f_z^{-1}(t) =ᵐ s } is closed in Z.
Русский
Множество { z | f_z^{-1}(t) =ᵐ s } замкнуто в Z.
LaTeX
$$$$\\{ z : f_z^{-1}(t) =^{a.e.}_{\\mu} s \\} \\text{ is closed in } Z.$$$$
Lean4
/-- Let `f : Z → C(X, Y)` be a continuous (in the compact open topology) family
of continuous measure-preserving maps.
Let `t : Set Y` be a null measurable set of finite measure.
Then for any `s`, the set of parameters `z`
such that the preimage of `t` under `f_z` is a.e. equal to `s`
is a closed set.
In particular, if `X = Y` and `s = t`,
then we see that the a.e. stabilizer of a set is a closed set. -/
theorem isClosed_setOf_preimage_ae_eq {f : Z → C(X, Y)} (hf : Continuous f) (hfm : ∀ z, MeasurePreserving (f z) μ ν)
(s : Set X) {t : Set Y} (htm : NullMeasurableSet t ν) (ht : ν t ≠ ∞) : IsClosed {z | f z ⁻¹' t =ᵐ[μ] s} :=
by
rw [← isOpen_compl_iff, isOpen_iff_mem_nhds]
intro z hz
replace hz : ∀ᶠ ε : ℝ≥0∞ in 𝓝 0, ε < μ ((f z ⁻¹' t) ∆ s) :=
by
apply gt_mem_nhds
rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]
filter_upwards [(tendsto_measure_symmDiff_preimage_nhds_zero (hf.tendsto z) (.of_forall hfm) (hfm z) htm
ht).eventually
hz] with
w hw
intro (hw' : f w ⁻¹' t =ᵐ[μ] s)
rw [measure_congr (hw'.symmDiff (ae_eq_refl _)), symmDiff_comm] at hw
exact hw.false
