Everywhere positive sets in measure spaces

A set s in a topological space with a measure μ is everywhere positive (also called self-supporting) if any neighborhood n of any point of s satisfies μ (s ∩ n) > 0.

Main definitions and results

• μ.IsEverywherePos s registers that, for any point in s, all its neighborhoods have positive measure inside s.
• μ.everywherePosSubset s is the subset of s made of those points all of whose neighborhoods have positive measure inside s.
• everywherePosSubset_ae_eq shows that s and μ.everywherePosSubset s coincide almost everywhere if μ is inner regular and s is measurable.
• isEverywherePos_everywherePosSubset shows that μ.everywherePosSubset s satisfies the property μ.IsEverywherePos if μ is inner regular and s is measurable.

The latter two statements have also versions when μ is inner regular for finite measure sets, assuming additionally that s has finite measure.

• IsEverywherePos.IsGδ proves that an everywhere positive compact closed set is a Gδ set, in a topological group with a left-invariant measure. This is a nontrivial statement, used crucially in the study of the uniqueness of Haar measures.
• innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top: for a Haar measure, any finite measure set can be approximated from inside by level sets of continuous compactly supported functions. This property is also known as completion-regularity of Haar measures.

def MeasureTheory.Measure.IsEverywherePos {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : Prop

A set s is everywhere positive (also called self-supporting) with respect to a measure μ if it has positive measure around each of its points, i.e., if all neighborhoods n of points of s satisfy μ (s ∩ n) > 0.

Equations

• μ.IsEverywherePos s = ∀ x ∈ s, ∀ n ∈ nhdsWithin x s, 0 < ↑↑μ n

def MeasureTheory.Measure.everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : Set α

• The everywhere positive subset of a set is the subset made of those points all of whose neighborhoods have positive measure inside the set.

Equations

• μ.everywherePosSubset s = {x : α | x ∈ s ∧ ∀ n ∈ nhdsWithin x s, 0 < ↑↑μ n}

theorem MeasureTheory.Measure.everywherePosSubset_subset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : μ.everywherePosSubset s ⊆ s

theorem MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α) : ∃ (u : Set α), IsOpen u ∧ μ.everywherePosSubset s = s \ u

The everywhere positive subset of a set is obtained by removing an open set.

theorem MeasurableSet.everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [OpensMeasurableSpace α] (hs : MeasurableSet s) : MeasurableSet (μ.everywherePosSubset s)

theorem IsClosed.everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : IsClosed s) : IsClosed (μ.everywherePosSubset s)

theorem IsCompact.everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : IsCompact s) : IsCompact (μ.everywherePosSubset s)

theorem MeasureTheory.Measure.measure_eq_zero_of_subset_diff_everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {k : Set α} (hk : IsCompact k) (h'k : k ⊆ s \ μ.everywherePosSubset s) : ↑↑μ k = 0

Any compact set contained in s \ μ.everywherePosSubset s has zero measure.

theorem MeasureTheory.Measure.everywherePosSubset_ae_eq {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [OpensMeasurableSpace α] [MeasureTheory.Measure.InnerRegular μ] (hs : MeasurableSet s) : μ.everywherePosSubset s =ᶠ[MeasureTheory.Measure.ae μ] s

In a space with an inner regular measure, any measurable set coincides almost everywhere with its everywhere positive subset.

theorem MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_top {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [OpensMeasurableSpace α] [MeasureTheory.Measure.InnerRegularCompactLTTop μ] (hs : MeasurableSet s) (h's : ↑↑μ s ≠ ⊤) : μ.everywherePosSubset s =ᶠ[MeasureTheory.Measure.ae μ] s

In a space with an inner regular measure for finite measure sets, any measurable set of finite measure coincides almost everywhere with its everywhere positive subset.

theorem MeasureTheory.Measure.isEverywherePos_everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [OpensMeasurableSpace α] [MeasureTheory.Measure.InnerRegular μ] (hs : MeasurableSet s) : μ.IsEverywherePos (μ.everywherePosSubset s)

In a space with an inner regular measure, the everywhere positive subset of a measurable set is itself everywhere positive. This is not obvious as μ.everywherePosSubset s is defined as the points whose neighborhoods intersect s along positive measure subsets, but this does not say they also intersect μ.everywherePosSubset s along positive measure subsets.

theorem MeasureTheory.Measure.isEverywherePos_everywherePosSubset_of_measure_ne_top {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [OpensMeasurableSpace α] [MeasureTheory.Measure.InnerRegularCompactLTTop μ] (hs : MeasurableSet s) (h's : ↑↑μ s ≠ ⊤) : μ.IsEverywherePos (μ.everywherePosSubset s)

In a space with an inner regular measure for finite measure sets, the everywhere positive subset of a measurable set of finite measure is itself everywhere positive. This is not obvious as μ.everywherePosSubset s is defined as the points whose neighborhoods intersect s along positive measure subsets, but this does not say they also intersect μ.everywherePosSubset s along positive measure subsets.

theorem MeasureTheory.Measure.IsEverywherePos.smul_measure {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ.IsEverywherePos s) {c : ENNReal} (hc : c ≠ 0) : (c • μ).IsEverywherePos s

theorem MeasureTheory.Measure.IsEverywherePos.smul_measure_nnreal {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} (hs : μ.IsEverywherePos s) {c : NNReal} (hc : c ≠ 0) : (c • μ).IsEverywherePos s

theorem MeasureTheory.Measure.IsEverywherePos.of_forall_exists_nhds_eq {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (hs : μ.IsEverywherePos s) (h : ∀ x ∈ s, ∃ t ∈ nhds x, ∀ u ⊆ t, ↑↑ν u = ↑↑μ u) : ν.IsEverywherePos s

If two measures coincide locally, then a set which is everywhere positive for the former is also everywhere positive for the latter.

theorem MeasureTheory.Measure.isEverywherePos_iff_of_forall_exists_nhds_eq {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} {s : Set α} (h : ∀ x ∈ s, ∃ t ∈ nhds x, ∀ u ⊆ t, ↑↑ν u = ↑↑μ u) : ν.IsEverywherePos s ↔ μ.IsEverywherePos s

If two measures coincide locally, then a set is everywhere positive for the former iff it is everywhere positive for the latter.

theorem IsOpen.isEverywherePos {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.Measure.IsOpenPosMeasure μ] (hs : IsOpen s) : μ.IsEverywherePos s

An open set is everywhere positive for a measure which is positive on open sets.

theorem MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isAddLeftInvariant {G : Type u_2} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.Measure.InnerRegularCompactLTTop μ] {k : Set G} (h : μ.IsEverywherePos k) (hk : IsCompact k) (h'k : IsClosed k) : IsGδ k

theorem MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isMulLeftInvariant {G : Type u_2} [Group G] [TopologicalSpace G] [TopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.Measure.InnerRegularCompactLTTop μ] {k : Set G} (h : μ.IsEverywherePos k) (hk : IsCompact k) (h'k : IsClosed k) : IsGδ k

If a compact closed set is everywhere positive with respect to a left-invariant measure on a topological group, then it is a Gδ set. This is nontrivial, as there is no second-countability or metrizability assumption in the statement, so a general compact closed set has no reason to be a countable intersection of open sets.

theorem MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup {G : Type u_2} [AddGroup G] [TopologicalSpace G] [TopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsAddLeftInvariant μ] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.Measure.InnerRegularCompactLTTop μ] : MeasureTheory.Measure.InnerRegularWRT μ (fun (s : Set G) => ∃ (f : G → ℝ), Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun (s : Set G) => MeasurableSet s ∧ ↑↑μ s ≠ ⊤

abbrev MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_addGroup.match_1 {G : Type u_1} [TopologicalSpace G] ⦃K : Set G⦄ (motive : IsCompact K ∧ IsClosed K → Prop) : ∀ (h : IsCompact K ∧ IsClosed K), (∀ (K_comp : IsCompact K) (K_closed : IsClosed K), motive (_ : IsCompact K ∧ IsClosed K)) → motive h

Equations

• (_ : motive h) = (_ : motive h)

theorem MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group {G : Type u_2} [Group G] [TopologicalSpace G] [TopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.Measure.IsMulLeftInvariant μ] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [MeasureTheory.Measure.InnerRegularCompactLTTop μ] : MeasureTheory.Measure.InnerRegularWRT μ (fun (s : Set G) => ∃ (f : G → ℝ), Continuous f ∧ HasCompactSupport f ∧ s = f ⁻¹' {1}) fun (s : Set G) => MeasurableSet s ∧ ↑↑μ s ≠ ⊤

Halmos' theorem: Haar measure is completion regular. More precisely, any finite measure set can be approximated from inside by a level set of a continuous function with compact support.