MeasureTheory.Content.borel_le_caratheodory
theorem MeasureTheory.Content.borel_le_caratheodory :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G]
[S : MeasurableSpace G] [inst_2 : BorelSpace G], S ≤ μ.outerMeasure.caratheodory
This theorem asserts that for any topological space `G` equipped with a `R1Space` structure and a Borel measurable space structure, the Borel sigma-algebra is contained in the Carathéodory sigma-algebra generated by the outer measure arising from a content `μ` on `G`. In other words, every Borel set in the space is measurable with respect to the given outer measure.
More concisely: The Borel sigma-algebra of a topological space equipped with an `R1Space` structure and a Borel measurable space structure is contained in the Carathéodory sigma-algebra generated by an outer measure on the space.
|
MeasureTheory.Content.outerMeasure_lt_top_of_isCompact
theorem MeasureTheory.Content.outerMeasure_lt_top_of_isCompact :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G]
[inst_2 : WeaklyLocallyCompactSpace G] {K : Set G}, IsCompact K → ↑μ.outerMeasure K < ⊤
This theorem states that for any topological space `G`, given a measure content `μ` and a particular set `K` in `G`, if `K` is compact, then the outer measure of `K` under `μ`, when considered as a real number, is strictly less than infinity. Here, the space `G` is assumed to be an `R1Space` (a real number system) and a `WeaklyLocallyCompactSpace` (a space where every point has a compact neighborhood). This theorem is essentially enforcing that compact sets in such a space have finite outer measure.
More concisely: In an `R1Space` and `WeaklyLocallyCompactSpace` `G`, the outer measure of a compact set `K` is finite.
|
MeasureTheory.Content.outerMeasure_eq_iInf
theorem MeasureTheory.Content.outerMeasure_eq_iInf :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G] (A : Set G),
↑μ.outerMeasure A = ⨅ U, ⨅ (hU : IsOpen U), ⨅ (_ : A ⊆ U), μ.innerContent { carrier := U, is_open' := hU }
The theorem `MeasureTheory.Content.outerMeasure_eq_iInf` states that for all types `G` equipped with a `TopologicalSpace` instance, for a given measure content `μ` and for a `Set` `A` of type `G`, the outer measure of `A` under the measure content `μ` is equal to the infimum of the inner content of all open sets `U` that contain `A`. The inner content of a set in this context is the supremum of the content of all its compact subsets. In other words, the outer measure of a set can be calculated as the infimum of the inner content of all open supersets of the set.
More concisely: The outer measure of a set in a topological space, with respect to a measure content, is equal to the infimum of the inner contents of all open sets containing the set.
|
MeasureTheory.Content.innerContent_iSup_nat
theorem MeasureTheory.Content.innerContent_iSup_nat :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G]
(U : ℕ → TopologicalSpace.Opens G), μ.innerContent (⨆ i, U i) ≤ ∑' (i : ℕ), μ.innerContent (U i)
This theorem states that for any type `G` that has a `TopologicalSpace` structure and a `R1Space` structure, the inner content of a supremum of open sets with respect to a given measure `μ` is always less than or equal to the sum of the inner contents of the individual open sets. Specifically, for a sequence of open sets `U` indexed by natural numbers, the inner content of the supremum of these sets is less than or equal to the series summation of the inner contents of the sets in the sequence.
More concisely: For any measure `μ` on a type `G` with `TopologicalSpace` and `R1Space` structures, the inner content of the supremum of a sequence of open sets with respect to `μ` is less than or equal to the sum of the inner contents of the individual sets.
|
MeasureTheory.Content.innerContent_mono
theorem MeasureTheory.Content.innerContent_mono :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) ⦃U V : Set G⦄ (hU : IsOpen U)
(hV : IsOpen V),
U ⊆ V → μ.innerContent { carrier := U, is_open' := hU } ≤ μ.innerContent { carrier := V, is_open' := hV }
The theorem `MeasureTheory.Content.innerContent_mono` states that for any two open sets `U` and `V` in a topological space `G`, if `U` is a subset of `V`, then the inner content of `U` with respect to a content `μ` (a measure on the compact subsets of `G`) is less than or equal to the inner content of `V` with respect to the same content `μ`. The inner content is defined as the supremum of the content of all compact subsets of the open set. This theorem is referred to as "unbundled" to fit the API of `inducedOuterMeasure`.
More concisely: For any open sets U and V in a topological space G and content μ, if U ⊆ V, then μ^(inner) (U) ≤ μ^(inner) (V).
|
MeasureTheory.Content.outerMeasure_opens
theorem MeasureTheory.Content.outerMeasure_opens :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G]
(U : TopologicalSpace.Opens G), ↑μ.outerMeasure ↑U = μ.innerContent U
This theorem states that for any topological space `G`, given a measure content `μ` and an open set `U` in `G`, the outer measure of `U` under `μ` is equal to the inner content of `μ` on `U`. In other words, it is a property of measure theory content saying that the outer measure, which is defined by extending a content on compact sets to all sets, when applied on an open set, equals to the inner content, which is defined as the supremum of the content of all compact subsets of the open set. This holds true under the condition that the topological space `G` is also an `R1Space`, a specific kind of topological space.
More concisely: For any `R1Space` `G` with measure content `μ`, the outer measure of an open set `U` equals the inner content of `μ` on `U`.
|
MeasureTheory.Content.mono
theorem MeasureTheory.Content.mono :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) (K₁ K₂ : TopologicalSpace.Compacts G),
↑K₁ ⊆ ↑K₂ → (fun s => ↑(μ.toFun s)) K₁ ≤ (fun s => ↑(μ.toFun s)) K₂
This theorem, `MeasureTheory.Content.mono`, states that for any type `G` that is a topological space and any measure `μ` defined on `G`, if we have two compact sets `K₁` and `K₂` such that `K₁` is a subset of `K₂`, then the measure of `K₁` is less than or equal to the measure of `K₂`. In other words, it's a monotonicity property of measure: larger (or equal) sets have larger (or equal) measure.
More concisely: For any topological space `G` and measure `μ` on `G`, if `K₁` is a compact subset of `K₂`, then `μ(K₁) ≤ μ(K₂)`.
|
MeasureTheory.Content.le_outerMeasure_compacts
theorem MeasureTheory.Content.le_outerMeasure_compacts :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G]
(K : TopologicalSpace.Compacts G), (fun s => ↑(μ.toFun s)) K ≤ ↑μ.outerMeasure ↑K
This theorem states that for any topological space `G`, given a measure content `μ` and a compact set `K` within that space, the measure of `K` under `μ` is less than or equal to the outer measure of `K` with respect to the measure extended from `μ`. This holds under the additional assumption that `G` is a one-dimensional real vector space (`R1Space G`). This extends the measure content, which is defined only on compact sets, to an outer measure, which is defined on all subsets of the topological space.
More concisely: For any one-dimensional real topological space `G` with measure content `μ` and compact set `K`, the content `μ(K)` is less than or equal to the outer measure `μ*` of `K` in `G`. (i.e., `μ(K) ≤ μ*(K)`)
|
MeasureTheory.Content.measure_eq_content_of_regular
theorem MeasureTheory.Content.measure_eq_content_of_regular :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : MeasurableSpace G]
[inst_2 : R1Space G] [inst_3 : BorelSpace G],
μ.ContentRegular → ∀ (K : TopologicalSpace.Compacts G), ↑↑μ.measure ↑K = (fun s => ↑(μ.toFun s)) K
This theorem states that if `μ` is a regular content in a given topological space `G`, which also has the structures of a measurable space, an `R1Space`, and a `BorelSpace`, then the measure induced by `μ` will agree with `μ` on compact sets. In other words, for all compact sets `K` in the topological space `G`, the measure of `K` under `μ` is equal to the value of `μ` applied to `K`.
More concisely: If `μ` is a regular content on the measurable, `R1Space`, and `BorelSpace` `G`, then for all compact sets `K` in `G`, `μ(K) = μ(K: set G)`.
|
MeasureTheory.Content.measure_apply
theorem MeasureTheory.Content.measure_apply :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : R1Space G]
[S : MeasurableSpace G] [inst_2 : BorelSpace G] {s : Set G},
MeasurableSet s → ↑↑μ.measure s = ↑μ.outerMeasure s
This theorem states that for any topological space `G`, given a measure content `μ` and a set `s` in `G` that is measurable, the measure of `s` induced by the outer measure derived from `μ`, is equal to the outer measure of `s` obtained directly from `μ`. This holds true regardless of the specific type of the topological space, provided the space is both a measurable space and a Borel space.
More concisely: For any measurable and Borel topological space `(G, τ)` and measurable set `s ∈ G` with respect to the σ-algebra generated by the open sets, the measure `μ(s)` equals the outer measure `μ∗(s)`.
|
MeasureTheory.Content.innerContent_iUnion_nat
theorem MeasureTheory.Content.innerContent_iUnion_nat :
∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [inst_1 : 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 theorem `MeasureTheory.Content.innerContent_iUnion_nat` asserts that for any topological space `G` and a given measure `μ`, the inner content (defined as the supremum of the content of all compact subsets) of a countable union of sets is less than or equal to the sum of the inner contents of the individual sets. This property holds true for all countable collections of open sets in `G`. This theorem is a key mathematical property ensuring the measure behaves consistently with respect to set union operations. The specific form of the theorem here is required for the implementation of the 'inducedOuterMeasure'.
More concisely: For any measure μ on a topological space G and countable collection {A_i} of open sets, the inner content of their union is less than or equal to the sum of the inner contents of each set: ∬(i in nat) μ(A_i) ≤ μ(⋃(i in nat) A_i).
|