Continuity of the preimage of a set under a measure preserving continuous function

In this file we prove that the preimage of a null measurable set s : Set Y under a measure preserving continuous function f : C(X, Y) is continuous in f in the sense that μ ((f a ⁻¹' s) ∆ (g ⁻¹' s)) tends to zero as f a tends to g.

As a corollary, we show that for a continuous family of continuous maps f z : C(X, Y), a null measurable set s, and a null measurable set t of finite measure, the set of parameters z such that f z ⁻¹' t is a.e. equal to s is a closed set.

theorem MeasureTheory.tendsto_measure_symmDiff_preimage_nhds_zero {α : Type u_1} {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {l : Filter α} {f : α → C(X, Y)} {g : C(X, Y)} {s : Set Y} (hfg : Filter.Tendsto f l (nhds g)) (hf : ∀ᶠ (a : α) in l, MeasureTheory.MeasurePreserving (⇑(f a)) μ ν) (hg : MeasureTheory.MeasurePreserving (⇑g) μ ν) (hs : MeasureTheory.NullMeasurableSet s ν) (hνs : ν s ≠ ⊤) : Filter.Tendsto (fun (a : α) => μ (symmDiff (⇑(f a) ⁻¹' s) (⇑g ⁻¹' s))) l (nhds 0)

Let X and Y be R₁ topological spaces with Borel σ-algebras and measures μ and ν, respectively. Suppose that μ is inner regular for finite measure sets with respect to compact sets and ν is a locally finite measure. Let f : α → C(X, Y) be a family of continuous maps that converges to a continuous map g : C(X, Y) in the compact-open topology along a filter l. Suppose that g is a measure preserving map and f a is a measure preserving map eventually along l. Then for any finite measure measurable set s, the preimages f a ⁻¹' s tend to the preimage g ⁻¹' s in measure. More precisely, the measure of the symmetric difference of these two sets tends to zero.

theorem MeasureTheory.isClosed_setOf_preimage_ae_eq {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [R1Space X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] [R1Space Y] [TopologicalSpace Z] {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure ν] {f : Z → C(X, Y)} (hf : Continuous f) (hfm : ∀ (z : Z), MeasureTheory.MeasurePreserving (⇑(f z)) μ ν) (s : Set X) {t : Set Y} (htm : MeasureTheory.NullMeasurableSet t ν) (ht : ν t ≠ ⊤) : IsClosed {z : Z | ⇑(f z) ⁻¹' t =ᵐ[μ] s}

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.