MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite
theorem MeasureTheory.Measure.InnerRegularWRT.weaklyRegular_of_finite :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : BorelSpace α]
(μ : MeasureTheory.Measure α) [inst_3 : MeasureTheory.IsFiniteMeasure μ],
μ.InnerRegularWRT IsClosed IsOpen → μ.WeaklyRegular
In a finite measure space, under the assumptions that the space is both a Measurable and a Topological space, as well as a Borel space, this theorem states that if it's possible to approximate any open set from inside using closed sets, then the given measure is weakly regular. This is expressed formally as: for all sets of a certain type `α`, if the measure `μ` is such that it is inner regular with respect to closed and open sets, then `μ` is weakly regular.
More concisely: In a finite measure space that is both measurable and topological, and a Borel space, if the measure is inner regular with respect to closed and open sets, then it is weakly regular.
|
MeasureTheory.Measure.InnerRegularWRT.restrict_of_measure_ne_top
theorem MeasureTheory.Measure.InnerRegularWRT.restrict_of_measure_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop},
(μ.InnerRegularWRT p fun s => MeasurableSet s ∧ ↑↑μ s ≠ ⊤) →
∀ {A : Set α}, ↑↑μ A ≠ ⊤ → (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s
The theorem `MeasureTheory.Measure.InnerRegularWRT.restrict_of_measure_ne_top` states that if a measure `μ` is inner regular with respect to a certain class of sets and for measurable finite measure sets, then the restriction of this measure to any finite measure set also exhibits inner regularity with respect to the same class of sets and for measurable sets. Here, inner regularity refers to the property of a measure where its value on a set can be approximated from within using subsets from a certain class. In this case, the class of sets is defined by the predicate `p`, and the measure sets considered are those that are measurable and have a measure that is not infinity (`⊤`).
More concisely: If a measure μ is inner regular with respect to a class of sets p for measurable, finite measure sets, then the restriction of μ to any such set exhibits inner regularity with respect to the same class of sets p for measurable sets.
|
MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup
theorem MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop} {U : Set α},
μ.InnerRegularWRT p q → q U → ↑↑μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), ↑↑μ K
This theorem states that for any measure `μ` that is inner regular with respect to predicates `p` and `q`, and for any set `U` that satisfies predicate `q`, the measure `μ` of `U` is equal to the supremum of the measures of subsets `K` of `U` that satisfy the predicate `p`. In other words, in this context, the measure of a set is determined by the measures of its 'interesting' subsets as defined by the predicate `p`.
More concisely: For any inner regular measure `μ` and predicates `p` and `q`, if `U` is a `q`-set, then `μ(U) = ��╗{μ(K) : K ⊆ U, p(K)}` (the supremum of measures of `p`-subsets of `U`).
|
MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular
theorem MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α},
μ.FiniteSpanningSetsIn {U | IsOpen U ∧ (μ.restrict U).OuterRegular} → μ.OuterRegular
The theorem `MeasureTheory.Measure.FiniteSpanningSetsIn.outerRegular` states: If we have a measure, denoted as `μ`, on a measurable and topological space `α` which also supports the Borel σ-algebra (`OpensMeasurableSpace α`), and if this measure `μ` has the property that it admits a finite collection of open sets that span the entire space (`μ.FiniteSpanningSetsIn`), such that the restriction of `μ` to each of these open sets is outer regular (`(μ.restrict U).OuterRegular`), then the original measure `μ` itself is outer regular (`μ.OuterRegular`). Outer regularity, in this context, refers to the property that the measure of a set can be approximated from "outside" by open sets.
More concisely: If a measure on a measurable and topological space with the Borel σ-algebra has a finite collection of open sets that spanning the space and such that the restriction of the measure to each open set is outer regular, then the measure is outer regular.
|
MeasureTheory.Measure.OuterRegular.of_restrict
theorem MeasureTheory.Measure.OuterRegular.of_restrict :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [inst_2 : OpensMeasurableSpace α]
{μ : MeasureTheory.Measure α} {s : ℕ → Set α},
(∀ (n : ℕ), (μ.restrict (s n)).OuterRegular) → (∀ (n : ℕ), IsOpen (s n)) → Set.univ ⊆ ⋃ n, s n → μ.OuterRegular
This theorem states that for any type `α` equipped with a measurable space structure, a topological space structure, and an open sets measurable space structure, given a measure `μ` on this type and a sequence of sets `s` indexed by natural numbers, if each measure `μ` restricted to the set `s n` is outer regular for all `n`, and each `s n` is an open set, and the union of all these sets `s n` covers the universal set (i.e., every element of the type `α` belongs to at least one `s n`), then the measure `μ` itself is outer regular.
In mathematical terms, if we have a measure space that is also a topological space, and every measure restricted to a countable collection of open sets is outer regular, and the union of these sets covers the entire space, then the original measure is outer regular. Outer regularity is a property of a measure meaning that for any measurable set, the measure of the set can be approximated from above by the measures of open supersets.
More concisely: If a measure on a type equipped with measurable space, topological space, and open sets measurable space structures, restricted to a countable collection of open sets and covering the universal set, is outer regular for each set, then the measure itself is outer regular.
|
MeasureTheory.Measure.Regular.smul
theorem MeasureTheory.Measure.Regular.smul :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.Regular] {x : ENNReal}, x ≠ ⊤ → (x • μ).Regular
The theorem `MeasureTheory.Measure.Regular.smul` states that for any type `α` which is both a `MeasurableSpace` and a `TopologicalSpace`, given a regular measure `μ` on `α` and a scalar `x` in the extended nonnegative real numbers (`ENNReal`) that is not infinite (`⊤`), the scaled measure (`x • μ`) is also regular. In Measure Theory, regular measures have certain properties like being finite on compact sets and outer regularity, which means every measurable set is approximately measurable by open sets from outside. This theorem ensures that these properties are maintained when the measure is scaled by a non-infinite scalar.
More concisely: Given a regular measure μ on a measurable space and topological space α, and a non-infinite scalar x in the extended nonnegative real numbers, the scaled measure x • μ is also regular.
|
MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen
theorem MeasureTheory.Measure.InnerRegularWRT.measurableSet_of_isOpen :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
{p : Set α → Prop} [inst_2 : μ.OuterRegular],
μ.InnerRegularWRT p IsOpen →
(∀ ⦃s U : Set α⦄, p s → IsOpen U → p (s \ U)) → μ.InnerRegularWRT p fun s => MeasurableSet s ∧ ↑↑μ s ≠ ⊤
This theorem states that in a measure space, given a measure `μ` that is inner regular with respect to a property `p` and for open sets, if for any set `s` satisfying property `p` and any open set `U`, the difference `s \ U` also satisfies property `p`, then the measure `μ` is inner regular with respect to the property `p` and sets that are both measurable and have finite measure. In other words, if a measure is inner regular on open sets, then every finite measurable set can be approximated by a subset that has property `p`.
More concisely: If a measure `μ` is inner regular with respect to open sets in a measure space and for any measurable set `s` with finite measure satisfying property `p` and any open set `U` with `s \ U` also having property `p`, then `μ` is inner regular with respect to property `p` for measurable sets of finite measure.
|
MeasureTheory.Measure.InnerRegular.map
theorem MeasureTheory.Measure.InnerRegular.map :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
{μ : MeasureTheory.Measure α} [inst_2 : BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β]
[inst_5 : BorelSpace β] [inst_6 : μ.InnerRegular] (f : α ≃ₜ β), (MeasureTheory.Measure.map (⇑f) μ).InnerRegular
This theorem states that, for any two types `α` and `β` with `α` being a measurable space and topological space, and `β` being a measurable space, topological space and Borel space, given a measure `μ` on `α` that is inner regular, and a homeomorphism `f` from `α` to `β`, the measure obtained by pushing forward `μ` with `f`, denoted as `MeasureTheory.Measure.map (⇑f) μ`, is also inner regular.
In simpler terms, it says that under certain conditions, the property of a measure being inner regular is preserved under a transformation (in this case, the homeomorphism `f`). Inner regularity of a measure is a property that links the measure theory with the topology of the space by saying that the measure of a set can be approximated from inside by compact subsets.
More concisely: Given a measurable space and topological space `α`, a Borel space `β`, an inner regular measure `μ` on `α`, and a homeomorphism `f` from `α` to `β`, the pushed-forward measure `MeasureTheory.Measure.map (⇑f) μ` is also inner regular.
|
MeasureTheory.Measure.InnerRegularWRT.of_imp
theorem MeasureTheory.Measure.InnerRegularWRT.of_imp :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop},
(∀ (s : Set α), q s → p s) → μ.InnerRegularWRT p q
The theorem `MeasureTheory.Measure.InnerRegularWRT.of_imp` states that for any type `α`, measurable space `m` of `α`, measure `μ` of `α`, and predicates `p` and `q` on the sets of `α`, if it holds that for every set `s`, `q s` implies `p s`, then the measure `μ` is inner regular with respect to `p` and `q`. In other words, for any set `U` that satisfies `q`, and any real number `r` less than the measure of `U`, there exists a subset `K` of `U` that satisfies `p` and its measure is greater than `r`.
More concisely: Given a measurable space `(α, m)`, measure `μ`, and predicates `p` and `q` on `α` such that `q ⊆ p` and `μ(U) < ∞` for all `U` with `q U`, for any `r < μ(U)`, there exists a `K ⊆ U` with `p K` and `μ(K) > r`.
|
MeasurableSet.measure_eq_iSup_isCompact_of_ne_top
theorem MeasurableSet.measure_eq_iSup_isCompact_of_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
MeasurableSet A → ↑↑μ A ≠ ⊤ → ↑↑μ A = ⨆ K, ⨆ (_ : K ⊆ A), ⨆ (_ : IsCompact K), ↑↑μ K
The theorem `MeasurableSet.measure_eq_iSup_isCompact_of_ne_top` states that, given a measure `μ` that is inner regular for finite measure sets with respect to compact sets, any measurable set `A` of finite measure (i.e., `μ A ≠ ∞`) can be approximated from inside by compact sets. In other words, the measure of the set `A` is equal to the supremum of the measures of all compact sets `K` that are subsets of `A`. This theorem allows us to approximate the measure of any finite measurable set using compact subsets, provided the measure is inner regular with respect to compact sets.
More concisely: Given a finite measure `μ` that is inner regular with respect to compact sets, the measure of any measurable set `A` equals the supremum of the measures of all compact subsets of `A`.
|
MeasureTheory.Measure.WeaklyRegular.restrict_of_measure_ne_top
theorem MeasureTheory.Measure.WeaklyRegular.restrict_of_measure_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : BorelSpace α] [inst_3 : μ.WeaklyRegular] {A : Set α}, ↑↑μ A ≠ ⊤ → (μ.restrict A).WeaklyRegular
This theorem states that for any type `α` which has a measurable space structure and a topological space structure, if `μ` is a weakly regular measure on `α`, and `A` is a set of `α` such that the measure of `A` under `μ` is not infinite, then the measure obtained by restricting `μ` to `A` is also weakly regular. The theorem assumes that `α` is also a Borel space, which is a requirement for the measure `μ` to be weakly regular.
More concisely: If `α` is a Borel space with both measurable and topological structures, `μ` is a weakly regular measure on `α` with finite measure for set `A ⊆ α`, then the restriction of `μ` to `A` is also a weakly regular measure.
|
IsOpen.exists_lt_isClosed
theorem IsOpen.exists_lt_isClosed :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.WeaklyRegular] ⦃U : Set α⦄, IsOpen U → ∀ {r : ENNReal}, r < ↑↑μ U → ∃ F ⊆ U, IsClosed F ∧ r < ↑↑μ F
This theorem states that if `μ` is a weakly regular measure on a topological measurable space `α`, then for any open set `U` in this space, it can be approximated by a closed subset. More specifically, for any extended nonnegative real number `r` that is less than the measure of `U`, there exists a closed set `F` that is a subset of `U` such that `r` is also less than the measure of `F`. This theorem is crucial in the context of measure theory where the measure of open sets can often be approximated by the measure of closed subsets.
More concisely: Given a weakly regular measure `μ` on a topological measurable space `α`, for any open set `U` and any `r` < `μ(U)`, there exists a closed subset `F` of `U` with `r` < `μ(F)`.
|
MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact
theorem MeasureTheory.Measure.OuterRegular.measure_closure_eq_of_isCompact :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : R1Space α] [inst_3 : μ.OuterRegular] {k : Set α}, IsCompact k → ↑↑μ (closure k) = ↑↑μ k
This theorem states that for every set `k` in a measurable space `α` that is both a topological space and a R1 space, if `k` is compact, then the measure of the closure of `k` (according to the outer regular measure `μ`) is equal to the measure of `k` itself. This theorem assumes the `σ`-algebra of the measure space to be arbitrary, and does not make any specific assumptions about the measure `μ`. This theorem is particularly related to the concept of outer regular measures in measure theory, and there exists a related version of this theorem (`IsCompact.measure_closure`) that specifically assumes the `σ`-algebra to be the Borel `σ`-algebra.
More concisely: If `μ` is an outer regular measure on the measurable space `(α, σ)` where `α` is a compact, topological space and an R1 space, then the measure of the closure of any set `k` in `α` equals the measure of `k` itself.
|
Mathlib.MeasureTheory.Measure.Regular._auxLemma.2
theorem Mathlib.MeasureTheory.Measure.Regular._auxLemma.2 : ∀ {b a : Prop}, (∃ (_ : a), b) = (a ∧ b)
This theorem states that for any two propositions 'a' and 'b', the existence of 'b' assuming 'a', denoted as `∃ (_ : a), b`, is equivalent to the conjunction of 'a' and 'b', denoted as `a ∧ b`. In other words, 'a' being true and 'b' existing under that assumption is the same as 'a' and 'b' both being true simultaneously.
More concisely: The theorem asserts that for any propositions 'a' and 'b' in Lean, `∃ (x : a), b` is logically equivalent to `a ∧ b`.
|
IsCompact.measure_eq_infi_isOpen
theorem IsCompact.measure_eq_infi_isOpen :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.InnerRegularCompactLTTop] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_4 : R1Space α]
[inst_5 : BorelSpace α] {K : Set α}, IsCompact K → ↑↑μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), ↑↑μ U
This theorem states that given a measurable space `α`, equipped with a topological structure, a measure `μ`, and a compact set `K`, if the measure `μ` is inner regular for finite measure sets with respect to compact sets and is locally finite in an R₁ space, then the measure of the compact set `K` is equal to the infimum of the measures of all open sets `U` that contain `K`. In other words, any compact set in such a space can be approximated from the outside by open sets.
More concisely: Given a measurable space with a topological structure, a locally finite and inner regular measure, if the measure of every compact set equals the infimum of measures of open sets containing it, then the measure of a compact set is equal to the infimum of the measures of all open sets that contain it.
|
IsOpen.measure_eq_iSup_isCompact
theorem IsOpen.measure_eq_iSup_isCompact :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] ⦃U : Set α⦄,
IsOpen U →
∀ (μ : MeasureTheory.Measure α) [inst_2 : μ.Regular], ↑↑μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), ↑↑μ K
The theorem `IsOpen.measure_eq_iSup_isCompact` states that for any open set `U` in a given measurable and topological space `α`, the measure of `U` under a regular measure `μ` is equal to the supremum of the measures of all compact subsets `K` of `U`. This means, intuitively, that the measure of an open set can be calculated as the "largest" measure of the compact sets it contains.
More concisely: For any open set U in a measurable and topological space α with a regular measure μ, the measure of U is equal to the supremum of the measures of all compact subsets K of U.
|
MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite
theorem MeasureTheory.Measure.InnerRegularWRT.of_sigmaFinite :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : MeasureTheory.SigmaFinite μ],
μ.InnerRegularWRT (fun s => MeasurableSet s ∧ ↑↑μ s ≠ ⊤) fun s => MeasurableSet s
This theorem states that for any sigma-finite measure `μ` in a measurable space `α`, any measurable set can be approximated from inside by a measurable set of finite measure. In other words, given any measurable set in the space, there exists a measurable set within it such that the measure of the internal set is finite and not infinite. This theorem is a part of the Inner Regularity property related to measure theory.
More concisely: For any sigma-finite measure `μ` on a measurable space `α`, every measurable set can be approximated from the inside by a measurable set of finite measure.
|
MeasureTheory.Measure.InnerRegularWRT.restrict
theorem MeasureTheory.Measure.InnerRegularWRT.restrict :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : Set α → Prop},
(μ.InnerRegularWRT p fun s => MeasurableSet s ∧ ↑↑μ s ≠ ⊤) →
∀ (A : Set α), (μ.restrict A).InnerRegularWRT p fun s => MeasurableSet s ∧ ↑↑(μ.restrict A) s ≠ ⊤
The theorem `MeasureTheory.Measure.InnerRegularWRT.restrict` states that if a measure `μ` is inner regular for sets that are both measurable and of finite measure, with respect to a certain class of sets `p`, then the restriction of `μ` to any set `A` also maintains this inner regularity with respect to the same class `p`. This is true for any sets of `A` that are measurable and have a finite measure under the restricted measure.
More concisely: If `μ` is an inner regular measure on the measurable sets of finite measure with respect to class `p`, then the restriction of `μ` to any measurable subset `A` of finite measure is also inner regular with respect to `p`.
|
IsOpen.exists_lt_isCompact
theorem IsOpen.exists_lt_isCompact :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.Regular] ⦃U : Set α⦄, IsOpen U → ∀ {r : ENNReal}, r < ↑↑μ U → ∃ K ⊆ U, IsCompact K ∧ r < ↑↑μ K
This theorem states that, given a regular measure `μ` in a measurable and topological space `α`, for any open set `U` in this space, and any extended nonnegative real number `r` that is less than the measure of `U`, there exists a compact subset `K` of `U` such that `r` is less than the measure of `K`. This can be interpreted as any open set in a measurable and topological space can be approximated by a compact subset when we are working with a regular measure.
More concisely: Given a regular measure `μ` in a measurable and topological space `α`, for any open set `U` and any `r` in `[0, μ(U))`, there exists a compact subset `K` of `U` with `μ(K) ≤ r`.
|
MeasureTheory.Measure.Regular.exists_compact_not_null
theorem MeasureTheory.Measure.Regular.exists_compact_not_null :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.Regular], (∃ K, IsCompact K ∧ ↑↑μ K ≠ 0) ↔ μ ≠ 0
The theorem `MeasureTheory.Measure.Regular.exists_compact_not_null` states that for any type `α` equipped with a measurable space structure and a topological space structure, and for any measure `μ` on `α` that is regular, there exists a compact set `K` such that the measure of `K` is not zero if and only if the measure `μ` is not zero. In mathematical terms, this can be written as for all regular measures `μ`, `∃ K, IsCompact K ∧ μ(K) ≠ 0` if and only if `μ ≠ 0`.
More concisely: A regular measure on a topological space is non-zero if and only if it assigns a non-zero measure to some compact set.
|
MeasurableSet.exists_lt_isClosed_of_ne_top
theorem MeasurableSet.exists_lt_isClosed_of_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.WeaklyRegular] ⦃A : Set α⦄,
MeasurableSet A → ↑↑μ A ≠ ⊤ → ∀ {r : ENNReal}, r < ↑↑μ A → ∃ K ⊆ A, IsClosed K ∧ r < ↑↑μ K
The theorem `MeasurableSet.exists_lt_isClosed_of_ne_top` states that, given a weakly regular measure `μ` over a measurable space `α` with a topological structure, for any measurable set `A` with finite measure (meaning the measure of `A` is not infinity), and for any extended nonnegative real number `r` that is strictly less than the measure of `A`, there exists a closed subset `K` of `A` such that `r` is strictly less than the measure of `K`. In other words, this theorem states that in a space with a weakly regular measure, we can always find a closed set within any measurable set of finite mass that has a measure larger than any given value less than the measure of the entire set.
More concisely: For any weakly regular measure μ on a measurable space α with topology, if A is a measurable set of finite measure and r < μ(A), then there exists a closed subset K ⊆ A with μ(K) < r.
|
Mathlib.MeasureTheory.Measure.Regular._auxLemma.3
theorem Mathlib.MeasureTheory.Measure.Regular._auxLemma.3 :
∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLinearOrder α] {a : α} {f : ι → α}, (iInf f < a) = ∃ i, f i < a
This theorem, `Mathlib.MeasureTheory.Measure.Regular._auxLemma.3`, states that for any type `α` equipped with a complete linear order, a given element `a` of type `α`, and a function `f` from some index set `ι` to `α`, the inequality `iInf f < a` holds if and only if there exists an index `i` such that `f(i) < a`. Here `iInf f` denotes the indexed infimum of the function `f`, which is the smallest element in the range of `f` in the given complete linear order.
More concisely: For a complete linear order on type `α`, an element `a` in `α`, and a function `f` from an index set `ι` to `α`, `iInf f < a` if and only if there exists an index `i` such that `f(i) < a`.
|
Set.measure_eq_iInf_isOpen
theorem Set.measure_eq_iInf_isOpen :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] (A : Set α) (μ : MeasureTheory.Measure α)
[inst_2 : μ.OuterRegular], ↑↑μ A = ⨅ U, ⨅ (_ : A ⊆ U), ⨅ (_ : IsOpen U), ↑↑μ U
The theorem `Set.measure_eq_iInf_isOpen` states that for any set `A` in a measurable space `α` which also has a topological structure, given a measure `μ` that is outer regular, the measure of the set `A` is equal to the infimum of the measures of all open sets `U` that contain `A`. In other words, for an outer regular measure `μ`, the measure of a set `A` is the smallest measure among all open sets that include `A`.
More concisely: For any outer regular measure μ on a measurable space α with a topology, the measure of a set A is equal to the infimum of the measures of all open sets containing A.
|
MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable
theorem MeasureTheory.Measure.WeaklyRegular.innerRegular_measurable :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.WeaklyRegular], μ.InnerRegularWRT IsClosed fun s => MeasurableSet s ∧ ↑↑μ s ≠ ⊤
This theorem states that for any measurable and topological space `α` and any weakly regular measure `μ` on `α`, `μ` is inner regular with respect to closed sets and sets which are measurable and not of infinite measure. In other words, for any set `U` which is measurable and not of infinite measure, and any real number `r` less than the measure of `U`, there exists a closed subset `K` of `U` such that the measure of `K` is greater than `r`. This is a property of weakly regular measures and is useful in several proofs about properties of measures.
More concisely: For any measurable and weakly regular measure `μ` on a measurable space `α`, and for any measurable set `U` of finite measure, there exists a closed subset `K` of `U` such that `μ(K) > μ(U) - r` for any real number `r` with `0 < r < μ(U)`.
|
MeasurableSet.exists_lt_isCompact
theorem MeasurableSet.exists_lt_isCompact :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.InnerRegular] ⦃A : Set α⦄,
MeasurableSet A → ∀ {r : ENNReal}, r < ↑↑μ A → ∃ K ⊆ A, IsCompact K ∧ r < ↑↑μ K
This theorem states that if a measure `μ` is inner regular, then for any measurable set `A`, we can approximate it by a compact subset. More specifically, for any extended nonnegative real number `r` that is less than the measure of `A`, there exists a compact subset `K` of `A` such that `r` is less than the measure of `K`. Inner regularity refers to the property of a measure where the measure of a set can be approximated from within by compact sets.
More concisely: If `μ` is an inner regular measure, then for any measurable set `A` and any `r` < `μ(A)`, there exists a compact subset `K` ⊆ `A` with `μ(K)` > `r`.
|
MeasureTheory.Measure.InnerRegular.map_of_continuous
theorem MeasureTheory.Measure.InnerRegular.map_of_continuous :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
{μ : MeasureTheory.Measure α} [inst_2 : BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β]
[inst_5 : BorelSpace β] [h : μ.InnerRegular] {f : α → β},
Continuous f → (MeasureTheory.Measure.map f μ).InnerRegular
The theorem `MeasureTheory.Measure.InnerRegular.map_of_continuous` states that for any types `α` and `β`, given that `α` is both a measurable space and a topological space, and `β` is a measurable space, a topological space and a Borel space, if `μ` is a measure on `α` that is inner regular and `f` is a continuous function from `α` to `β`, then the pushforward measure of `μ` by `f`, denoted as `MeasureTheory.Measure.map f μ`, is also inner regular. This means that the property of inner regularity of a measure is preserved under the action of continuous functions.
More concisely: If `μ` is an inner regular measure on the measurable and topological space `α`, and `f` is a continuous function from `α` to the measurable and Borel space `β`, then `MeasureTheory.Measure.map f μ` is also an inner regular measure on `β`.
|
MeasurableSet.measure_eq_iSup_isClosed_of_ne_top
theorem MeasurableSet.measure_eq_iSup_isClosed_of_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.WeaklyRegular] ⦃A : Set α⦄,
MeasurableSet A → ↑↑μ A ≠ ⊤ → ↑↑μ A = ⨆ K, ⨆ (_ : K ⊆ A), ⨆ (_ : IsClosed K), ↑↑μ K
The theorem states that given a measure space with a weakly regular measure, for any measurable set of finite measure, the measure of the set is equal to the supremum of the measures of all closed subsets that are contained in the set. This means that for any such measurable set, we can approximate its measure from below by using closed subsets of this set.
More concisely: For any measurable set in a weakly regular measure space with finite measure, the set's measure equals the supremum of the measures of its closed subsets.
|
MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed
theorem MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed :
∀ {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : SigmaCompactSpace X] [inst_2 : MeasurableSpace X]
(μ : MeasureTheory.Measure X), μ.InnerRegularWRT IsCompact IsClosed
The theorem `MeasureTheory.Measure.InnerRegularWRT.isCompact_isClosed` states that in a σ-compact space (a topological space that is the countable union of compact subsets), given any measure `μ` defined on the space, every closed set can be approximated by a compact subset. More specifically, inner regularity with respect to compactness and closedness holds, meaning that for any closed set, there is a compact subset that, when measured under `μ`, comes arbitrarily close to the measure of the whole closed set.
More concisely: In a σ-compact space, every closed set can be approximated arbitrarily closely in measure by a compact subset, with respect to an inner regular measure.
|
IsOpen.measure_eq_iSup_isClosed
theorem IsOpen.measure_eq_iSup_isClosed :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] ⦃U : Set α⦄,
IsOpen U →
∀ (μ : MeasureTheory.Measure α) [inst_2 : μ.WeaklyRegular],
↑↑μ U = ⨆ F, ⨆ (_ : F ⊆ U), ⨆ (_ : IsClosed F), ↑↑μ F
This theorem states that if `μ` is a weakly regular measure in a measurable space with a topological structure, then for any open set `U`, the measure `μ` of `U` is equal to the supremum of the measures of all closed subsets `F` of `U`. In simpler terms, you can approximate the measure of an open set by taking the supremum of the measures of its closed subsets, but only if the measure is weakly regular.
More concisely: If `μ` is a weakly regular measure on a measurable space with a topology, then the measure of any open set `U` equals the supremum of the measures of its closed subsets.
|
MeasureTheory.Measure.Regular.map
theorem MeasureTheory.Measure.Regular.map :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
{μ : MeasureTheory.Measure α} [inst_2 : BorelSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β]
[inst_5 : BorelSpace β] [inst_6 : μ.Regular] (f : α ≃ₜ β), (MeasureTheory.Measure.map (⇑f) μ).Regular
This theorem states that for any two types `α` and `β` with `α` having a measurable space structure, a topological space structure, a borel space structure and a regular measure `μ`, and `β` having a measurable space structure, a topological space structure, and a borel space structure, if there exists a homeomorphism `f` from `α` to `β`, then the measure obtained by pushing forward `μ` via `f` is also a regular measure. This essentially means that under these conditions, the property of being a regular measure is preserved under the operation of pushing forward by a homeomorphism.
More concisely: If `α` and `β` are measurable spaces with topological spaces and borel structures, `μ` is a regular measure on `α`, `f` is a homeomorphism from `α` to `β`, then the pushforward measure `f_*\mu` on `β` is also a regular measure.
|
MeasurableSet.exists_isClosed_lt_add
theorem MeasurableSet.exists_isClosed_lt_add :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.WeaklyRegular] {s : Set α},
MeasurableSet s → ↑↑μ s ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ s, IsClosed K ∧ ↑↑μ s < ↑↑μ K + ε
The theorem `MeasurableSet.exists_isClosed_lt_add` states that for any given measurable space `α` with a topological space structure, a weakly regular measure `μ` on `α`, and a measurable set `s` such that `μ` is finite on `s`, and for any positive extended nonnegative real number `ε`, there exists a closed set `K` that is a subset of `s`, such that the measure of `s` is less than the measure of `K` plus `ε`.
More concisely: For any measurable space with a topological structure, weakly regular measure, and measurable set with finite measure, there exists a closed subset with strictly smaller measure.
|
MeasurableSet.exists_isCompact_diff_lt
theorem MeasurableSet.exists_isCompact_diff_lt :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : OpensMeasurableSpace α] [inst_3 : T2Space α] [inst_4 : μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
MeasurableSet A → ↑↑μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ ↑↑μ (A \ K) < ε
This theorem states that for a given measure `μ` that is inner regular for finite measure sets with respect to compact sets, any measurable set of finite measure can be approximated by a compact subset. More specifically, if `A` is a measurable set such that its measure under `μ` is not infinite, then for any non-zero extended nonnegative real number `ε`, there exists a compact subset `K` of `A` such that the measure of the difference between `A` and `K` is less than `ε`. This theorem is relevant in the context of measure theory and topological spaces, and it provides a way to approximate measurable sets with compact sets under certain conditions.
More concisely: Given a finite measure `μ` that is inner regular on compact sets, any measurable set of finite measure can be approximated from within by a compact subset up to an arbitrary, non-zero epsilon.
|
MeasureTheory.Measure.InnerRegularWRT.smul
theorem MeasureTheory.Measure.InnerRegularWRT.smul :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q : Set α → Prop},
μ.InnerRegularWRT p q → ∀ (c : ENNReal), (c • μ).InnerRegularWRT p q
The theorem `MeasureTheory.Measure.InnerRegularWRT.smul` states that for any type `α`, measurable space `m`, measure `μ`, and predicates `p` and `q` on sets of `α`, if the measure `μ` is inner regular with respect to `p` and `q`, then for any extended nonnegative real number `c`, the measure `c • μ` (which is the scalar multiplication of `c` and `μ`) is also inner regular with respect to `p` and `q`. In other words, the property of inner regularity is preserved under scalar multiplication of the measure.
More concisely: If measure `μ` is inner regular with respect to predicates `p` and `q` on measurable space `m` of type `α`, then for any extended nonnegative real number `c`, the measure `c • μ` is also inner regular with respect to `p` and `q`.
|
MeasurableSet.exists_isCompact_lt_add
theorem MeasurableSet.exists_isCompact_lt_add :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
MeasurableSet A → ↑↑μ A ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ K ⊆ A, IsCompact K ∧ ↑↑μ A < ↑↑μ K + ε
This theorem states that if a measure `μ` is inner regular for finite measure sets with respect to compact sets, then for any measurable set `A` of finite measure that is not infinite, and for any non-zero extended nonnegative real number `ε`, there exists a compact subset `K` of `A` such that the measure of `A` is less than the measure of `K` plus `ε`. This theorem provides a way to approximate a measurable set with finite measure by a compact subset.
More concisely: If `μ` is an inner regular finite measure, then for every measurable set `A` of finite, non-infinite measure and any `ε > 0`, there exists a compact subset `K` of `A` with `μ(A) < μ(K) + ε`.
|
Set.exists_isOpen_lt_of_lt
theorem Set.exists_isOpen_lt_of_lt :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.OuterRegular] (A : Set α) (r : ENNReal), ↑↑μ A < r → ∃ U ⊇ A, IsOpen U ∧ ↑↑μ U < r
This theorem states that for any type `α` that is both a measurable and topological space, for any measure `μ` of this space that is outer regular, for any set `A` of type `α`, and for any extended nonnegative real number `r`, if the measure of `A` is less than `r`, then there exists a superset `U` of `A` that is open in the topological space and whose measure is also less than `r`.
More concisely: For any measurable and topological space `(α, τ)` with outer regular measure `μ`, if `A ⊆ α` has measure `μ(A) < r` for some extended nonnegative real `r`, then there exists an open `U ⊇ A` with `μ(U) < r`.
|
MeasurableSet.measure_eq_iSup_isCompact
theorem MeasurableSet.measure_eq_iSup_isCompact :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] ⦃U : Set α⦄,
MeasurableSet U →
∀ (μ : MeasureTheory.Measure α) [inst_2 : μ.InnerRegular],
↑↑μ U = ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : IsCompact K), ↑↑μ K
The theorem `MeasurableSet.measure_eq_iSup_isCompact` states that for any type `α` with a measurable space structure and a topological space structure, given any measurable set `U`, the measure of `U` (with respect to any measure `μ` that has the property of inner regularity) is equal to the supremum of the measures of all compact subsets of `U`. In other words, for any measurable set, its measure can be approximated from within by compact subsets.
More concisely: For any measurable set `U` in a type `α` with inner regular measure `μ`, the measure of `U` equals the supremum of measures of its compact subsets.
|
MeasurableSet.exists_lt_isCompact_of_ne_top
theorem MeasurableSet.exists_lt_isCompact_of_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
MeasurableSet A → ↑↑μ A ≠ ⊤ → ∀ {r : ENNReal}, r < ↑↑μ A → ∃ K ⊆ A, IsCompact K ∧ r < ↑↑μ K
The theorem `MeasurableSet.exists_lt_isCompact_of_ne_top` states that if a measure `μ` is inner regular with regards to compact sets for finite measure sets, then for any measurable set `A` of finite measure (i.e., the measure of `A` is not infinite), you can approximate it with a compact subset `K`. More specifically, for any extended nonnegative real number `r` that is less than the measure of `A`, there exists a compact subset `K` of `A` such that `r` is also less than the measure of `K`.
More concisely: For any finite measure measurable set `A` and any `r` strictly less than its measure in an inner regular measure `μ`, there exists a compact subset `K` of `A` with `r` as a lower bound for its measure.
|
MeasureTheory.Measure.InnerRegularWRT.trans
theorem MeasureTheory.Measure.InnerRegularWRT.trans :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p q q' : Set α → Prop},
μ.InnerRegularWRT p q → μ.InnerRegularWRT q q' → μ.InnerRegularWRT p q'
The theorem `MeasureTheory.Measure.InnerRegularWRT.trans` states that for any type `α`, measurable space `m` and measure `μ` on `α`, and any predicates `p`, `q`, and `q'` on the set of `α`, if the measure `μ` is inner regular with respect to `p` and `q`, and also inner regular with respect to `q` and `q'`, then it is inner regular with respect to `p` and `q'`. In other words, inner regularity with respect to two pairs of predicates is transitive. This means that given a set `U` for which `q' U` holds, and a real number `r` less than the measure of `U`, we can find a subset `K` of `U` such that `p K` holds and the measure of `K` is greater than `r`.
More concisely: If measures μ on a measurable space (α, m) are inner regular with respect to predicates p and q, and inner regular with respect to q and q', then they are inner regular with respect to p and q'.
|
IsCompact.measure_eq_iInf_isOpen
theorem IsCompact.measure_eq_iInf_isOpen :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : μ.InnerRegularCompactLTTop] [inst_3 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_4 : R1Space α]
[inst_5 : BorelSpace α] {K : Set α}, IsCompact K → ↑↑μ K = ⨅ U, ⨅ (_ : K ⊆ U), ⨅ (_ : IsOpen U), ↑↑μ U
The theorem `IsCompact.measure_eq_iInf_isOpen` states that given a measurable space `α` equipped with a topological space structure and a measure `μ`, under certain conditions, any compact set can be approximated from outside by open sets. Specifically, if `μ` is inner regular for finite measure sets with respect to compact sets, and `μ` is locally finite in an R₁ space, then for any compact set `K`, the measure of `K` is equal to the infimum of the measures of open sets `U` that contain `K`. These conditions ensure that the measure `μ` interacts well with the topological structure of `α`, and `K` can be approximated by a family of open sets in a desirable way.
More concisely: If `μ` is an inner regular and locally finite measure on the measurable space `(α, Σ)` with a topological structure, then for any compact set `K ∈ Σ`, one has `μ(K) = inf {μ(U) : U ∈ Σ, K ⊆ U}`.
|
MeasureTheory.Measure.Regular.restrict_of_measure_ne_top
theorem MeasureTheory.Measure.Regular.restrict_of_measure_ne_top :
∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] {μ : MeasureTheory.Measure α}
[inst_2 : R1Space α] [inst_3 : BorelSpace α] [inst_4 : μ.Regular] {A : Set α},
↑↑μ A ≠ ⊤ → (μ.restrict A).Regular
The theorem states that the restriction of a regular measure to a set with finite measure is also a regular measure. In the specific terms, for any type `α` equipped with a measurable space structure, a topological space structure, and an `R1Space` and `BorelSpace` structure, given any regular measure `μ` on `α` and any set `A` of `α`, if the measure of `A` under `μ` is not infinite, then the measure obtained by restricting `μ` to `A` is also a regular measure.
More concisely: If `α` is a measurable space with a regular measure `μ`, and `A` is a subset of `α` with finite measure under `μ`, then the restriction of `μ` to `A` is also a regular measure.
|
MeasureTheory.Measure.InnerRegularWRT.of_restrict
theorem MeasureTheory.Measure.InnerRegularWRT.of_restrict :
∀ {α : Type u_1} [inst : MeasurableSpace α] {p : Set α → Prop} {μ : MeasureTheory.Measure α} {s : ℕ → Set α},
(∀ (n : ℕ), (μ.restrict (s n)).InnerRegularWRT p MeasurableSet) →
Set.univ ⊆ ⋃ n, s n → Monotone s → μ.InnerRegularWRT p MeasurableSet
The theorem `MeasureTheory.Measure.InnerRegularWRT.of_restrict` states that for a given measurable space `α`, a property `p` on the sets of `α`, a measure `μ` on `α`, and a sequence of sets `s` in `α`, if the restrictions of the measure `μ` to each set in the monotone sequence `s` are inner regular with respect to the property `p` and all measurable sets, and if the union of all sets in the sequence `s` covers the entire space, then the measure `μ` itself is inner regular with respect to the property `p` and all measurable sets. This means that the inner regularity of the measure restricted to each set in a monotone sequence that covers the space implies the inner regularity of the measure itself.
More concisely: If for a measurable space and property, a sequence of measurable sets with monotone increasing union covering the space, and a measure, the restrictions of to each are inner regular with respect to with all measurable sets, then is itself inner regular with respect to and all measurable sets.
|
MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace
theorem MeasureTheory.Measure.InnerRegularWRT.of_pseudoMetrizableSpace :
∀ {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace.PseudoMetrizableSpace X]
[inst_2 : MeasurableSpace X] (μ : MeasureTheory.Measure X), μ.InnerRegularWRT IsClosed IsOpen
This theorem states that in a pseudo-metrizable space, which is a mild generalization of a metrizable space, any open set can be approximated from the inside by closed sets. Specifically, given a measure `μ` on the space, the measure is inner regular with respect to the properties of being closed and open. This means that for every open set `U` and any real number `r` less than the measure of `U`, there exists a closed subset `K` of `U` such that the measure of `K` is greater than `r`. This theorem allows us to approximate the measure of an open set by the measures of its closed subsets.
More concisely: In a pseudo-metrizable space equipped with a measure, every open set can be approximated from the inside by closed sets with respect to measure.
|