Documentation

Mathlib.MeasureTheory.Measure.EverywherePos

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 #

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

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 = xs, nnhdsWithin x s, 0 < μ n
Instances For
    • 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
    Instances For
      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 α] [μ.InnerRegular] (hs : MeasurableSet s) :
      μ.everywherePosSubset s =ᵐ[μ] 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 α] [μ.InnerRegularCompactLTTop] (hs : MeasurableSet s) (h's : μ s ) :
      μ.everywherePosSubset s =ᵐ[μ] 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 α] [μ.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 α] [μ.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 : xs, tnhds x, ut, ν 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 : xs, tnhds x, ut, ν 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 α} [μ.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} [μ.IsAddLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (h : μ.IsEverywherePos k) (hk : IsCompact k) (h'k : IsClosed 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} [μ.IsMulLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] {k : Set G} (h : μ.IsEverywherePos k) (hk : IsCompact k) (h'k : IsClosed 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} [μ.IsAddLeftInvariant] [MeasureTheory.IsFiniteMeasureOnCompacts μ] [μ.InnerRegularCompactLTTop] :
      μ.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 KProp) :
      ∀ (h : IsCompact K IsClosed K), (∀ (K_comp : IsCompact K) (K_closed : IsClosed K), motive )motive h
      Equations
      • =
      Instances For
        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} [μ.IsMulLeftInvariant] [MeasureTheory.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.