MeasureTheory.OuterMeasure.coe_smul
theorem MeasureTheory.OuterMeasure.coe_smul :
∀ {α : Type u_1} {R : Type u_3} [inst : SMul R ENNReal] [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R)
(m : MeasureTheory.OuterMeasure α), ↑(c • m) = c • ↑m
The theorem `MeasureTheory.OuterMeasure.coe_smul` states that for any type `α`, any type `R` that has a scalar multiplication operation with extended non-negative real numbers (`ENNReal`), and assuming `R` forms a scalar tower with `ENNReal`, then for any scalar `c` of type `R` and any outer measure `m` of type `α`, the coercion of the scalar multiplication of `c` and `m` is equivalent to the scalar multiplication of `c` and the coercion of `m`. In other words, scalar multiplication commutes with the coercion operation in the context of outer measures.
More concisely: For any outer measure `m` on type `α` and scalar `c` in a type `R` with a commutative scalar multiplication and extended non-negative real numbers, the coercion of `c * m` is equivalent to `c * (coe m)`.
|
MeasureTheory.OuterMeasure.union
theorem MeasureTheory.OuterMeasure.union :
∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α) (s₁ s₂ : Set α), ↑m (s₁ ∪ s₂) ≤ ↑m s₁ + ↑m s₂
The theorem `MeasureTheory.OuterMeasure.union` states that for any given type `α`, any outer measure `m` on `α`, and any two sets `s₁` and `s₂` of `α`, the measure of the union of `s₁` and `s₂` is less than or equal to the sum of the measures of `s₁` and `s₂`. This is a formal statement of the subadditivity property of outer measures. In mathematical notation, this would be written as m(s₁ ∪ s₂) ≤ m(s₁) + m(s₂).
More concisely: For any outer measure `m` on a type `α`, the measure of the union of any two sets `s₁` and `s₂` satisfies `m(s₁ ∪ s₂) ≤ m(s₁) + m(s₂)`.
|
MeasureTheory.extend_eq
theorem MeasureTheory.extend_eq :
∀ {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : P s), MeasureTheory.extend m s = m s h
The theorem `MeasureTheory.extend_eq` states that for any type `α`, any property `P` on `α`, and any function `m` from elements of `α` satisfying `P` to the extended nonnegative real numbers (`ENNReal`), if `s` is an element of `α` that satisfies `P`, then applying the `MeasureTheory.extend` function to `m` and `s` gives the same result as directly applying `m` to `s` and the proof that `s` satisfies `P`. In other words, `MeasureTheory.extend` indeed extends the function `m` without altering its original values on elements that satisfy the property `P`.
More concisely: For any type `α`, property `P` on `α`, and function `m` from `P`-elements of `α` to `ENNReal`, `MeasureTheory.extend m s = m s` holds for any `s` satisfying `P`.
|
MeasureTheory.OuterMeasure.iUnion
theorem MeasureTheory.OuterMeasure.iUnion :
∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {β : Type u_5} [inst : Countable β] (s : β → Set α),
↑m (⋃ i, s i) ≤ ∑' (i : β), ↑m (s i)
This theorem states that for any outer measure `m` on a type `α` and for any countable set `β`, the outer measure of the union of a collection of sets `s : β → Set α` (that is, a collection of sets indexed by `β`) is less than or equal to the sum of the outer measures of the individual sets in that collection. This theorem encapsulates a property of outer measures that allows us to approximate them by summing over smaller sets, which plays an important role in measure theory.
More concisely: For any outer measure `m` on a type `α` and countable collection `s : β → Set α` of sets, `m(⋃ i in β, s i) ≤ ∑ i in β, m(s i)`.
|
MeasureTheory.OuterMeasure.coe_fn_injective
theorem MeasureTheory.OuterMeasure.coe_fn_injective : ∀ {α : Type u_1}, Function.Injective fun μ s => ↑μ s
This theorem states that for any type `α`, the function that takes a measure `μ` and a set `s` and returns the measure of the set `s` with respect to the measure `μ`, is injective. That means, if the measure of two different sets `s1` and `s2` with respect to the same measure `μ` are equal, then the sets `s1` and `s2` must be the same. In mathematical terms, for all `μ, s1, s2`, if `μ(s1) = μ(s2)`, then `s1 = s2`. This is a property of measures in measure theory.
More concisely: For any measure `μ` in measure theory, the measure function is injective, that is, `μ(s1) = μ(s2)` implies `s1 = s2` for all sets `s1` and `s2`.
|
MeasureTheory.OuterMeasure.top_apply
theorem MeasureTheory.OuterMeasure.top_apply : ∀ {α : Type u_1} {s : Set α}, s.Nonempty → ↑⊤ s = ⊤
The theorem `MeasureTheory.OuterMeasure.top_apply` states that for any type `α` and any set `s` of type `α`, if the set `s` is nonempty (i.e., there exists at least one element in `s`), then the application of the top outer measure (denoted by `↑⊤`) to the set `s` equals the top element in the order of outer measures (denoted by `⊤`). This essentially means that the outer measure of any nonempty set according to the most inclusive (or 'top') measure is itself the 'top' or maximum possible measure.
More concisely: For any nonempty set `s` in a measurable space, the top outer measure `⊤(s)` equals the application of the top measure `↑⊤` to `s`.
|
MeasureTheory.OuterMeasure.isCaratheodory_iff_le
theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le :
∀ {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α},
MeasurableSet s ↔ ∀ (t : Set α), ↑m (t ∩ s) + ↑m (t \ s) ≤ ↑m t
This theorem, `MeasureTheory.OuterMeasure.isCaratheodory_iff_le`, states that for any type `α`, any outer measure `m` on `α`, and any set `s` of type `α`, the set `s` is measurable if and only if for all sets `t` of type `α`, the sum of the measures of the intersection of `t` and `s` and the set difference of `t` and `s` is less than or equal to the measure of `t`. Here, the measure of a set is obtained using the outer measure `m`. This theorem relates the concept of measurability of a set to the property of being Caratheodory measurable, which involves the measures of intersections and differences of sets.
More concisely: For any outer measure `m` on a type `α`, a set `s` is measurable if and only if for all sets `t`, the measure of `s ∩ t` plus the measure of `s \ t` is less than or equal to the measure of `t`.
|
MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter
theorem MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter :
∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} {s t : Set α},
(∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → ¬P u) →
↑(MeasureTheory.inducedOuterMeasure m P0 m0) (s ∪ t) =
↑(MeasureTheory.inducedOuterMeasure m P0 m0) s + ↑(MeasureTheory.inducedOuterMeasure m P0 m0) t
The theorem `MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter` states that for any type `α`, given a property `P` on sets of `α`, a function `m` which maps sets satisfying `P` to extended nonnegative real numbers, and the conditions `P0` and `m0` which ensure that the empty set satisfies `P` and `m` maps the empty set to 0, respectively, and any two sets `s` and `t` of `α`, if there does not exist any set `u` that intersects both `s` and `t` non-trivially and satisfies `P`, then the value of the induced outer measure on the union of `s` and `t` is the sum of the induced outer measure on `s` and the induced outer measure on `t`.
For example, if `α` is considered as an (e)metric space and `P` as a property stating that the diameter of a set is less than some `r`, then the theorem ensures that for any two sets `s` and `t` such that the extended distance between any two points `x` from `s` and `y` from `t` is at least `r`, the induced outer measure on the union of `s` and `t` equals the sum of the induced outer measures on `s` and `t`.
More concisely: For any type `α`, property `P` on sets of `α`, and function `m` mapping `P` sets to extended nonnegative reals with `m∅ = 0`, if there is no set `u` intersecting both `s` and `t` non-trivially that satisfies `P`, then `m(s ∪ t) = ms + mt`.
|
Mathlib.MeasureTheory.OuterMeasure.Basic._auxLemma.8
theorem Mathlib.MeasureTheory.OuterMeasure.Basic._auxLemma.8 :
∀ {α : Type u_1} {ι : Sort u_5} [inst : CompleteLattice α] {f : ι → α} {a : α}, (a ≤ iInf f) = ∀ (i : ι), a ≤ f i
This theorem states that for any type `α` which forms a complete lattice, for any index set `ι` and for any function `f` mapping `ι` to `α`, and for any element `a` of `α`, `a` is less than or equal to the indexed infimum (`iInf`) of `f` if and only if `a` is less than or equal to `f(i)` for every `i` in `ι`. In mathematical terms, we could write this as $a \leq \inf_i f(i)$ if and only if $a \leq f(i)$ for all indices $i$. This is essentially unpacking the definition of the infimum in terms of the original function `f`.
More concisely: For any complete lattice `α`, index set `ι`, and function `f` from `ι` to `α`, an element `a` in `α` is less than or equal to the indexed infimum `iInf(f)` if and only if it is less than or equal to `f(i)` for all `i` in `ι`. In other words, `a ≤ iInf(f)` if and only if `a ≤ f(i)` for all `i` in `ι`.
|
MeasureTheory.OuterMeasure.iUnion_null
theorem MeasureTheory.OuterMeasure.iUnion_null :
∀ {α : Type u_1} {ι : Sort u_5} [inst : Countable ι] (m : MeasureTheory.OuterMeasure α) {s : ι → Set α},
(∀ (i : ι), ↑m (s i) = 0) → ↑m (⋃ i, s i) = 0
This theorem in Measure Theory pertains to the notion of an outer measure. It states that for any type `α` and any index type `ι` that is countable, given an outer measure `m` on `α` and a function `s` mapping `ι` to sets of `α`, if the measure of every set `s i` is zero, then the measure of the union of all such sets (denoted by `⋃ i, s i`) is also zero. In essence, if each set in a countable collection has measure zero, then the entire collection together also has measure zero.
More concisely: If `m` is an outer measure on a type `α` and `ι` is a countable index type, then `m (⋃ i, s i) = 0` whenever `m (s i) = 0` for all `i ∈ ι`.
|
MeasureTheory.OuterMeasure.comap_apply
theorem MeasureTheory.OuterMeasure.comap_apply :
∀ {α : Type u_1} {β : Type u_5} (f : α → β) (m : MeasureTheory.OuterMeasure β) (s : Set α),
↑((MeasureTheory.OuterMeasure.comap f) m) s = ↑m (f '' s)
This theorem states that for any two types α and β, a function `f` from α to β, a measure `m` on β, and a set `s` of type α, the measure of the preimage of the set `s` under `f` using the pullback of the measure `m` (`(MeasureTheory.OuterMeasure.comap f) m`) is equal to the measure of the image of `s` under `f` using `m`. In other words, pulling back the measure `m` with `f` and then applying it to `s` gives us the same result as applying `m` to the image of `s` under `f`.
More concisely: For any measure `m` on type β, the pullback measure of `m` through a function `f` from type α to β, and any set `s` of type α, the measure of `s` under the pullback measure equals the measure of the image of `s` under `f` using `m`.
|
MeasureTheory.OuterMeasure.empty'
theorem MeasureTheory.OuterMeasure.empty' : ∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α), ↑m ∅ = 0
This theorem states that for any type `α` and any outer measure `m` of type `MeasureTheory.OuterMeasure α`, the measure of the empty set is zero. In other words, in the context of measure theory and for any given outer measure, the measure of an empty set is universally zero.
More concisely: For any outer measure `m`, the measure of the empty set is 0: `m ∘ isEmpty = 0`.
|
MeasureTheory.OuterMeasure.trim_sup
theorem MeasureTheory.OuterMeasure.trim_sup :
∀ {α : Type u_1} [inst : MeasurableSpace α] (m₁ m₂ : MeasureTheory.OuterMeasure α),
(m₁ ⊔ m₂).trim = m₁.trim ⊔ m₂.trim
The theorem `MeasureTheory.OuterMeasure.trim_sup` states that for any two outer measures `m₁` and `m₂` in a measurable space `α`, the "trim" operation sends the supremum (least upper bound) of `m₁` and `m₂` to the supremum of the trimmed versions of `m₁` and `m₂`. In other words, trimming the supremum of two outer measures results in the supremum of their individual trimmed measures.
More concisely: For any two outer measures `m₁` and `m₂` in a measurable space `α`, `MeasureTheory.OuterMeasure.trim_sup m₁ (trim m₂) = trim (m₁ ��ustral m₂)`.
|
MeasureTheory.OuterMeasure.trim_eq
theorem MeasureTheory.OuterMeasure.trim_eq :
∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) {s : Set α},
MeasurableSet s → ↑m.trim s = ↑m s
This theorem, `MeasureTheory.OuterMeasure.trim_eq`, states that for any type `α` equipped with a `MeasurableSpace` instance, any outer measure `m` on `α`, and any set `s` of type `α`, if `s` is a measurable set, then the value of the trimmed outer measure `m` at `s` is equal to the value of the original outer measure `m` at `s`. In other words, trimming an outer measure does not change its value on measurable sets.
More concisely: For any measurable space `(α, Σ, mu)` and measurable set `s ∈ Σ`, the trimmed outer measure `muᵢ(s)` equals the original outer measure `mu(s)`.
|
MeasureTheory.inducedOuterMeasure_eq
theorem MeasureTheory.inducedOuterMeasure_eq :
∀ {α : Type u_1} [inst : MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0),
(∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
Pairwise (Disjoint on f) → m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) →
∀ {s : Set α} (hs : MeasurableSet s), ↑(MeasureTheory.inducedOuterMeasure m ⋯ m0) s = m s hs
This theorem, `MeasureTheory.inducedOuterMeasure_eq`, states that for any type `α` in a measurable space, given a function `m` from a measurable set of `α` to the extended nonnegative real numbers (abbreviated as `ENNReal`), such that `m` of the empty set is zero, if for any sequence of measurable sets `(f i)` that are pairwise disjoint, the measure `m` of the union of these sets equals the sum of the measures of each set in the sequence, then for any measurable set `s`, the measure of `s` under the outer measure induced by `m` equals the original measure `m` of `s`.
In simpler terms, this theorem asserts that if a measure on a collection of measurable sets satisfies certain properties (it is zero on the empty set and additive over countable disjoint unions), then the outer measure it induces coincides with the original measure on these sets.
More concisely: If a measure on a collection of measurable sets is additive and zero on the empty set, then it is equal to the outer measure induced by that measure on any measurable set.
|
MeasureTheory.inducedOuterMeasure_eq_iInf
theorem MeasureTheory.inducedOuterMeasure_eq_iInf :
∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
(PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
(∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
(∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
∀ (s : Set α), ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s = ⨅ t, ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht
This theorem states that, for any type `α`, any property `P` of sets of `α`, any function `m` from sets of `α` satisfying `P` to the extended nonnegative real numbers, any proof `P0` that the empty set satisfies `P`, and any proof `m0` that `m` applied to the empty set is zero, if `P` is closed under countable unions `PU` and `m` is countably subadditive, and `m` is monotonic with respect to set inclusion, then for every set `s` of `α`, the value of the induced outer measure on `s` is equal to the infimum over all sets `t` satisfying `P` that contain `s` of `m(t)`.
In other words, the outer measure induced by `m` under these conditions is the infimum of `m` over all sets containing the given set, among those sets that satisfy `P`.
More concisely: Given a type `α`, a property `P` of sets of `α`, a function `m` from `P` sets to extended nonnegative real numbers satisfying countable subadditivity, monotonicity, and closure under countable unions, and proofs that the empty set satisfies `P` and `m` applied to the empty set is zero, then for any set `s` of `α`, the outer measure of `s` equals the infimum of `m` over all `P` sets containing `s`.
|
MeasureTheory.OuterMeasure.restrict_apply
theorem MeasureTheory.OuterMeasure.restrict_apply :
∀ {α : Type u_1} (s t : Set α) (m : MeasureTheory.OuterMeasure α),
↑((MeasureTheory.OuterMeasure.restrict s) m) t = ↑m (t ∩ s)
The theorem `MeasureTheory.OuterMeasure.restrict_apply` states that for any types `α`, and for any sets `s` and `t` of type `α`, and for any outer measure `m` of type `α`, the outer measure `m` restricted to the set `s` and then applied to the set `t` is equal to the outer measure `m` applied to the intersection of sets `t` and `s`. In other words, restricting an outer measure to a subset and then measuring another set is the same as measuring the intersection of the two sets with the original outer measure.
More concisely: For any outer measure `m` on a type `α`, and sets `s` and `t` of type `α`, `m` applied to the intersection of `s` and `t` is equal to the restriction of `m` to `s` and then the application to `t`.
|
MeasureTheory.OuterMeasure.sInf_apply'
theorem MeasureTheory.OuterMeasure.sInf_apply' :
∀ {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α},
s.Nonempty → ↑(sInf m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, ↑μ (t n)
This theorem states that for any type `α`, any set `m` of outer measures on `α`, and any non-empty set `s` of `α`, the infimum value of the outer measures in `m` applied to `s` is equal to the infimum of the sum of measures of a countably infinite sequence of sets `t` that cover `s`. For each set `t_n` in this covering sequence, the measure used could be a different one from the set `m` of outer measures. This theorem therefore provides a detailed description of how to calculate the infimum of a set of outer measures applied to a non-empty set `s`.
More concisely: For any type `α`, any non-empty set `s` of `α`, and any set `m` of outer measures on `α`, the infimum of the outer measures in `m` applied to `s` equals the infimum of the sums of measures in `m` of countably many sets covering `s`.
|
MeasureTheory.OuterMeasure.biInf_apply'
theorem MeasureTheory.OuterMeasure.biInf_apply' :
∀ {α : Type u_1} {ι : Type u_2} (I : Set ι) (m : ι → MeasureTheory.OuterMeasure α) {s : Set α},
s.Nonempty → ↑(⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, ↑(m i) (t n)
The theorem `MeasureTheory.OuterMeasure.biInf_apply'` states that for any type `α` and `ι`, given a set `I` of type `ι`, a function `m` mapping elements of `ι` to outer measures on `α`, and a nonempty set `s` of type `α`, the infimum value of the outer measures (`m i`) for `i` in `I` applied to `s` is equal to the infimum over all possible sequences `t` such that `s` is a subset of the indexed union of `t`. For each natural number `n`, the value is the infimum of the outer measures (`m i`) for `i` in `I` applied to `t n`. In other words, it is not simply the minimum value of a measure on the set `s`, but rather the infimum sum of measures of a countable set of sets `t` that covers `s`, for which a different measure can be used for each set in the cover.
More concisely: The infimum of the outer measures of a set with respect to a family of measures indexed by a set is equal to the infimum of the sums of measures of countable subsets that cover the set.
|
MeasureTheory.inducedOuterMeasure_eq'
theorem MeasureTheory.inducedOuterMeasure_eq' :
∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
(PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
(∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
(∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
∀ {s : Set α} (hs : P s), ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s = m s hs
This theorem is about the equality of an induced outer measure and a given measure function on a particular set. Given a type `α`, a property `P` on sets of `α`, and a measure `m` from the properties of sets to extended nonnegative real numbers (`ENNReal`), that assigns `0` to the empty set, if the following conditions hold:
1. The property `P` is preserved under taking countable unions, i.e., if `P` holds for each set in a sequence of sets, then `P` holds for the union of these sets.
2. The measure of a countable union of sets is at most the sum of the measures of the sets.
3. For any two sets where the first set is a subset of the second and `P` holds for both sets, the measure of the first set is less than or equal to the measure of the second set.
Then, for any set `s` satisfying the property `P`, the induced outer measure of `s` equals the measure `m` of `s`.
More concisely: If `P` is a countably additive property on sets such that `m(∅) = 0` and `m` is monotonic on `P` sets, then for any `P` set `s`, the induced outer measure of `s` equals `m(s)`.
|
MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict
theorem MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict :
∀ {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) {s : Set α},
m.Nonempty →
(MeasureTheory.OuterMeasure.restrict s) (sInf m) = sInf (⇑(MeasureTheory.OuterMeasure.restrict s) '' m)
This theorem states that for any type `α`, a set `m` of outer measures on `α`, and a set `s` of elements of type `α`, if `m` is nonempty, then the infimum (`sInf`) of the set of outer measures `m` restricted to the set `s` is the same as the infimum of the set obtained by restricting each outer measure in `m` to `s`. In simpler terms, it says that the process of restriction commutes with taking the infimum in the context of outer measures, provided that the set of outer measures is not empty.
More concisely: For any non-empty set `m` of outer measures on type `α` and set `s` of elements of type `α`, the infimum of `m` restricted to `s` equals the infimum of the set of restrictions of measures in `m` to `s`.
|
MeasureTheory.OuterMeasure.ofFunction_eq
theorem MeasureTheory.OuterMeasure.ofFunction_eq :
∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α),
(∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t) →
(∀ (s : ℕ → Set α), m (⋃ i, s i) ≤ ∑' (i : ℕ), m (s i)) →
↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s = m s
This theorem states that for any type `α`, given a function `m` that assigns measures to sets (with the property that `m` of the empty set is zero) and a set `s` of type `α`, if two conditions are satisfied: first, for any set `t` that contains `s`, the measure of `s` is less than or equal to the measure of `t`; and second, the measure of the union of a sequence of sets is less than or equal to the sum of the measures of the individual sets in the sequence, then the measure of `s` under the maximal outer measure `μ` constructed by `MeasureTheory.OuterMeasure.ofFunction` is equal to `m s`. In other words, the maximal outer measure `μ` is consistent with the original measure assigning function `m` under these conditions.
More concisely: If `m` is a measure function on type `α` with `m ∅ = 0`, and for any set `s` and any set `t` containing `s`, `m s ≤ m t`, and the measure of any countable union equals the sum of the measures of its elements, then `m s = μ s`, where `μ` is the maximal outer measure constructed from `m`.
|
MeasureTheory.OuterMeasure.trim_smul
theorem MeasureTheory.OuterMeasure.trim_smul :
∀ {α : Type u_1} [inst : MeasurableSpace α] {R : Type u_2} [inst_1 : SMul R ENNReal]
[inst_2 : IsScalarTower R ENNReal ENNReal] (c : R) (m : MeasureTheory.OuterMeasure α),
(c • m).trim = c • m.trim
The theorem `MeasureTheory.OuterMeasure.trim_smul` states that for any type `α` with a `MeasurableSpace` structure, any type `R` with a scalar multiplication (`SMul`) structure on extended nonnegative real numbers (`ENNReal`), and any instance showing that `R` is a scalar tower over `ENNReal`, the `trim` operation on an outer measure is compatible with scalar multiplication. More specifically, if `c` is a scalar of type `R` and `m` is an outer measure on `α`, then the `trim` of the outer measure scaled by `c` (`c • m`) is equal to the outer measure of the trimmed measure scaled by `c` (`c • m.trim`).
More concisely: For any measurable space `(α, Σ)`, scalar multiplication `R` on extended nonnegative real numbers `ENNReal`, and a scalar `c` in `R`, the outer measures `c • m` and `c • m.trim` are equal, where `m` is an outer measure on `α`.
|
MeasureTheory.OuterMeasure.trim_binop
theorem MeasureTheory.OuterMeasure.trim_binop :
∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ m₃ : MeasureTheory.OuterMeasure α}
{op : ENNReal → ENNReal → ENNReal},
(∀ (s : Set α), ↑m₁ s = op (↑m₂ s) (↑m₃ s)) → ∀ (s : Set α), ↑m₁.trim s = op (↑m₂.trim s) (↑m₃.trim s)
The given theorem is about the operation on outer measures in measure theory. It states that if we have three outer measures `m₁`, `m₂`, and `m₃`, and an operation `op` on the extended nonnegative real numbers such that for every set `s`, the measure `m₁` of `s` equals the result of applying operation `op` to the measures `m₂` and `m₃` of `s`, then the same relationship holds when we consider the trimmed versions of these measures. In other words, if the measure of a set under `m₁` equals the result of some operation on the measures under `m₂` and `m₃`, this property will still hold true after trimming these measures.
More concisely: If outer measures $m\_1$, $m\_2$, and $m\_3$ satisfy $m\_1(S) = \operatorop{op}(m\_2(S), m\_3(S))$ for all sets $S$, then $m\_{1\text{-}trim}(S) = \operatorop{op}(m\_{2\text{-}trim}(S), m\_{3\text{-}trim}(S))$ for all sets $S$.
|
MeasureTheory.OuterMeasure.le_trim
theorem MeasureTheory.OuterMeasure.le_trim :
∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α), m ≤ m.trim
This theorem states that for any outer measure `m` on a measurable space `α`, `m` is less than or equal to the trimmed outer measure `m.trim`. In other words, the original outer measure does not exceed the trimmed measure, which is the unique maximal outer measure that is less than or equivalent to the original outer measure when restricted to measurable sets.
More concisely: For any outer measure `m` on a measurable space `α`, we have `m ≤ m.trim`.
|
MeasureTheory.OuterMeasure.le_trim_iff
theorem MeasureTheory.OuterMeasure.le_trim_iff :
∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ : MeasureTheory.OuterMeasure α},
m₁ ≤ m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s
This theorem states that for any type `α` with a given `MeasurableSpace` structure and any two outer measures `m₁` and `m₂` on `α`, the measure `m₁` is less than or equal to the trimmed measure of `m₂` if and only if for every set `s` of `α` that is measurable, the measure of `s` under `m₁` is less than or equal to its measure under `m₂`. In mathematical terms, this could be written as: \(m_1 \leq \text{{trim}}(m_2) \iff \forall s: \text{{MeasurableSet }} s \rightarrow m_1(s) \leq m_2(s)\).
More concisely: For any measurable spaces `(α, Σ)` and measurable sets `s` in `α`, and for any outer measures `m₁` and `m₂` on `α`, the inequality `m₁ ≤ trim(m₂)` holds if and only if `m₁(s) ≤ m₂(s)` for all measurable sets `s`.
|
MeasureTheory.OuterMeasure.sUnion_null_iff
theorem MeasureTheory.OuterMeasure.sUnion_null_iff :
∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {S : Set (Set α)},
S.Countable → (↑m S.sUnion = 0 ↔ ∀ s ∈ S, ↑m s = 0)
This theorem is stating that for any type `α`, given an outer measure `m` on `α` and a countable collection of sets `S` of type `α`, the measure of the union of sets `S` is zero if and only if the measure of each set `s` in `S` is also zero. In mathematical terms, if `S` is a countable collection of subsets of a set `α` and `m` is an outer measure on `α`, then the total measure (according to `m`) of the union of all the sets in `S` is zero if and only if the measure of every set in `S` is zero.
More concisely: For any outer measure `m` on a type `α` and countable collection `S` of subsets of `α`, the union of sets in `S` has measure zero if and only if every set in `S` has measure zero.
|
MeasureTheory.extend_iUnion_le_tsum_nat'
theorem MeasureTheory.extend_iUnion_le_tsum_nat' :
∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal}
(PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
(∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
∀ (s : ℕ → Set α), MeasureTheory.extend m (⋃ i, s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)
The theorem `MeasureTheory.extend_iUnion_le_tsum_nat'` states that for any type `α`, any predicate `P` over sets of `α`, and `m` a function from sets satisfying `P` to the extended nonnegative real numbers, if for any sequence of sets (indexed over the natural numbers) that all satisfy `P`, the measure of the union of the sets is less than or equal to the sum of the measures of the individual sets, then this inequality still holds when we extend the function `m` to sets that may not satisfy `P`. In more succinct terms, it says that the measure of a countable union of sets is less than or equal to the sum of the measures of the individual sets, even when we extend the measure function beyond its original domain.
More concisely: Given a type α, a predicate P over sets of α, and a function m from sets satisfying P to extended nonnegative reals, if the union of any countable sequence of sets satisfying P has measure less than or equal to the sum of the measures of its elements according to m, then this inequality holds for the extended measure function m' that includes sets not satisfying P.
|
MeasureTheory.OuterMeasure.boundedBy.proof_1
theorem MeasureTheory.OuterMeasure.boundedBy.proof_1 :
∀ {α : Type u_1} (m : Set α → ENNReal), ⨆ (_ : ∅.Nonempty), m ∅ = 0
The theorem `MeasureTheory.OuterMeasure.boundedBy.proof_1` states that for any function `m` from a set of elements of arbitrary type `α` to the extended nonnegative real numbers (usually denoted by `[0, ∞]`), the supremum of `m ∅` over the condition that the empty set is nonempty (which is never true) is equal to zero. In other words, in the context of measure theory, the measure of the empty set is always zero, regardless of how the measure function is defined.
More concisely: The measure of the empty set, under any measure function, is equal to 0.
|
MeasureTheory.OuterMeasure.biInf_apply
theorem MeasureTheory.OuterMeasure.biInf_apply :
∀ {α : Type u_1} {ι : Type u_2} {I : Set ι},
I.Nonempty →
∀ (m : ι → MeasureTheory.OuterMeasure α) (s : Set α),
↑(⨅ i ∈ I, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, ↑(m i) (t n)
This theorem states that for a nonempty set `I` of indices and a function `m` mapping each index to an 'outer measure' on a set, the infimum (greatest lower bound) of these measures applied to a set `s` is equal to the infimum of the sum of measures of countable sets that cover `s`. It's important to note that a different measure can be used for each set in the cover. In other words, the infimum measure of `s` is not simply the smallest measure of `s`, but the infimum of the sum of measures for all possible countable covers of `s`, potentially using a different measure for each subset in the cover.
More concisely: For a nonempty index set `I` and a function `m` mapping each index to an outer measure, the infimum of the function `m` over a set `s` equals the infimum of the sums of `m(i)(S\_i)` over all countable covers `{S\_i}_i` of `s`.
|
MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim
theorem MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim :
∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Sort u_2} [inst_1 : Countable ι]
(μ : ι → MeasureTheory.OuterMeasure α) (s : Set α),
∃ t, s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(μ i).trim s
This theorem states that if `μ i` represents a countable family of outer measures, then for any set `s`, there exists a measurable set `t` that is a superset of `s` (`s ⊆ t`) such that the measure of `t` with respect to `μ i` equals the trimmed measure of `s` with respect to `μ i` for every `i`. In other words, for every set `s`, we can always find a measurable superset `t` such that the outer measures of `t` and the trimmed measure of `s` are equal for all `i` in the countable index set.
More concisely: For any countable family `μ i` of outer measures and any set `s`, there exists a measurable superset `t` of `s` such that `μ i(t) = μ⁎(s)` for all `i`, where `μ⁎(s)` is the trimmed measure of `s`.
|
MeasureTheory.OuterMeasure.ofFunction_le
theorem MeasureTheory.OuterMeasure.ofFunction_le :
∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α),
↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s ≤ m s
The theorem `MeasureTheory.OuterMeasure.ofFunction_le` states that for any type `α`, any function `m` that assigns extended nonnegative real numbers to sets of `α` such that the empty set is assigned 0, and any set `s` of `α`, the outer measure of `s` under the outer measure constructed from `m` (denoted as `MeasureTheory.OuterMeasure.ofFunction m`) is less than or equal to the measure `m` assigns to `s`. Essentially, this theorem expresses that the outer measure created from a measure function will never assign a larger measure to a set than the original measure function.
More concisely: For any function `m` that assigns extended nonnegative real numbers to sets and sets the empty set to 0, the outer measure `MeasureTheory.OuterMeasure.ofFunction m` of a set `s` is less than or equal to `m(s)`.
|
MeasureTheory.OuterMeasure.iInf_apply
theorem MeasureTheory.OuterMeasure.iInf_apply :
∀ {α : Type u_1} {ι : Sort u_2} [inst : Nonempty ι] (m : ι → MeasureTheory.OuterMeasure α) (s : Set α),
↑(⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i, ↑(m i) (t n)
This theorem states that, given a nonempty family of outer measures `m` and a set `s`, the value of the infimum (greatest lower bound) of the family of outer measures on the set is not merely the smallest measure value on that set. Rather, it is the infimum of the sum of measures of a countable collection of sets that envelop the set `s`. Moreover, a different measure from the family can be applied to each set in this cover. The `Set.iUnion` function is used to form the union of this countable collection of sets.
More concisely: Given a nonempty family of outer measures and a set, the infimum of the family is the smallest sum of measures of a countable collection of sets from the family whose union envelops the set.
|
MeasureTheory.OuterMeasure.ext
theorem MeasureTheory.OuterMeasure.ext :
∀ {α : Type u_1} {μ₁ μ₂ : MeasureTheory.OuterMeasure α}, (∀ (s : Set α), ↑μ₁ s = ↑μ₂ s) → μ₁ = μ₂
The theorem `MeasureTheory.OuterMeasure.ext` states that for any given type `α`, if two outer measures `μ₁` and `μ₂` applied to any set `s` of type `α` produce the same result, then `μ₁` and `μ₂` are equal. In other words, two outer measures are considered equal if and only if they yield identical measures for every set of elements of the type `α`.
More concisely: Two outer measures on a type `α` are equal if and only if they agree on the measure of every set.
|
MeasureTheory.inducedOuterMeasure_caratheodory
theorem MeasureTheory.inducedOuterMeasure_caratheodory :
∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0}
(PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)),
(∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ i, f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) →
(∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) →
∀ (s : Set α),
MeasurableSet s ↔
∀ (t : Set α),
P t →
↑(MeasureTheory.inducedOuterMeasure m P0 m0) (t ∩ s) +
↑(MeasureTheory.inducedOuterMeasure m P0 m0) (t \ s) ≤
↑(MeasureTheory.inducedOuterMeasure m P0 m0) t
This theorem states that to check whether a set `s` is Carathéodory-measurable, it suffices to only consider the sets `t` for which the property `P t` holds. More specifically, given a type `α`, a property `P` defined on sets of `α`, a function `m` that assigns to each set satisfying `P` an extended nonnegative real number, and given that `P` is true for the empty set and `m` assigns the value 0 to the empty set, if `P` is preserved under countable unions and `m` is countably sub-additive and monotone on `P` sets, then a set `s` is measurable if and only if for every set `t` satisfying `P`, the induced outer measure of `t` intersected with `s` plus the induced outer measure of `t` minus `s` is less than or equal to the induced outer measure of `t`.
This theorem provides a characterization of Carathéodory-measurability in terms of the property `P` and the function `m`, and it is useful in the theory of measure and integration, specifically in the construction of measures.
More concisely: A set is Carathéodory-measurable if and for every set satisfying a property `P`, the induced outer measure of their intersection and difference is less than or equal to the induced outer measure of that set.
|
MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero
theorem MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero :
∀ {α : Type u_1} {ι : Type u_5} (m : MeasureTheory.OuterMeasure α) {s : ι → Set α} (l : Filter ι) [inst : l.NeBot],
Filter.Tendsto (fun k => ↑m ((⋃ n, s n) \ s k)) l (nhds 0) → ↑m (⋃ n, s n) = ⨆ n, ↑m (s n)
This theorem is a statement about a sequence of sets and a measure defined on those sets. Given a sequence of sets `s : ι → Set α`, and a measure `m : MeasureTheory.OuterMeasure α`, if the union of these sets, denoted as `S = ⋃ n, s n`, has the property that the measure of the difference between `S` and each `s n`, denoted as `m (S \ s n)`, tends to zero along some nontrivial filter `l : Filter ι` (usually the filter `atTop` when `ι = ℕ`), then the measure of `S` is equal to the supremum of the measures of each `s n`, denoted as `m S = ⨆ n, m (s n)`. This theorem provides a way to calculate the measure of the union of a sequence of sets based on the measures of the individual sets, under the specified condition.
More concisely: If a sequence of sets `s : ι → Set α` and a measure `m : MeasureTheory.OuterMeasure α` satisfy the condition that `m (S \ s n)` tends to zero along some nontrivial filter `l : Filter ι` as `n` approaches some limit, then `m S = ⨆ n, m (s n)`.
|
MeasureTheory.OuterMeasure.ext_nonempty
theorem MeasureTheory.OuterMeasure.ext_nonempty :
∀ {α : Type u_1} {μ₁ μ₂ : MeasureTheory.OuterMeasure α}, (∀ (s : Set α), s.Nonempty → ↑μ₁ s = ↑μ₂ s) → μ₁ = μ₂ := by
sorry
This theorem, `MeasureTheory.OuterMeasure.ext_nonempty`, states that for any given type `α`, and any two outer measures `μ₁` and `μ₂` on `α`, if for every nonempty set `s` of `α`, `μ₁` applied to `s` equals `μ₂` applied to `s`, then `μ₁` equals `μ₂`. In other words, two outer measures are considered equal if they agree on the measures of all nonempty sets. The measure of the empty set is ensured to be equal by using `MeasureTheory.OuterMeasure.empty'`.
More concisely: Two outer measures on a type agree if they give equal measures to all nonempty sets.
|
MeasureTheory.OuterMeasure.le_ofFunction
theorem MeasureTheory.OuterMeasure.le_ofFunction :
∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {μ : MeasureTheory.OuterMeasure α},
μ ≤ MeasureTheory.OuterMeasure.ofFunction m m_empty ↔ ∀ (s : Set α), ↑μ s ≤ m s
The theorem `MeasureTheory.OuterMeasure.le_ofFunction` states that for any type `α`, any function `m` that maps sets of `α` to extended nonnegative real numbers (with the condition that `m` of the empty set equals zero), and any outer measure `μ` on `α`, `μ` is less than or equal to the outer measure derived by the function `m` if and only if for all sets of `α`, the value of `μ` on that set is less than or equal to the value of `m` on that set. In other words, it gives a condition for one outer measure to be less than or equal to another.
More concisely: For any type α, outer measure μ, and function m mapping sets of α to extended nonnegative real numbers with m(∅) = 0, μ ≤ m if and only if μ(A) ≤ m(A) for all sets A of α.
|
MeasureTheory.OuterMeasure.biUnion_null_iff
theorem MeasureTheory.OuterMeasure.biUnion_null_iff :
∀ {α : Type u_1} {β : Type u_2} (m : MeasureTheory.OuterMeasure α) {s : Set β},
s.Countable → ∀ {t : β → Set α}, ↑m (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, ↑m (t i) = 0
The theorem `MeasureTheory.OuterMeasure.biUnion_null_iff` states that for any two types `α` and `β`, a given outer measure `m` on `α`, and a countable set `s` of objects of type `β`, the outer measure of the union of a family of sets `t i` (for each `i` in `s`) is zero if and only if the outer measure of each individual set `t i` is zero. In simpler terms, it states that for a countable collection of sets, the total measure is zero if and only if each individual set has measure zero.
More concisely: For any outer measure `m` and a countable family of sets `(t\_i : β → Set α)_i`, the outer measure of their union is zero if and only if the outer measure of each `t\_i` is zero.
|
MeasureTheory.OuterMeasure.mono'
theorem MeasureTheory.OuterMeasure.mono' :
∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s₁ s₂ : Set α}, s₁ ⊆ s₂ → ↑m s₁ ≤ ↑m s₂
The theorem `MeasureTheory.OuterMeasure.mono'` states that for any type `α`, given an outer measure `m` on `α` and two sets `s₁` and `s₂` of `α`, if `s₁` is a subset of `s₂` (`s₁ ⊆ s₂`), then the outer measure of `s₁` is less than or equal to the outer measure of `s₂`. In other words, the outer measure of a set does not increase if the set is enlarged.
More concisely: For any outer measure `m` and sets `s₁ ⊆ s₂`, we have `m(s₁) ≤ m(s₂)`.
|
MeasureTheory.OuterMeasure.comap_iInf
theorem MeasureTheory.OuterMeasure.comap_iInf :
∀ {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α → β) (m : ι → MeasureTheory.OuterMeasure β),
(MeasureTheory.OuterMeasure.comap f) (⨅ i, m i) = ⨅ i, (MeasureTheory.OuterMeasure.comap f) (m i)
The theorem `MeasureTheory.OuterMeasure.comap_iInf` states that for any function `f` mapping from a type `α` to a type `β`, and a sequence `m` of outer measures on `β` indexed by `ι`, the pullback of the infimum (greatest lower bound) of `m` through `f` is the same as the infimum of the pullbacks of the individual measures in `m` through `f`. In other words, pulling back 'commutes' with taking the infimum of a sequence of outer measures.
More concisely: Given a function `f: α → β` and a sequence `(m_i : MeasurableSpace β)_(i: ι)` of outer measures on `β`, we have `∫(f ∫(x: α) f(x) ∥d(m_i)_x∥) = ∫(x: α) ∥f(x)∥d(∫(i: ι) m_i)`.
|
MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top
theorem MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top :
∀ {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α},
(∀ (n : ℕ), s n ⊆ s (n + 1)) → ∑' (k : ℕ), ↑m (s (k + 1) \ s k) ≠ ⊤ → ↑m (⋃ n, s n) = ⨆ n, ↑m (s n)
The theorem, `MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top`, states that given a sequence `s` of sets indexed by natural numbers, where each set in the sequence is a subset of the following set (i.e., the sequence is monotone), and the sum of the measures of differences between consecutive sets in the sequence is not infinite, then the measure of the union of all the sets in the sequence is equal to the supremum of the measures of the sets in the sequence. Here, the measure is taken with respect to some outer measure `m`.
More concisely: If `(s_n)` is a monotonic sequence of sets with finite sum of measure differences `(m(s_{n+1}) - m(s_n))` with respect to some outer measure `m`, then `m(⋃n finset.index s_n) = sup {m(s_n) | n ∈ ℕ}`.
|
MeasureTheory.OuterMeasure.iSup_apply
theorem MeasureTheory.OuterMeasure.iSup_apply :
∀ {α : Type u_1} {ι : Sort u_5} (f : ι → MeasureTheory.OuterMeasure α) (s : Set α), ↑(⨆ i, f i) s = ⨆ i, ↑(f i) s
The theorem `MeasureTheory.OuterMeasure.iSup_apply` states that for any type `α`, any type `ι`, any function `f` that maps from `ι` to the outer measure of `α`, and any set `s` of type `α`, the outer measure of the supremum (greatest lower bound) of `f` applied to `s` is equal to the supremum of the outer measure of `f` applied to `s`. In simpler terms, it asserts that the outer measure operation can be interchanged with the taking of supremum in a function over a set.
More concisely: For any type `α`, any type `ι`, and any function `f : ι → ℝ` mapping from `ι` to the outer measure of `α`, the outer measure of the supremum of `f` over a set `s` in `α` equals the supremum of the outer measures of `f` over `s`.
|
MeasureTheory.OuterMeasure.boundedBy_le
theorem MeasureTheory.OuterMeasure.boundedBy_le :
∀ {α : Type u_1} {m : Set α → ENNReal} (s : Set α), ↑(MeasureTheory.OuterMeasure.boundedBy m) s ≤ m s
This theorem states that for all types `α` and for all functions `m` which assign measures in the extended nonnegative real numbers to sets of type `α`, the measure of any set `s` of type `α` under the unique maximal outer measure `μ` (which is derived from `m` by `MeasureTheory.OuterMeasure.boundedBy`) is less than or equal to the measure of `s` under `m`. In other words, the measure of a set under the maximal outer measure never exceeds its measure under the original measure function.
More concisely: For all types `α` and measures `m`, the outer measure `μ` derived from `m` satisfies `μ(s) ≤ m(s)` for all sets `s` of type `α`.
|
MeasureTheory.OuterMeasure.restrict_trim
theorem MeasureTheory.OuterMeasure.restrict_trim :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.OuterMeasure α} {s : Set α},
MeasurableSet s →
((MeasureTheory.OuterMeasure.restrict s) μ).trim = (MeasureTheory.OuterMeasure.restrict s) μ.trim
The theorem `MeasureTheory.OuterMeasure.restrict_trim` states that for any type `α` that has a `MeasurableSpace` structure, any `OuterMeasure` `μ` on `α`, and any measurable set `s` of `α`, the trimmed version of the restricted outer measure of `μ` to `s` is equal to the restriction to `s` of the trimmed outer measure of `μ`. In simpler terms, it shows that restricting a trimmed outer measure still yields a trimmed outer measure.
More concisely: For any measurable space `(α, Σ)`, measurable set `s ∈ Σ`, and OuterMeasure `μ` on `α`, the trimmed outer measure of `μ` restricted to `s` equals the trimmed outer measure of `μ` trimmed to `s`.
|
MeasureTheory.OuterMeasure.iInf_apply'
theorem MeasureTheory.OuterMeasure.iInf_apply' :
∀ {α : Type u_1} {ι : Sort u_2} (m : ι → MeasureTheory.OuterMeasure α) {s : Set α},
s.Nonempty → ↑(⨅ i, m i) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i, ↑(m i) (t n)
This theorem states that for any type `α` and a family of outer measures `m` indexed by type `ι`, and a nonempty set `s` of type `α`, the infimum value of the outer measures on set `s` is not simply the minimum measure on that set. Instead, it equals the infimum of the sum of measures of a countable set of sets that cover set `s`. Notably, a different outer measure from the family can be used for each set in the covering. The covering set `t` is such that set `s` is a subset of the indexed union of the set `t`. For each natural number `n`, the sum is taken over the infimum of the outer measures on the `n`-th set in `t`.
More concisely: The infimum of a family of outer measures on a set is equal to the infimum of the sums of outer measures of countably many sets covering the set, where each set in the covering may be assigned a different outer measure.
|
MeasureTheory.OuterMeasure.null_of_locally_null
theorem MeasureTheory.OuterMeasure.null_of_locally_null :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : SecondCountableTopology α] (m : MeasureTheory.OuterMeasure α)
(s : Set α), (∀ x ∈ s, ∃ u ∈ nhdsWithin x s, ↑m u = 0) → ↑m s = 0
This theorem states that if for every point in a set, there exists a "neighborhood within" the set around that point that has zero measure under some outer measure, then the entire set also has zero measure under the same outer measure. The underlying space is assumed to be a topological space that is also second-countable, which means the space has a countable basis for its topology.
More concisely: If every point in a second-countable topological space has a neighborhood with zero outer measure, then the entire space has zero outer measure.
|
MeasureTheory.OuterMeasure.trim_op
theorem MeasureTheory.OuterMeasure.trim_op :
∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ : MeasureTheory.OuterMeasure α} {op : ENNReal → ENNReal},
(∀ (s : Set α), ↑m₁ s = op (↑m₂ s)) → ∀ (s : Set α), ↑m₁.trim s = op (↑m₂.trim s)
The theorem `MeasureTheory.OuterMeasure.trim_op` states that for any type `α` equipped with a `MeasurableSpace` structure, and any two outer measures `m₁` and `m₂` on `α`, along with an operation `op` on the extended nonnegative real numbers (`ENNReal`), if it holds that the application of `op` to the measure `m₂` of any set `s` equals the measure `m₁` of the same set, then the same property holds when `m₁` and `m₂` are replaced by their `trim` versions. In other words, if the measure of a set under `m₁` is the result of applying `op` to the measure of the set under `m₂` for all sets, then the same is true when we consider the trimmed versions of these measures.
More concisely: If outer measures $m\_1$ and $m\_2$ on a measurable space satisfy $m\_2(s) = \operatorname{op}(m\_1(s))$ for all sets $s$, then their trimmed versions also satisfy $m\_2' (s) = \operatorname{op}(m\_1'(s))$.
|
MeasureTheory.OuterMeasure.sInf_apply
theorem MeasureTheory.OuterMeasure.sInf_apply :
∀ {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α},
m.Nonempty → ↑(sInf m) s = ⨅ t, ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, ↑μ (t n)
This theorem, `MeasureTheory.OuterMeasure.sInf_apply`, is about the concept of infimum of a nonempty set of outer measures in measure theory. Specifically, the theorem states that for any type `α`, any set of outer measures `m` of type `α`, and any set `s` also of type `α`, if the set `m` of outer measures is not empty, then the infimum of this set of outer measures evaluated at `s` is equal to the infimum over all possible collections `t` of sets, where each `t` covers `s`, of the sum of infimum over all outer measures in `m` applied to each set in `t`.
This theorem establishes the intricate relationship between the infimum of a set of outer measures and the infimum of sums of measures over a countable set of sets that cover the given set, demonstrating that the value of the infimum of a nonempty set of outer measures on a set is not simply the minimum value of a measure on that set. Instead, it depends on the structure of countable set of sets that covers the given set. A different measure from the set of outer measures can be applied to each set in the countable cover.
More concisely: For any nonempty set of outer measures on a type `α` and any set `s` of type `α`, the infimum of the outer measures on `s` equals the infimum of the sums of infima of outer measures over countable covers of `s`.
|
MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim
theorem MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim :
∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α),
∃ t, s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ↑m.trim s
This theorem states that for any type `α` equipped with a structure `MeasurableSpace α`, for any outer measure `m` on `α`, and for any set `s` of type `α`, there exists a measurable superset `t` of `s` such that the measure of `t` with respect to the outer measure `m` is equal to the measure of `s` with respect to the trimmed outer measure of `m`. In other words, it's possible to find a measurable superset of any given set that retains the same measure as the original set when we consider the trimmed version of the outer measure.
More concisely: For any measurable space `(α, Σ, m)`, given a set `s ∈ Σ`, there exists a measurable set `t ⊇ s` with `m(t) = m^{*}(s)`, where `m^{*}` denotes the trimmed outer measure of `m`.
|
MeasureTheory.OuterMeasure.trim_add
theorem MeasureTheory.OuterMeasure.trim_add :
∀ {α : Type u_1} [inst : MeasurableSpace α] (m₁ m₂ : MeasureTheory.OuterMeasure α),
(m₁ + m₂).trim = m₁.trim + m₂.trim
This theorem states that the `trim` operation of outer measures in Measure Theory is additive. More specifically, for any given type `α` along with an instance of `MeasurableSpace α` and two outer measures `m₁` and `m₂` of this type, the `trim` of the sum of `m₁` and `m₂` is equal to the sum of their individual `trims`. Hence, the `trim` operation preserves the addition of outer measures.
More concisely: For any measurable spaces `(α, Σ, m₁)` and `(α, Σ, m₂)`, and their respective trimmed outer measures `m₁'` and `m₂'`, we have `m₁' + m₂' = (m₁ + m₂)'`, where `+` denotes the sum of outer measures.
|
MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter
theorem MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter :
∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {s t : Set α},
(∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤) →
↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) (s ∪ t) =
↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s + ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) t
This theorem states that, for any type `α`, given a measure function `m` from sets of `α` to the extended nonnegative reals (which assigns a measure of 0 to the empty set), and any two sets `s` and `t` of `α`, if every set `u` with non-empty intersections with both `s` and `t` is assigned an `∞` measure by `m`, then the measure of the union of `s` and `t` computed by the maximal outer measure `μ` derived from `m` is equal to the sum of the measures of `s` and `t`.
For instance, if `α` is an (e)metric space and `m` assigns `∞` to any set with diameter `≥ r`, then this theorem indicates that the measure of the union of any two sets `s` and `t` such that the (extended) distance between every point in `s` and every point in `t` is `≥ r` is equal to the sum of their individual measures.
More concisely: If measure function `m` assigns `∞` to every non-empty set intersecting both `s` and `t` in type `α`, then `μ(s ∪ t) = μ(s) + μ(t)`.
|
MeasureTheory.OuterMeasure.trim_iSup
theorem MeasureTheory.OuterMeasure.trim_iSup :
∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Sort u_2} [inst_1 : Countable ι]
(μ : ι → MeasureTheory.OuterMeasure α), (⨆ i, μ i).trim = ⨆ i, (μ i).trim
The theorem `MeasureTheory.OuterMeasure.trim_iSup` states that for any countable family of outer measures (denoted by `μ`), the supremum (`⨆`) of the trimmed outer measures is equal to the trimmed supremum of the outer measures. This is valid for any type `α` that forms a measurable space.
More concisely: For any countable family of outer measures `μ` on a measurable space `α`, the supremum of the trimmed outer measures is equal to the trimmed supremum of `μ`.
|
MeasureTheory.OuterMeasure.trim_eq_iInf
theorem MeasureTheory.OuterMeasure.trim_eq_iInf :
∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α),
↑m.trim s = ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), ↑m t
This theorem, `MeasureTheory.OuterMeasure.trim_eq_iInf`, states that for any type `α` with an associated measurable space, any outer measure `m` on `α`, and any set `s` of type `α`, the value of the trimmed outer measure of `m` on `s` is equal to the infimum of the outer measure `m` on set `t`, where `t` is any set that contains `s` and is a measurable set. In mathematical terms, if `s` is a subset of `t` and `t` is a measurable set, then the value of the trimmed `m` on `s` is the same as the infimum of the values of `m` on `t`.
More concisely: For any measurable space, outer measure, and measurable set, the trimmed outer measure of a subset is equal to the infimum of the outer measure on any superset containing it.
|
MeasureTheory.OuterMeasure.map_apply
theorem MeasureTheory.OuterMeasure.map_apply :
∀ {α : Type u_1} {β : Type u_5} (f : α → β) (m : MeasureTheory.OuterMeasure α) (s : Set β),
↑((MeasureTheory.OuterMeasure.map f) m) s = ↑m (f ⁻¹' s)
This theorem states that for any types `α` and `β`, a function `f` from `α` to `β`, an outer measure `m` on `α`, and a set `s` of `β`, the application of the mapped outer measure of `m` along `f` on the set `s` is equal to the application of `m` on the preimage of `s` under `f`. In mathematical terms, if `f` is a function mapping from `α` to `β`, `m` is an outer measure on `α`, and `s` is a set in `β`, then applying the outer measure induced by `f` on `m` to `s` is the same as applying `m` to the preimage of `s` under `f`.
More concisely: For any function \(f: \alpha \to \beta\), outer measure \(m\) on \(\alpha\), and set \(s \subseteq \beta\), \(m^{\mathcal{L}}(f^{-1}(s)) = \mathcal{L}(m)(f)(s)\). Here, \(m^{\mathcal{L}}\) denotes the outer measure induced by \(f\) and \(\mathcal{L}(m)\) denotes the original outer measure on \(\alpha\).
|
MeasureTheory.extend_empty
theorem MeasureTheory.extend_empty :
∀ {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅),
m ∅ P0 = 0 → MeasureTheory.extend m ∅ = 0
This theorem, `MeasureTheory.extend_empty`, states that for any type `α`, any property `P` of sets of `α`, and any function `m` from sets of `α` satisfying `P` to the extended nonnegative real numbers `ENNReal`, if the empty set satisfies property `P` and `m` maps the empty set to zero, then the extension of `m` using `MeasureTheory.extend` also maps the empty set to zero. Essentially, it guarantees that the extended function will preserve the zero measure of the empty set, which is a basic requirement in a measure theory context.
More concisely: If `m` is a measure function on sets of type `α` satisfying `P`, mapping the empty set to zero, then the extended measure `MeasureTheory.extend m` also maps the empty set to zero.
|
MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter
theorem MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter :
∀ {α : Type u_1} {m : Set α → ENNReal} {s t : Set α},
(∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤) →
↑(MeasureTheory.OuterMeasure.boundedBy m) (s ∪ t) =
↑(MeasureTheory.OuterMeasure.boundedBy m) s + ↑(MeasureTheory.OuterMeasure.boundedBy m) t
This theorem states that for any type `α`, any function `m` that assigns measures to sets, and any sets `s` and `t`, if the measure of any set `u` that has nonempty intersection with both `s` and `t` is infinity, then the measure of the union of `s` and `t` (denoted `μ (s ∪ t)`, where `μ` is the maximal outer measure satisfying `μ w ≤ m w` for all `w : Set α`) is equal to the sum of the measures of `s` and `t`.
An example would be, if `α` represents an extended metric space with the given measure function `m u` equating to infinity for any set of diameter `≥ r`, this theorem implies that for any two sets where the extended distance between any pair of points (`x ∈ s` and `y ∈ t`) is `≥ r`, the measure of the union of the two sets equals the sum of their individual measures.
More concisely: If `μ` is a measure satisfying `μ w ≤ m w` for all sets `w`, and for any set `u` intersecting both `s` and `t` has infinite measure, then `μ (s ∪ t) = μ (s) + μ (t)`.
|
MeasureTheory.OuterMeasure.exists_mem_forall_mem_nhds_within_pos
theorem MeasureTheory.OuterMeasure.exists_mem_forall_mem_nhds_within_pos :
∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : SecondCountableTopology α] (m : MeasureTheory.OuterMeasure α)
{s : Set α}, ↑m s ≠ 0 → ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, 0 < ↑m t
The theorem `MeasureTheory.OuterMeasure.exists_mem_forall_mem_nhds_within_pos` states that for any given type `α` with a topological space and second countable topology, with a measure `m` and set `s`, if the measure of the set `s` is not zero, then there exists a point `x` in the set `s` such that for any subset `t` in the neighborhood within `s` and `x`, the measure of `t` is positive. The neighborhood within `s` and `x`, denoted `𝓝[s] x`, consists of sets containing the intersection of `s` and a neighborhood of `x`.
More concisely: Given a second countable topological space `(α, top)` with a non-zero measure `m`, there exists a point `x` in a measurable set `s` such that for every neighborhood `t` of `x` in `s`, the measure of `t` is positive.
|