# 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.

source
def MeasureTheory.Measure.IsEverywherePos {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : 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

Instances For

source
def MeasureTheory.Measure.everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : 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}

Instances For

source
theorem MeasureTheory.Measure.everywherePosSubset_subset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : Measure α) (s : Set α) :
μ.everywherePosSubset s ⊆ s
source
theorem MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_diff {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] (μ : 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.

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

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

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

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

source
theorem MeasureTheory.Measure.everywherePosSubset_ae_eq_of_measure_ne_top {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s : Set α} [OpensMeasurableSpace α] [μ.InnerRegularCompactLTTop] (hs : MeasurableSet s) (h's : μ s ≠ ⊤) :
μ.everywherePosSubset s =ᶠ[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.

source
theorem MeasureTheory.Measure.isEverywherePos_everywherePosSubset {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s : Set α} [OpensMeasurableSpace α] [μ.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.

source
theorem MeasureTheory.Measure.isEverywherePos_everywherePosSubset_of_measure_ne_top {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s : Set α} [OpensMeasurableSpace α] [μ.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.

source
theorem MeasureTheory.Measure.IsEverywherePos.smul_measure {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : μ.IsEverywherePos s) {c : ENNReal} (hc : c ≠ 0) :
(c • μ).IsEverywherePos s
source
theorem MeasureTheory.Measure.IsEverywherePos.smul_measure_nnreal {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ : Measure α} {s : Set α} (hs : μ.IsEverywherePos s) {c : NNReal} (hc : c ≠ 0) :
(c • μ).IsEverywherePos s
source
theorem MeasureTheory.Measure.IsEverywherePos.of_forall_exists_nhds_eq {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ ν : 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.

source
theorem MeasureTheory.Measure.isEverywherePos_iff_of_forall_exists_nhds_eq {α : Type u_1} [TopologicalSpace α] [MeasurableSpace α] {μ ν : 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.

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

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

source
theorem MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isMulLeftInvariant {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : Measure G} [μ.IsMulLeftInvariant] [IsFiniteMeasureOnCompacts μ] [μ.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.

source
theorem MeasureTheory.Measure.IsEverywherePos.IsGdelta_of_isAddLeftInvariant {G : Type u_2} [AddGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : Measure G} [μ.IsAddLeftInvariant] [IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (h : μ.IsEverywherePos k) (hk : IsCompact k) (h'k : IsClosed k) :
IsGδ k
source
theorem MeasureTheory.Measure.innerRegularWRT_preimage_one_hasCompactSupport_measure_ne_top_of_group {G : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [LocallyCompactSpace G] [MeasurableSpace G] [BorelSpace G] {μ : Measure G} [μ.IsMulLeftInvariant] [IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] :
μ.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.

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