Lusin's theorem

A measurable map from a weakly regular measure space into a second-countable topological space is continuous off a set of arbitrarily small measure: for every measurable set s of finite measure and every ε > 0 there is a closed set F ⊆ s with μ (s \ F) < ε on which the map is continuous. This is Lusin's theorem. Its usual formulation with a compact set is the closed one followed by inner regularity by compact sets, and its usual hypothesis, a finite Borel measure on a Polish or metrizable space, is one of the regimes in which measures are weakly regular (Mathlib's MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_of_isFiniteMeasure); for such a measure the whole space is an admissible s, and μ (Set.univ \ F) is μ Fᶜ.

The proof approximates s itself, the part of s mapped into each member of a countable basis of the target, and the part of s mapped into its complement, from inside by closed sets, and intersects the resulting unions; on the intersection every basic preimage is relatively open. For an almost-everywhere measurable map, the set s is first shrunk by the null set on which the map differs from a measurable one. A strongly measurable map has separable range, which is second countable in a pseudometrizable target, so the theorem applies to it through its range.

The theorem is the bridge from measurability to topology in arguments about weak convergence of measures: it lets a Borel map be treated as a continuous one on a closed set carrying almost all of the mass, so that the portmanteau theorem, which only sees closed and open sets, applies to sets defined through the map. The almost-everywhere measurable version is included because the maps produced by ProbabilityTheory.HasLaw are only almost-everywhere measurable.

Main statements

• Measurable.exists_isClosed_measure_sdiff_lt_continuousOn — Lusin's theorem: a measurable map into a second-countable space is continuous on a closed subset of any measurable set s of finite measure whose complement in s has measure less than any prescribed ε > 0;
• AEMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn — the same for an almost-everywhere measurable map;
• MeasureTheory.StronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn and MeasureTheory.AEStronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn — the same for a strongly measurable, respectively almost-everywhere strongly measurable, map into a pseudometrizable space, with no measurable structure and no countability assumption on the target;
• TauCeti.exists_isClosed_measure_sdiff_lt_continuousOn_of_ae_eq — Lusin's conclusion transfers to an almost-everywhere equal map, which reduces each almost-everywhere version to its everywhere counterpart;
• LowerSemicontinuous.aemeasurable_comp_of_forall_exists_isClosed_continuousOn — a lower semicontinuous function of a map that is continuous on closed sets with arbitrarily small complement mass is almost-everywhere measurable.

References

• W. Rudin, Real and Complex Analysis, third edition, McGraw-Hill 1987, Theorem 2.24, the classical statement for locally compact Hausdorff spaces.
• D. H. Fremlin, Measure Theory, Volume 4, Torres Fremlin 2003, §418, Lusin's theorem for measurable functions into second-countable spaces from the inner regularity of the measure.

theorem TauCeti.exists_isClosed_measure_sdiff_lt_continuousOn_of_ae_eq {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] {μ : MeasureTheory.Measure X} {f g : X → Y} {s : Set X} {ε : ENNReal} (hfg : f =ᵐ[μ] g) (hs : MeasurableSet s) (hg : ∀ t ⊆ s, MeasurableSet t → ∃ F ⊆ t, IsClosed F ∧ μ (t \ F) < ε ∧ ContinuousOn g F) : ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn f F

Lusin's conclusion passes to a map almost everywhere equal to one for which it holds on every measurable subset of s: shrink s by a measurable null set containing the set where the two maps differ. No topological or measurable assumption on the target is needed.

theorem Measurable.exists_isClosed_measure_sdiff_lt_continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X} [μ.WeaklyRegular] {f : X → Y} {s : Set X} {ε : ENNReal} (hf : Measurable f) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hε : ε ≠ 0) : ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn f F

Lusin's theorem. A measurable map f from a weakly regular measure space into a second-countable topological space is continuous on a closed set F ⊆ s with μ (s \ F) < ε, for every measurable set s of finite measure and every ε > 0.

theorem AEMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] [TopologicalSpace Y] [SecondCountableTopology Y] [MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure X} [μ.WeaklyRegular] {f : X → Y} {s : Set X} {ε : ENNReal} (hf : AEMeasurable f μ) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hε : ε ≠ 0) : ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn f F

Lusin's theorem for an almost-everywhere measurable map: it is continuous on a closed set F ⊆ s with μ (s \ F) < ε, for every measurable set s of finite measure and every ε > 0.

A strongly measurable map has separable range, and a separable subset of a pseudometrizable space is second countable, so Lusin's theorem applies to it with no measurable structure and no countability assumption on the target.

theorem MeasureTheory.StronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : Measure X} [μ.WeaklyRegular] {s : Set X} {ε : ENNReal} {Z : Type u_3} [TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] {g : X → Z} (hg : StronglyMeasurable g) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hε : ε ≠ 0) : ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn g F

Lusin's theorem for a strongly measurable map into a pseudometrizable space: it is continuous on a closed set F ⊆ s with μ (s \ F) < ε, for every measurable set s of finite measure and every ε > 0. The target needs no measurable structure and need not be second countable.

theorem MeasureTheory.AEStronglyMeasurable.exists_isClosed_measure_sdiff_lt_continuousOn {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {μ : Measure X} [μ.WeaklyRegular] {s : Set X} {ε : ENNReal} {Z : Type u_3} [TopologicalSpace Z] [TopologicalSpace.PseudoMetrizableSpace Z] {g : X → Z} (hg : AEStronglyMeasurable g μ) (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (hε : ε ≠ 0) : ∃ F ⊆ s, IsClosed F ∧ μ (s \ F) < ε ∧ ContinuousOn g F

Lusin's theorem for an almost-everywhere strongly measurable map into a pseudometrizable space: it is continuous on a closed set F ⊆ s with μ (s \ F) < ε, for every measurable set s of finite measure and every ε > 0.

theorem LowerSemicontinuous.aemeasurable_comp_of_forall_exists_isClosed_continuousOn {Ω : Type u_3} {W : Type u_4} [TopologicalSpace Ω] [MeasurableSpace Ω] [OpensMeasurableSpace Ω] [TopologicalSpace W] {h : W → ENNReal} {Φ : Ω → W} {μ : MeasureTheory.Measure Ω} (hh : LowerSemicontinuous h) (hΦ : ∀ (ε : ENNReal), ε ≠ 0 → ∃ (C : Set Ω), IsClosed C ∧ ContinuousOn Φ C ∧ μ Cᶜ ≤ ε) : AEMeasurable (fun (x : Ω) => h (Φ x)) μ

A lower semicontinuous function of a map that is continuous on closed sets with arbitrarily small complement mass is almost-everywhere measurable: the map is continuous on countably many closed sets whose union is a full-measure set, and on each of them the composite is lower semicontinuous.