Support of a Measure

This file develops the theory of the support of a measure μ on a topological measurable space. The support is defined as the set of points whose every open neighborhood has positive measure. We give equivalent characterizations, prove basic measure-theoretic properties, and study interactions with sums, restrictions, and absolute continuity. Under various Lindelöf conditions, the support is conull, and various descriptions of the complement of the support are provided.

Main definitions

• Measure.support : the support of a measure μ, defined as {x | ∃ᶠ u in (𝓝 x).smallSets, 0 < μ u} — equivalently, every neighborhood of x has positive μ-measure.

Main results

• compl_support_eq_sUnion and support_eq_sInter : the complement of the support is the union of open measure-zero sets, and the support is the intersection of closed sets whose complements have measure zero.
• isClosed_support : the support is a closed set.
• support_mem_ae_of_isLindelof and support_mem_ae : under Lindelöf (or hereditarily Lindelöf) hypotheses, the support is conull.

Tags

measure, support, Lindelöf

def MeasureTheory.Measure.support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (μ : Measure X) : Set X

A point x is in the support of μ if any open neighborhood of x has positive measure. We provide the definition in terms of the filter-theoretic equivalent ∃ᶠ u in (𝓝 x).smallSets, 0 < μ u.

Equations

• μ.support = {x : X | ∃ᶠ (u : Set X) in (nhds x).smallSets, 0 < μ u}

theorem Filter.HasBasis.mem_measureSupport {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set X} {x : X} (hl : (nhds x).HasBasis p s) : x ∈ μ.support ↔ ∀ (i : ι), p i → 0 < μ (s i)

theorem MeasureTheory.Measure.mem_support_iff {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} {x : X} : x ∈ μ.support ↔ ∃ᶠ (u : Set X) in (nhds x).smallSets, 0 < μ u

A point x is in the support of measure μ iff any neighborhood of x contains a subset with positive measure.

theorem MeasureTheory.Measure.mem_support_iff_forall {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} (x : X) : x ∈ μ.support ↔ ∀ U ∈ nhds x, 0 < μ U

A point x is in the support of measure μ iff every neighborhood of x has positive measure.

theorem MeasureTheory.Measure.support_eq_univ {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [μ.IsOpenPosMeasure] : μ.support = Set.univ

theorem MeasureTheory.Measure.AbsolutelyContinuous.support_mono {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ ν : Measure X} (hμν : μ.AbsolutelyContinuous ν) : μ.support ⊆ ν.support

theorem MeasureTheory.Measure.support_mono {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ ν : Measure X} (h : μ ≤ ν) : μ.support ⊆ ν.support

theorem MeasureTheory.Measure.notMem_support_iff {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} {x : X} : x ∉ μ.support ↔ ∀ᶠ (u : Set X) in (nhds x).smallSets, μ u = 0

A point x lies outside the support of μ iff all of the subsets of one of its neighborhoods have measure zero.

theorem Filter.HasBasis.notMem_measureSupport {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : MeasureTheory.Measure X} {ι : Sort u_2} {p : ι → Prop} {s : ι → Set X} {x : X} (hl : (nhds x).HasBasis p s) : x ∉ μ.support ↔ ∃ (i : ι), p i ∧ μ (s i) = 0

@[simp]

theorem MeasureTheory.Measure.support_zero {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] : Measure.support 0 = ∅

theorem MeasureTheory.Measure.support_add {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] (μ ν : Measure X) : (μ + ν).support = μ.support ∪ ν.support

The support of the sum of two measures is the union of the supports.

theorem MeasureTheory.Measure.notMem_support_iff_exists {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} {x : X} : x ∉ μ.support ↔ ∃ U ∈ nhds x, μ U = 0

A point x lies outside the support of μ iff some neighborhood of x has measure zero.

theorem MeasureTheory.Measure.support_eq_forall_isOpen {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} : μ.support = {x : X | ∀ (u : Set X), x ∈ u → IsOpen u → 0 < μ u}

The support of a measure equals the set of points whose open neighborhoods all have positive measure.

theorem MeasureTheory.Measure.isClosed_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} : IsClosed μ.support

theorem MeasureTheory.Measure.isOpen_compl_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} : IsOpen μ.supportᶜ

theorem MeasureTheory.Measure.subset_compl_support_of_isOpen {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} {t : Set X} (ht : IsOpen t) (h : μ t = 0) : t ⊆ μ.supportᶜ

theorem MeasureTheory.Measure.support_subset_of_isClosed {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} {t : Set X} (ht : IsClosed t) (h : t ∈ ae μ) : μ.support ⊆ t

theorem MeasureTheory.Measure.compl_support_eq_sUnion {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} : μ.supportᶜ = ⋃₀ {t : Set X | IsOpen t ∧ μ t = 0}

theorem MeasureTheory.Measure.support_eq_sInter {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} : μ.support = ⋂₀ {t : Set X | IsClosed t ∧ μ tᶜ = 0}

theorem MeasureTheory.Measure.support_mem_ae_of_isLindelof {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} (h : IsLindelof μ.supportᶜ) : μ.support ∈ ae μ

If the complement of the support is Lindelöf, then the support of a measure is conull.

theorem MeasureTheory.Measure.support_mem_ae {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [HereditarilyLindelofSpace X] : μ.support ∈ ae μ

In a hereditarily Lindelöf space, the support of a measure is conull.

@[simp]

theorem MeasureTheory.Measure.measure_compl_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [HereditarilyLindelofSpace X] : μ μ.supportᶜ = 0

theorem MeasureTheory.Measure.nonempty_inter_support_of_pos {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [HereditarilyLindelofSpace X] {s : Set X} (hμ : 0 < μ s) : (s ∩ μ.support).Nonempty

theorem MeasureTheory.Measure.nullMeasurableSet_compl_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [HereditarilyLindelofSpace X] : NullMeasurableSet μ.supportᶜ μ

Under the assumption OpensMeasurableSpace, this is redundant because the complement of the support is open, and therefore measurable.

theorem MeasureTheory.Measure.nullMeasurableSet_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [HereditarilyLindelofSpace X] : NullMeasurableSet μ.support μ

Under the assumption OpensMeasurableSpace, this is redundant because the support is closed, and therefore measurable.

theorem MeasureTheory.Measure.nonempty_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [HereditarilyLindelofSpace X] (hμ : μ ≠ 0) : μ.support.Nonempty

theorem MeasureTheory.Measure.nonempty_support_iff {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [HereditarilyLindelofSpace X] : μ.support.Nonempty ↔ μ ≠ 0

theorem MeasureTheory.Measure.mem_support_restrict {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [OpensMeasurableSpace X] {s : Set X} {x : X} : x ∈ (μ.restrict s).support ↔ ∃ᶠ (u : Set X) in (nhdsWithin x s).smallSets, 0 < μ u

theorem MeasureTheory.Measure.interior_inter_support {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [OpensMeasurableSpace X] {s : Set X} : interior s ∩ μ.support ⊆ (μ.restrict s).support

theorem MeasureTheory.Measure.support_restrict_subset {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] {μ : Measure X} [OpensMeasurableSpace X] {s : Set X} : (μ.restrict s).support ⊆ closure s ∩ μ.support