Documentation

Mathlib.MeasureTheory.Measure.Content

Contents #

In this file we work with contents. A content λ is a function from a certain class of subsets (such as the compact subsets) to ℝ≥0 that is

We show that:

We define bundled contents as Content. In this file we only work on contents on compact sets, and inner contents on open sets, and both contents and inner contents map into the extended nonnegative reals. However, in other applications other choices can be made, and it is not a priori clear what the best interface should be.

Main definitions #

For μ : Content G, we define

These definitions are given for spaces which are R₁. The resulting measure μ.measure is always outer regular by design. When the space is locally compact, μ.measure is also regular.

References #

A content is an additive function on compact sets taking values in ℝ≥0. It is a device from which one can define a measure.

Instances For
    theorem MeasureTheory.Content.mono' {G : Type w} [TopologicalSpace G] (self : MeasureTheory.Content G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) :
    K₁ K₂self.toFun K₁ self.toFun K₂
    theorem MeasureTheory.Content.sup_disjoint' {G : Type w} [TopologicalSpace G] (self : MeasureTheory.Content G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) :
    Disjoint K₁ K₂IsClosed K₁IsClosed K₂self.toFun (K₁ K₂) = self.toFun K₁ + self.toFun K₂
    theorem MeasureTheory.Content.sup_le' {G : Type w} [TopologicalSpace G] (self : MeasureTheory.Content G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) :
    self.toFun (K₁ K₂) self.toFun K₁ + self.toFun K₂
    Equations
    • MeasureTheory.instInhabitedContent = { default := { toFun := fun (x : TopologicalSpace.Compacts G) => 0, mono' := , sup_disjoint' := , sup_le' := } }

    Although the toFun field of a content takes values in ℝ≥0, we register a coercion to functions taking values in ℝ≥0∞ as most constructions below rely on taking iSups and iInfs, which is more convenient in a complete lattice, and aim at constructing a measure.

    Equations
    theorem MeasureTheory.Content.apply_eq_coe_toFun {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (K : TopologicalSpace.Compacts G) :
    (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K = (μ.toFun K)
    theorem MeasureTheory.Content.mono {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) (h : K₁ K₂) :
    (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K₁ (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K₂
    theorem MeasureTheory.Content.sup_disjoint {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) (h : Disjoint K₁ K₂) (h₁ : IsClosed K₁) (h₂ : IsClosed K₂) :
    (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (K₁ K₂) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K₁ + (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K₂
    theorem MeasureTheory.Content.sup_le {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (K₁ : TopologicalSpace.Compacts G) (K₂ : TopologicalSpace.Compacts G) :
    (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (K₁ K₂) (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K₁ + (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K₂
    theorem MeasureTheory.Content.empty {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) :
    (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) = 0

    Constructing the inner content of a content. From a content defined on the compact sets, we obtain a function defined on all open sets, by taking the supremum of the content of all compact subsets.

    Equations
    Instances For
      theorem MeasureTheory.Content.le_innerContent {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (K : TopologicalSpace.Compacts G) (U : TopologicalSpace.Opens G) (h2 : K U) :
      (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K μ.innerContent U
      theorem MeasureTheory.Content.innerContent_le {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (U : TopologicalSpace.Opens G) (K : TopologicalSpace.Compacts G) (h2 : U K) :
      μ.innerContent U (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K
      theorem MeasureTheory.Content.innerContent_of_isCompact {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) {K : Set G} (h1K : IsCompact K) (h2K : IsOpen K) :
      μ.innerContent { carrier := K, is_open' := h2K } = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) { carrier := K, isCompact' := h1K }
      theorem MeasureTheory.Content.innerContent_mono {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) ⦃U : Set G ⦃V : Set G (hU : IsOpen U) (hV : IsOpen V) (h2 : U V) :
      μ.innerContent { carrier := U, is_open' := hU } μ.innerContent { carrier := V, is_open' := hV }

      This is "unbundled", because that is required for the API of inducedOuterMeasure.

      theorem MeasureTheory.Content.innerContent_exists_compact {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) {U : TopologicalSpace.Opens G} (hU : μ.innerContent U ) {ε : NNReal} (hε : ε 0) :
      ∃ (K : TopologicalSpace.Compacts G), K U μ.innerContent U (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K + ε
      theorem MeasureTheory.Content.innerContent_iSup_nat {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : TopologicalSpace.Opens G) :
      μ.innerContent (⨆ (i : ), U i) ∑' (i : ), μ.innerContent (U i)

      The inner content of a supremum of opens is at most the sum of the individual inner contents.

      theorem MeasureTheory.Content.innerContent_iUnion_nat {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] ⦃U : Set G (hU : ∀ (i : ), IsOpen (U i)) :
      μ.innerContent { carrier := ⋃ (i : ), U i, is_open' := } ∑' (i : ), μ.innerContent { carrier := U i, is_open' := }

      The inner content of a union of sets is at most the sum of the individual inner contents. This is the "unbundled" version of innerContent_iSup_nat. It is required for the API of inducedOuterMeasure.

      theorem MeasureTheory.Content.innerContent_comap {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (f : G ≃ₜ G) (h : ∀ ⦃K : TopologicalSpace.Compacts G⦄, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map f K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (U : TopologicalSpace.Opens G) :
      μ.innerContent ((TopologicalSpace.Opens.comap f.toContinuousMap) U) = μ.innerContent U
      theorem MeasureTheory.Content.is_add_left_invariant_innerContent {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [AddGroup G] [TopologicalAddGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g + b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (g : G) (U : TopologicalSpace.Opens G) :
      μ.innerContent ((TopologicalSpace.Opens.comap (Homeomorph.addLeft g).toContinuousMap) U) = μ.innerContent U
      theorem MeasureTheory.Content.is_mul_left_invariant_innerContent {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [Group G] [TopologicalGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g * b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (g : G) (U : TopologicalSpace.Opens G) :
      μ.innerContent ((TopologicalSpace.Opens.comap (Homeomorph.mulLeft g).toContinuousMap) U) = μ.innerContent U
      theorem MeasureTheory.Content.innerContent_pos_of_is_add_left_invariant {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [AddGroup G] [TopologicalAddGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g + b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (K : TopologicalSpace.Compacts G) (hK : (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K 0) (U : TopologicalSpace.Opens G) (hU : (↑U).Nonempty) :
      0 < μ.innerContent U
      theorem MeasureTheory.Content.innerContent_pos_of_is_mul_left_invariant {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [Group G] [TopologicalGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g * b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (K : TopologicalSpace.Compacts G) (hK : (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K 0) (U : TopologicalSpace.Opens G) (hU : (↑U).Nonempty) :
      0 < μ.innerContent U
      theorem MeasureTheory.Content.innerContent_mono' {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) ⦃U : Set G ⦃V : Set G (hU : IsOpen U) (hV : IsOpen V) (h2 : U V) :
      μ.innerContent { carrier := U, is_open' := hU } μ.innerContent { carrier := V, is_open' := hV }

      Extending a content on compact sets to an outer measure on all sets.

      Equations
      Instances For
        theorem MeasureTheory.Content.outerMeasure_opens {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : TopologicalSpace.Opens G) :
        μ.outerMeasure U = μ.innerContent U
        theorem MeasureTheory.Content.outerMeasure_of_isOpen {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : Set G) (hU : IsOpen U) :
        μ.outerMeasure U = μ.innerContent { carrier := U, is_open' := hU }
        theorem MeasureTheory.Content.outerMeasure_le {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : TopologicalSpace.Opens G) (K : TopologicalSpace.Compacts G) (hUK : U K) :
        μ.outerMeasure U (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K
        theorem MeasureTheory.Content.le_outerMeasure_compacts {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (K : TopologicalSpace.Compacts G) :
        (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K μ.outerMeasure K
        theorem MeasureTheory.Content.outerMeasure_eq_iInf {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (A : Set G) :
        μ.outerMeasure A = ⨅ (U : Set G), ⨅ (hU : IsOpen U), ⨅ (_ : A U), μ.innerContent { carrier := U, is_open' := hU }
        theorem MeasureTheory.Content.outerMeasure_exists_compact {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] {U : TopologicalSpace.Opens G} (hU : μ.outerMeasure U ) {ε : NNReal} (hε : ε 0) :
        ∃ (K : TopologicalSpace.Compacts G), K U μ.outerMeasure U μ.outerMeasure K + ε
        theorem MeasureTheory.Content.outerMeasure_exists_open {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] {A : Set G} (hA : μ.outerMeasure A ) {ε : NNReal} (hε : ε 0) :
        ∃ (U : TopologicalSpace.Opens G), A U μ.outerMeasure U μ.outerMeasure A + ε
        theorem MeasureTheory.Content.outerMeasure_preimage {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (f : G ≃ₜ G) (h : ∀ ⦃K : TopologicalSpace.Compacts G⦄, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map f K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (A : Set G) :
        μ.outerMeasure (f ⁻¹' A) = μ.outerMeasure A
        theorem MeasureTheory.Content.is_add_left_invariant_outerMeasure {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [AddGroup G] [TopologicalAddGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g + b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (g : G) (A : Set G) :
        μ.outerMeasure ((fun (x : G) => g + x) ⁻¹' A) = μ.outerMeasure A
        theorem MeasureTheory.Content.is_mul_left_invariant_outerMeasure {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [Group G] [TopologicalGroup G] (h : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g * b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (g : G) (A : Set G) :
        μ.outerMeasure ((fun (x : G) => g * x) ⁻¹' A) = μ.outerMeasure A
        theorem MeasureTheory.Content.outerMeasure_caratheodory {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (A : Set G) :
        MeasurableSet A ∀ (U : TopologicalSpace.Opens G), μ.outerMeasure (U A) + μ.outerMeasure (U \ A) μ.outerMeasure U
        theorem MeasureTheory.Content.outerMeasure_pos_of_is_add_left_invariant {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [AddGroup G] [TopologicalAddGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g + b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (K : TopologicalSpace.Compacts G) (hK : (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) :
        0 < μ.outerMeasure U
        theorem MeasureTheory.Content.outerMeasure_pos_of_is_mul_left_invariant {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [Group G] [TopologicalGroup G] (h3 : ∀ (g : G) {K : TopologicalSpace.Compacts G}, (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) (TopologicalSpace.Compacts.map (fun (b : G) => g * b) K) = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K) (K : TopologicalSpace.Compacts G) (hK : (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K 0) {U : Set G} (h1U : IsOpen U) (h2U : U.Nonempty) :
        0 < μ.outerMeasure U
        theorem MeasureTheory.Content.borel_le_caratheodory {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] :
        S μ.outerMeasure.caratheodory

        For the outer measure coming from a content, all Borel sets are measurable.

        The measure induced by the outer measure coming from a content, on the Borel sigma-algebra.

        Equations
        • μ.measure = μ.outerMeasure.toMeasure
        Instances For
          theorem MeasureTheory.Content.measure_apply {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] {s : Set G} (hs : MeasurableSet s) :
          μ.measure s = μ.outerMeasure s
          instance MeasureTheory.Content.outerRegular {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] [S : MeasurableSpace G] [BorelSpace G] :
          μ.measure.OuterRegular
          Equations
          • =

          In a locally compact space, any measure constructed from a content is regular.

          Equations
          • =

          A content μ is called regular if for every compact set K, μ(K) = inf {μ(K') : K ⊂ int K' ⊂ K'}. See Paul Halmos (1950), Measure Theory, §54

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem MeasureTheory.Content.contentRegular_exists_compact {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) (H : μ.ContentRegular) (K : TopologicalSpace.Compacts G) {ε : NNReal} (hε : ε 0) :
            ∃ (K' : TopologicalSpace.Compacts G), K.carrier interior K'.carrier (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K' (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K + ε
            theorem MeasureTheory.Content.measure_eq_content_of_regular {G : Type w} [TopologicalSpace G] (μ : MeasureTheory.Content G) [MeasurableSpace G] [R1Space G] [BorelSpace G] (H : μ.ContentRegular) (K : TopologicalSpace.Compacts G) :
            μ.measure K = (fun (s : TopologicalSpace.Compacts G) => (μ.toFun s)) K

            If μ is a regular content, then the measure induced by μ will agree with μ on compact sets.