Topological support on discrete spaces and under restriction, products, scalar multiplication

and maps

This file characterizes support by singleton masses on discrete spaces, and identifies the support of restriction to an open set for a measure positive on nonempty open sets, the support of a nonzero scalar multiple of a measure, and the support of a pushforward by a continuous map. It also shows that pushing a measure forward along a homeomorphism transports its topological support onto the image of the original support. Finite products have the product of the supports of their factors. A measurable map that is continuous at a source support point sends that point into the support of the pushforward; global continuity is unnecessary for this inclusion.

Main result

• MeasureTheory.Measure.mem_support_iff_measure_singleton_pos — on a discrete space, support membership is equivalent to positive singleton mass.
• MeasureTheory.Measure.support_eq_setOf_singleton_ne_zero — on a discrete space, the support consists exactly of the points with nonzero singleton mass.
• MeasureTheory.Measure.support_smul_measure — multiplying a measure by a nonzero scalar preserves its support.
• MeasureTheory.Measure.support_restrict_of_isOpen — restricting a measure positive on nonempty open sets to an open set gives support equal to that set's closure.
• MeasureTheory.Measure.support_map_eq_closure_image — a continuous pushforward has support equal to the closure of the image of the support, when the source support has full measure.
• MeasureTheory.Measure.support_map_eq_closure_range — a continuous image of a full-support measure has support equal to the closure of the map's range.
• MeasureTheory.Measure.support_map_homeomorph — the support of a pushforward by a homeomorphism is the image of the original support.

@[simp]

theorem MeasureTheory.Measure.mem_support_iff_measure_singleton_pos {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] [MeasurableSpace X] {μ : Measure X} {x : X} : x ∈ μ.support ↔ 0 < μ {x}

On a discrete space, a point belongs to the support exactly when its singleton has positive mass. No compatibility between the measurable structure and topology is needed.

theorem MeasureTheory.Measure.support_eq_setOf_singleton_ne_zero {X : Type u_1} [TopologicalSpace X] [DiscreteTopology X] [MeasurableSpace X] (μ : Measure X) : μ.support = {x : X | μ {x} ≠ 0}

On a discrete topological space, the support of a measure consists exactly of the points with nonzero singleton mass.

@[simp]

theorem MeasureTheory.Measure.support_pi {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → TopologicalSpace (α i)] [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → Measure (α i)) [∀ (i : ι), SigmaFinite (μ i)] : (Measure.pi μ).support = Set.univ.pi fun (i : ι) => (μ i).support

The support of a finite product of sigma-finite measures is the product of their supports. No compatibility between the topologies and measurable structures is needed.

theorem MeasureTheory.Measure.mem_support_map_of_continuousAt {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [TopologicalSpace Y] [MeasurableSpace Y] {μ : Measure X} {f : X → Y} {x : X} (hf : AEMeasurable f μ) (hfx : ContinuousAt f x) (hx : x ∈ μ.support) : f x ∈ (map f μ).support

A measurable map continuous at a source support point sends it into the support of the pushforward, even if the map is discontinuous elsewhere.

theorem MeasureTheory.Measure.support_smul_measure {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (c : ENNReal) (μ : Measure X) (hc : c ≠ 0) : (c • μ).support = μ.support

Multiplying a measure by a nonzero ℝ≥0∞ scalar preserves its topological support.

@[simp]

theorem MeasureTheory.Measure.support_restrict_of_isOpen {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] (μ : Measure X) [μ.IsOpenPosMeasure] {s : Set X} (hs : IsOpen s) : (μ.restrict s).support = closure s

Restricting a measure positive on nonempty open sets to an open set gives support equal to the closure of that set.

theorem MeasureTheory.Measure.support_map_eq_closure_image {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ : Measure X) (hμ : μ.support ∈ ae μ) {f : X → Y} (hf : Continuous f) : (map f μ).support = closure (f '' μ.support)

The support of a continuous pushforward is the closure of the image of the support, provided that the source support has full measure.

theorem MeasureTheory.Measure.support_map_eq_closure_range {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ : Measure X) {f : X → Y} (hμ : μ.support = Set.univ) (hf : Continuous f) : (map f μ).support = closure (Set.range f)

The support of the pushforward of a full-support measure by a continuous map is the closure of the map's range. No injectivity, surjectivity, or properness hypothesis is needed.

theorem MeasureTheory.Measure.support_map_homeomorph {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [MeasurableSpace X] [BorelSpace X] [TopologicalSpace Y] [MeasurableSpace Y] [BorelSpace Y] (μ : Measure X) (e : X ≃ₜ Y) : (map (⇑e) μ).support = ⇑e '' μ.support

A homeomorphism carries the support of a measure onto the support of its pushforward.