English
Under suitable regularity and convergence hypotheses, the measure of the symmetric difference between f_a^{-1}(s) and g^{-1}(s) tends to 0 as a tends to l.
Русский
При заданных условиях сходимости и регулярности меры мера симметрической разности предобразов стремится к нулю.
LaTeX
$$$$\\operatorname{Tendsto}\\limits_{a \\to l} \\mu((f(a)^{-1}(s))\\triangle (g^{-1}(s))) = 0.$$$$
Lean4
/-- 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 tendsto_measure_symmDiff_preimage_nhds_zero {l : Filter α} {f : α → C(X, Y)} {g : C(X, Y)} {s : Set Y}
(hfg : Tendsto f l (𝓝 g)) (hf : ∀ᶠ a in l, MeasurePreserving (f a) μ ν) (hg : MeasurePreserving g μ ν)
(hs : NullMeasurableSet s ν) (hνs : ν s ≠ ∞) : Tendsto (fun a ↦ μ ((f a ⁻¹' s) ∆ (g ⁻¹' s))) l (𝓝 0) :=
by
have : ν.InnerRegularCompactLTTop := by
rw [← hg.map_eq]
exact .map_of_continuous (map_continuous _)
rw [ENNReal.tendsto_nhds_zero]
intro ε hε
wlog hso : IsOpen s generalizing s ε
· have H : 0 < ε / 3 := ENNReal.div_pos hε.ne' ENNReal.coe_ne_top
rcases hs.exists_isOpen_symmDiff_lt hνs H.ne' with ⟨U, hUo, hU, hUs⟩
have hmU : NullMeasurableSet U ν := hUo.measurableSet.nullMeasurableSet
replace hUs := hUs.le
filter_upwards [hf, this hmU hU.ne _ H hUo] with a hfa ha
calc
μ ((f a ⁻¹' s) ∆ (g ⁻¹' s)) ≤
μ ((f a ⁻¹' s) ∆ (f a ⁻¹' U)) + μ ((f a ⁻¹' U) ∆ (g ⁻¹' U)) + μ ((g ⁻¹' U) ∆ (g ⁻¹' s)) :=
by
refine (measure_symmDiff_le _ (g ⁻¹' U) _).trans ?_
gcongr
apply measure_symmDiff_le
_ ≤ ε / 3 + ε / 3 + ε / 3 := by
gcongr
· rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
· rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]
_ = ε := by
simp
-- Take a compact closed subset `K ⊆ g ⁻¹' s` of almost full measure,
-- `μ (g ⁻¹' s \ K) < ε / 2`.
have hνs' : μ (g ⁻¹' s) ≠ ∞ := by rwa [hg.measure_preimage hs]
obtain ⟨K, hKg, hKco, hKcl, hKμ⟩ : ∃ K, MapsTo g K s ∧ IsCompact K ∧ IsClosed K ∧ μ (g ⁻¹' s \ K) < ε / 2 :=
(hg.measurable hso.measurableSet).exists_isCompact_isClosed_diff_lt hνs' <| by simp [hε.ne']
have hKm : NullMeasurableSet K μ := hKcl.nullMeasurableSet
filter_upwards [hf, ContinuousMap.tendsto_nhds_compactOpen.mp hfg K hKco s hso hKg] with a hfa ha
rw [← ENNReal.add_halves ε]
refine (measure_symmDiff_le _ K _).trans ?_
rw [symmDiff_of_ge ha.subset_preimage, symmDiff_of_le hKg.subset_preimage]
gcongr
have hK' : μ K ≠ ∞ := ne_top_of_le_ne_top hνs' <| measure_mono hKg.subset_preimage
rw [measure_diff_le_iff_le_add hKm ha.subset_preimage hK', hfa.measure_preimage hs, ← hg.measure_preimage hs, ←
measure_diff_le_iff_le_add hKm hKg.subset_preimage hK']
exact hKμ.le
