Null sets on manifolds

This file defines chartwise nullity for subsets of a charted manifold, without installing a measurable structure on the manifold itself. The definition is independent of the choice of Haar measure on the model and has the usual subset and countable-union closure properties. On a manifold with a finite-dimensional model a null set has empty interior, so its complement is dense; this is how Sard's theorem produces regular values.

Nullity of an image f '' s under a map between manifolds can be checked on coordinate expressions (TauCeti.isNullSet_image_of_forall_addHaar_image_extChartAt): when the source is Lindelöf, it suffices that every coordinate expression extChartAt J y₀ ∘ f ∘ (extChartAt I x₀).symm sends the chart image of the points of s seen by both charts to a Haar-null set. This is how Sard-type statements about maps between normed spaces pass to manifolds.

def TauCeti.IsNullSet {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [MeasurableSpace E] [hE : BorelSpace E] (s : Set M) : Prop

A set is null on a manifold when its image in every extended chart is null for every Haar measure on the model. This definition needs no measurable structure on the manifold itself.

theorem TauCeti.isNullSet_iff {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [MeasurableSpace E] [hE : BorelSpace E] (s : Set M) : IsNullSet I s ↔ ∀ (x : M) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure], μ (↑(extChartAt I x) '' (s ∩ (extChartAt I x).source)) = 0

The chartwise characterization of IsNullSet.

theorem TauCeti.IsNullSet.chartwise {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [MeasurableSpace E] [hE : BorelSpace E] {s : Set M} (hs : IsNullSet I s) (x : M) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] : μ (↑(extChartAt I x) '' (s ∩ (extChartAt I x).source)) = 0

The chartwise nullity statement for a null set at a point and Haar measure.

theorem TauCeti.IsNullSet.mono {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [MeasurableSpace E] [hE : BorelSpace E] {s t : Set M} (ht : IsNullSet I t) (hst : s ⊆ t) : IsNullSet I s

A subset of a null set is null.

theorem TauCeti.IsNullSet.union {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [MeasurableSpace E] [hE : BorelSpace E] {s t : Set M} (hs : IsNullSet I s) (ht : IsNullSet I t) : IsNullSet I (s ∪ t)

The union of two null sets is null.

theorem TauCeti.IsNullSet.iUnion {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [MeasurableSpace E] [hE : BorelSpace E] {ι : Sort u_4} [Countable ι] {s : ι → Set M} (hs : ∀ (i : ι), IsNullSet I (s i)) : IsNullSet I (⋃ (i : ι), s i)

A countable union of null sets is null.

theorem TauCeti.IsNullSet.biUnion {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [MeasurableSpace E] [hE : BorelSpace E] {ι : Type u_4} {t : Set ι} (ht : t.Countable) {s : ι → Set M} (hs : ∀ i ∈ t, IsNullSet I (s i)) : IsNullSet I (⋃ i ∈ t, s i)

A union of null sets indexed by a countable set is null.

theorem TauCeti.IsNullSet.interior_eq_empty {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set M} (hs : IsNullSet I s) : interior s = ∅

On a manifold with a finite-dimensional model, a null set has empty interior.

theorem TauCeti.IsNullSet.dense_compl {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {s : Set M} (hs : IsNullSet I s) : Dense sᶜ

On a manifold with a finite-dimensional model, the complement of a null set is dense.

theorem TauCeti.isNullSet_boundary {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [IsManifold I 1 M] : IsNullSet I (ModelWithCorners.boundary M)

The intrinsic boundary of any finite-dimensional real manifold is chartwise null. No measurable structure on the manifold itself is required.

theorem TauCeti.isNullSet_image_of_forall_addHaar_image_extChartAt {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [TopologicalSpace H] [TopologicalSpace M] [ChartedSpace H M] {E' : Type u_4} {H' : Type u_5} {N : Type u_6} [NormedAddCommGroup E'] [NormedSpace ℝ E'] [MeasurableSpace E'] [BorelSpace E'] [TopologicalSpace H'] [TopologicalSpace N] [ChartedSpace H' N] {I : ModelWithCorners ℝ E H} {J : ModelWithCorners ℝ E' H'} {f : M → N} {s : Set M} [LindelofSpace M] (h : ∀ (x₀ : M) (y₀ : N) (μ : MeasureTheory.Measure E') [μ.IsAddHaarMeasure], μ (↑(extChartAt J y₀) ∘ f ∘ ↑(extChartAt I x₀).symm '' ↑(extChartAt I x₀) '' (s ∩ (chartAt H x₀).source ∩ f ⁻¹' (chartAt H' y₀).source)) = 0) : IsNullSet J (f '' s)

Nullity of an image is read in coordinates. Let M be Lindelöf. Suppose that for every chart at x₀ of M and every chart at y₀ of N, the coordinate expression extChartAt J y₀ ∘ f ∘ (extChartAt I x₀).symm sends the chart image of the points of s lying in both charts to a set that is null for every Haar measure. Then f '' s is null in N.

No regularity of f is assumed, and both manifolds may have boundary or corners.