MeasureTheory.sub_ae_eq_zero
theorem MeasureTheory.sub_ae_eq_zero :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7} [inst : AddGroup β]
(f g : α → β), μ.ae.EventuallyEq (f - g) 0 ↔ μ.ae.EventuallyEq f g
The theorem `MeasureTheory.sub_ae_eq_zero` states that for any measurable space `α`, measure `μ` on `α`, and functions `f` and `g` from `α` to some additive group `β`, the statement "the difference between `f` and `g` equals zero almost everywhere with respect to the measure `μ`" is equivalent to saying that "`f` and `g` are equal almost everywhere with respect to the measure `μ`". Here, "almost everywhere" refers to the set of points in the space `α` outside of a subset of measure zero.
More concisely: For any measurable spaces `(α, Σ)`, measures `μ`, and functions `f, g : α → add-monoid β`, the sets `{x ∈ α : f x ≠ g x}` and `{x ∈ α : f x ─ g x ≠ 0}` have zero measure with respect to `μ`. Thus, `f` and `g` are equal almost everywhere if and only if their difference is zero almost everywhere.
|
MeasureTheory.Measure.restrict_mono_ae
theorem MeasureTheory.Measure.restrict_mono_ae :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyLE s t → μ.restrict s ≤ μ.restrict t
This theorem states that for any type `α`, given a measurable space `m0` over the type `α`, a measure `μ` on the measurable space, and any two sets `s` and `t` of type `α`, if the set `s` is almost everywhere less than or equal to the set `t` with respect to the measure `μ` (i.e., `s` is a subset of `t` except possibly on a set of measure zero), then the restriction of the measure `μ` to the set `s` is less than or equal to the restriction of the measure `μ` to the set `t`. In other words, the measure of the set `s` under its almost everywhere condition is less than or equal to the measure of the set `t`.
More concisely: For any measurable spaces `(α, m0)` and measures `μ`, if `s ⊆ t` almost everywhere and `μ(t) < ∞`, then `μ(s) ≤ μ(t)`.
|
MeasureTheory.ae_restrict_iff'
theorem MeasureTheory.ae_restrict_iff' :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
MeasurableSet s → ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
The theorem `MeasureTheory.ae_restrict_iff'` states that for any type `α`, a measurable space `m0` over `α`, a measure `μ` on that space, a set `s` of elements of type `α`, and a predicate `p` over `α`, if the set `s` is measurable, then the property `p` holds almost everywhere with respect to the measure `μ` restricted to `s` if and only if `p` holds almost everywhere with respect to the measure `μ` for all elements in the set `s`. Here, "almost everywhere" means for all elements except for a set of measure zero.
More concisely: For any measurable space `(α, m0)`, measure `μ` on `m0`, set `s ⊆ α` with measurable boundary, and predicate `p` over `α`, if `μ(s^c) = 0` and `p` is measurable, then `p` almost everywhere holds on `s` if and only if `p` almost everywhere holds on `α`.
|
MeasureTheory.Measure.restrict_mono
theorem MeasureTheory.Measure.restrict_mono :
∀ {α : Type u_2} {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄,
s ⊆ s' → ∀ ⦃μ ν : MeasureTheory.Measure α⦄, μ ≤ ν → μ.restrict s ≤ ν.restrict s'
The theorem `MeasureTheory.Measure.restrict_mono` states that for any type `α` equipped with a `MeasurableSpace` structure, if we have two sets `s` and `s'` of this type such that `s` is a subset of `s'`, and two measures `μ` and `ν` such that `μ` is less than or equal to `ν`, then the restriction of the measure `μ` to the set `s` is less than or equal to the restriction of the measure `ν` to the set `s'`. This shows that restricting a measure to a subset is a monotone operation in both the set and the measure.
More concisely: If `α` is a MeasurableSpace, `s ⊆ s'`, `μ ≤ ν` are measures on `α`, then `μ!s ≤ ν!s'`.
|
MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict
theorem MeasureTheory.ae_restrict_of_ae_eq_of_ae_restrict :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : α → Prop},
μ.ae.EventuallyEq s t → ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ.restrict t, p x
This theorem states that for any two measurable sets "s" and "t" in a given measure space, if these sets are almost everywhere equal (ae_eq), then any proposition that is almost everywhere true on one set is also almost everywhere true on the other set. In other words, if a proposition holds for almost all elements in one measurable set, and the two sets are almost everywhere equal, then the proposition holds for almost all elements in the other set too.
More concisely: If measurable sets $s$ and $t$ are almost everywhere equal (aeq), then any proposition almost everywhere true on $s$ is also almost everywhere true on $t$.
|
MeasureTheory.ae_restrict_mem
theorem MeasureTheory.ae_restrict_mem :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → ∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
The theorem `MeasureTheory.ae_restrict_mem` states that for any type `α`, equipped with a measurable space structure `m0` and a measure `μ`, if `s` is a set of elements of type `α` and is measurable, then almost every element `x` of type `α` with respect to the restriction of `μ` to `s`, belongs to `s`. In layman's terms, if we restrict our attention to the set `s`, almost all of the points we "randomly" encounter will actually belong to `s`.
More concisely: For any measurable set `s` and measure `μ` on type `α`, almost every element `x` in `α` with respect to the restriction of `μ` to `s` lies in `s`.
|
MeasureTheory.ae_eq_comp
theorem MeasureTheory.ae_eq_comp :
∀ {α : Type u_2} {β : Type u_3} {δ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
{μ : MeasureTheory.Measure α} {f : α → β} {g g' : β → δ},
AEMeasurable f μ → (MeasureTheory.Measure.map f μ).ae.EventuallyEq g g' → μ.ae.EventuallyEq (g ∘ f) (g' ∘ f)
This theorem, `MeasureTheory.ae_eq_comp`, asserts that for any types `α`, `β`, and `δ`, a measurable space `α` denoted as `m0`, another measurable space `β`, a measure `μ` on `α`, a function `f` mapping from `α` to `β`, and two functions `g` and `g'` both mapping from `β` to `δ`, if `f` is almost everywhere measurable with respect to `μ`, and `g` is almost everywhere equal to `g'` with respect to the measure resulting from mapping `f` to `μ`, then the composition of `g` and `f` is almost everywhere equal to the composition of `g'` and `f` with respect to measure `μ`.
In essence, if the function `f` is almost everywhere measurable and two functions `g` and `g'` are almost everywhere equivalent under the measure transformed by `f`, then the compositions `g ∘ f` and `g' ∘ f` are also almost everywhere equivalent under the original measure.
More concisely: If `f` is almost everywhere measurable with respect to `μ` on `α` and `g` is almost everywhere equal to `g'` with respect to the pushforward measure of `μ` by `f` on `β`, then `g ∘ f` is almost everywhere equal to `g' ∘ f` with respect to `μ` on `α`.
|
MeasureTheory.Measure.restrict_apply₀
theorem MeasureTheory.Measure.restrict_apply₀ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.NullMeasurableSet t (μ.restrict s) → ↑↑(μ.restrict s) t = ↑↑μ (t ∩ s)
The `MeasureTheory.Measure.restrict_apply₀` theorem states: For any type `α`, given a measurable space `m0` on `α`, a measure `μ` on `α`, and two sets `s` and `t` of `α`, if `t` is a null measurable set under the restriction of `μ` to `s`, then the measure of `t` under the restriction of `μ` to `s` is equal to the measure of the intersection of `t` and `s` under `μ`. In other words, when `t` is null measurable, restricting the measure to a set `s` doesn't change the measure of the intersection of `t` and `s`.
More concisely: If `μ` is a measure on a measurable space `(α, m0)`, `s ⊆ α`, `t` is null measurable in `s` under `μ`, then `μ(t ∩ s) = μ(t)|s`.
|
MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset
theorem MeasureTheory.Measure.ext_of_generateFrom_of_cover_subset :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S T : Set (Set α)},
m0 = MeasurableSpace.generateFrom S →
IsPiSystem S →
T ⊆ S → T.Countable → T.sUnion = Set.univ → (∀ s ∈ T, ↑↑μ s ≠ ⊤) → (∀ s ∈ S, ↑↑μ s = ↑↑ν s) → μ = ν
This theorem states that two measures, μ and ν, are equal if they satisfy two conditions: first, they are equal on the π-system that generates the σ-algebra, and second, they are both finite on an increasing sequence of sets within the π-system that spans the entire space. The π-system here is denoted by 'S' and the spanning sequence of sets is denoted by 'T'. This theorem is described in the context of a measurable space 'm0' that is generated from the π-system 'S'. The theorem also assumes that 'T' is a subset of 'S', 'T' is countable, and the union of all sets in 'T' equals the universal set.
More concisely: If two measures μ and ν on a measurable space (m0, S) generated by a π-system S satisfy μ(A) = ν(A) for all A in the countable subset T of S that spans the universal set and have finite values on T, then μ = ν.
|
MeasureTheory.Measure.restrict_eq_zero
theorem MeasureTheory.Measure.restrict_eq_zero :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ.restrict s = 0 ↔ ↑↑μ s = 0
This theorem is about the restriction of a measure in measure theory. For any given type `α`, and given `m0` which is a measurable space over `α`, and `μ` which is a measure over `α`, and `s` which is a set of `α`, the theorem states that the restriction of measure `μ` to set `s` equals zero if and only if the measure of set `s` with respect to measure `μ` equals zero. This theorem connects the concepts of restriction of a measure and the measure of a set in measure theory, and provides a condition under which these two quantities are equal to zero.
More concisely: For any measurable space `(α, m0)` and measure `μ` over `α`, the restriction of `μ` to a set `s` equals zero if and only if the measure of `s` with respect to `μ` is zero.
|
MeasureTheory.Measure.restrict_biUnion_congr
theorem MeasureTheory.Measure.restrict_biUnion_congr :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set ι}
{t : ι → Set α},
s.Countable →
(μ.restrict (⋃ i ∈ s, t i) = ν.restrict (⋃ i ∈ s, t i) ↔ ∀ i ∈ s, μ.restrict (t i) = ν.restrict (t i))
This theorem, `MeasureTheory.Measure.restrict_biUnion_congr`, states that for any given type `α` and `ι`, a measurable space `m0` of type `α`, two measures `μ` and `ν` on this measurable space, a countable set `s` of type `ι`, and a function `t` from `ι` to a set of type `α`, the restriction of measures `μ` and `ν` to the union of sets `t i` for each `i` in set `s` are equal if and only if the restriction of measures `μ` and `ν` to each set `t i` for all `i` in set `s` are equal.
In other words, it says that the equality of measure restriction over the union of a countable collection of sets is equivalent to the pointwise equality of measure restriction over each set in that collection.
More concisely: For any measurable spaces `(α, ι, m0)`, measures `μ` and `ν` on `m0`, a countable set `s ι`, and a function `t : ι → α`, the measures `μ` and `ν` restricted to the union of sets `{t i | i ∈ s}` are equal if and only if they are equal on each set `{t i}` for all `i ∈ s`.
|
MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ
theorem MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : Countable ι]
{s : ι → Set α}, ⋃ i, s i = Set.univ → (μ = ν ↔ ∀ (i : ι), μ.restrict (s i) = ν.restrict (s i))
This theorem states that for any type `α` and a countable index type `ι`, given a measurable space on `α` and two measures (`μ` and `ν`) on this space, if we have a collection of sets `s` indexed by `ι` such that the union of all these sets is the universal set on `α` (i.e., it covers the entire space), then the two measures `μ` and `ν` are equal if and only if their restrictions to each individual set `s i` in the collection are equal. This is a way to compare two measures by looking at their behavior on a collection of sets covering the entire space.
More concisely: For any measurable spaces on type `α` with countable index type `ι`, measures `μ` and `ν` are equal if and only if their restrictions to each `s i` in the collection of sets covering `α` are equal.
|
MeasureTheory.Measure.restrict_toMeasurable
theorem MeasureTheory.Measure.restrict_toMeasurable :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
↑↑μ s ≠ ⊤ → μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
This theorem states that for any type `α`, any measurable space `m0` of type `α`, any measure `μ` of that measurable space, and any set `s` of type `α`, if `μ s` is not equal to infinity, then the restriction of `μ` to the measurable set derived from `s` is equal to the restriction of `μ` to `s` itself. In other words, if a set does not have infinite measure, the measure restricted to it remains the same even if we replace the set with the corresponding measurable set.
More concisely: For any measurable space `(α, m0)`, measure `μ`, and set `s` of finite measure `μ(s)`, the restriction of `μ` to the measurable set `{x : α | x ∈ s}∘m0` is equal to `μ` restricted to `s`.
|
MeasureTheory.Measure.restrict_inter_add_diff₀
theorem MeasureTheory.Measure.restrict_inter_add_diff₀ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
MeasureTheory.NullMeasurableSet t μ → μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
This theorem states that for any given type `α` with a corresponding `MeasurableSpace` and a measure `μ`, and any two sets `s` and `t` of type `α` where `t` is a `NullMeasurableSet`, the measure of the intersection of `s` and `t` added to the measure of the difference of `s` and `t` is equal to the measure of `s` itself. In mathematical terms, if `μ` is a measure and `s` and `t` are sets with `t` being null measurable, then `μ(s ∩ t) + μ(s \ t) = μ(s)`.
More concisely: For any measure `μ` and null measurable sets `s` and `t` in a measurable space, `μ(s ∩ t) + μ(s \ t) = μ(s)`.
|
MeasureTheory.Measure.restrict_iUnion_ae
theorem MeasureTheory.Measure.restrict_iUnion_ae :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι]
{s : ι → Set α},
Pairwise (MeasureTheory.AEDisjoint μ on s) →
(∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
μ.restrict (⋃ i, s i) = MeasureTheory.Measure.sum fun i => μ.restrict (s i)
The theorem `MeasureTheory.Measure.restrict_iUnion_ae` states that for any type `α`, any countable index set `ι`, any measurable space `m0`, any measure `μ`, and any indexed family of sets `s`, if each pair of sets from `s` is almost everywhere disjoint with respect to measure `μ`, and each set in `s` is a null measurable set with respect to measure `μ`, then the measure `μ` restricted to the union of all sets in `s` is equal to the sum of the measures `μ` restricted to each individual set in `s`. In simpler terms, if we have a family of sets that don't overlap almost everywhere and each set can be approximated by a measurable set up to a set of null measure, then the total measure over the union of these sets is the sum of the measures over each individual set.
More concisely: If `(ι : Type)` is countable, `(m0 : MeasurableSpace α)`, `(μ : Measure m0)`, and `(s : ι → Set α)` are such that each pair of sets in `s` is almost everywhere disjoint and each set in `s` is null measurable, then `μ.restrict (⋃ i in ι, s i) = Σ i in ι, μ.restrict (s i)`.
|
MeasureTheory.ae_restrict_biUnion_eq
theorem MeasureTheory.ae_restrict_biUnion_eq :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : ι → Set α) {t : Set ι},
t.Countable → (μ.restrict (⋃ i ∈ t, s i)).ae = ⨆ i ∈ t, (μ.restrict (s i)).ae
This theorem, `MeasureTheory.ae_restrict_biUnion_eq`, states that for any type `α`, any index type `ι`, any measurable space `m0` over `α`, any measure `μ` on `α`, and any function `s` from `ι` to sets of `α`, if we have a countable set `t` of `ι`, then the almost everywhere filter of the measure restricted to the union of sets `s i` for `i` in `t` is equal to the supremum of the almost everywhere filters of the measures restricted to each `s i` for `i` in `t`.
In other words, considering "almost everywhere" in the context of a measure restricted to a countable union of sets is the same as considering it separately for each set in the union and then taking the supremum of the results.
More concisely: For any measurable space `(α, Σ, m)`, measure `μ`, countable index set `ι`, and function `s : ι → Σ`, the almost everywhere filter of `μ` restricted to the countable union of `s i` equals the supremum of the almost everywhere filters of `μ` restricted to each `s i`.
|
MeasureTheory.Measure.restrict_mono'
theorem MeasureTheory.Measure.restrict_mono' :
∀ {α : Type u_2} {_m0 : MeasurableSpace α} ⦃s s' : Set α⦄ ⦃μ ν : MeasureTheory.Measure α⦄,
μ.ae.EventuallyLE s s' → μ ≤ ν → μ.restrict s ≤ ν.restrict s'
The theorem `MeasureTheory.Measure.restrict_mono'` asserts that the restriction of a measure to a subset is monotone in both the set and the measure. In particular, for any type `α` endowed with a `MeasurableSpace` structure, and for any two sets `s` and `s'` of type `α`, along with any two measures `μ` and `ν` on the `MeasurableSpace` of `α`; then if `s` is almost everywhere lesser than or equal to `s'` (under the measure `μ`), and if measure `μ` is lesser than or equal to measure `ν`, it follows that the restriction of measure `μ` to set `s` is lesser than or equal to the restriction of measure `ν` to set `s'`.
More concisely: If `μ` is a measure that is less than or equal to `ν` on a measurable space `(α, Σ)`, and `s` is a subset of `α` that is almost everywhere less than or equal to another subset `s'` with respect to `μ`, then `μ(s)` is less than or equal to `ν(s')`.
|
MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe
theorem MeasureTheory.Measure.MeasurableSet.nullMeasurableSet_subtype_coe :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {t : Set ↑s},
MeasureTheory.NullMeasurableSet s μ → MeasurableSet t → MeasureTheory.NullMeasurableSet (Subtype.val '' t) μ
This theorem states that, for every type `α` with a given `MeasurableSpace` structure `m0` and a measure `μ`, if we have a set `s` of type `α` and a set `t` of elements that are subtypes of `s`, and if `s` is a null measurable set with respect to `μ` and `t` is a measurable set, then the set of underlying elements of `t` (obtained using the `Subtype.val` function on each element of `t`) is also a null measurable set with respect to `μ`.
In other words, it asserts that measurability and null measurability properties are preserved when going from a set of subtypes to the corresponding set of underlying elements.
More concisely: If `s` is a null measurable set and `t` is a measurable subset of a measurable space `(α, m0)` with measure `μ`, then the set of underlying elements of `t` is a null measurable set.
|
MeasureTheory.Measure.restrict_empty
theorem MeasureTheory.Measure.restrict_empty :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.restrict ∅ = 0
This theorem states that for any type `α`, any measurable space `m0` over this type, and any measure `μ` over this measurable space, restricting the measure `μ` to the empty set results in a measure of zero. Written mathematically, if we have a measure μ on a measurable space, then μ restricted to the empty set is equal to zero.
More concisely: For any measure `μ` on a measurable space, `μ(∅) = 0`.
|
indicator_ae_eq_restrict
theorem indicator_ae_eq_restrict :
∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
[inst_1 : Zero β], MeasurableSet s → (μ.restrict s).ae.EventuallyEq (s.indicator f) f
The theorem `indicator_ae_eq_restrict` states that for any types `α` and `β`, any measurable space `α`, any measure `μ` on `α`, any set `s` of `α`, and any function `f` from `α` to `β`, given `β` has a zero, if `s` is a measurable set, then almost everywhere (with respect to the measure `μ` restricted to `s`) the indicator function of `s` with respect to `f` is equal to `f`. In other words, for almost all elements in the set `s`, applying the indicator function gives the same result as just applying the function `f`.
More concisely: For any measurable spaces `α` and `β`, measures `μ` on `α`, sets `s` of `α`, and functions `f: α → β` with `β` having a zero, if `s` is measurable, then almost everywhere on `s`, the indicator function of `s` and `f` agree: `1_[s] = f`.
|
MeasureTheory.ae_restrict_iUnion_eq
theorem MeasureTheory.ae_restrict_iUnion_eq :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι]
(s : ι → Set α), (μ.restrict (⋃ i, s i)).ae = ⨆ i, (μ.restrict (s i)).ae
The theorem `MeasureTheory.ae_restrict_iUnion_eq` states that for any type `α` and an index type `ι`, given a `MeasurableSpace` on `α`, a measure `μ` on that space and a countable index set of `ι`, if `s` is a mapping from `ι` to sets of `α`, the almost everywhere filter of the measure restricted to the union of the sets `s i` (denoted as `μ.restrict (⋃ i, s i)`) is equal to the supremum (or greatest lower bound) of the almost everywhere filters of the measures restricted to each individual set `s i`, symbolically represented as `⨆ i, MeasureTheory.Measure.ae (μ.restrict (s i))`. In other words, the almost everywhere behavior of the measure on the union of a collection of sets is described by the supremum of the almost everywhere behavior of the measure on each of the individual sets.
More concisely: The theorem `MeasureTheory.ae_restrict_iUnion_eq` asserts that the almost everywhere filter of a measure restricted to the union of a countable collection of sets is equal to the supremum (or greatest lower bound) of the almost everywhere filters of the measures restricted to each individual set.
|
map_comap_subtype_coe
theorem map_comap_subtype_coe :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {s : Set α},
MeasurableSet s →
∀ (μ : MeasureTheory.Measure α),
MeasureTheory.Measure.map Subtype.val (MeasureTheory.Measure.comap Subtype.val μ) = μ.restrict s
This theorem, `map_comap_subtype_coe`, states that for any type `α` with a given measurable space `m0`, and any set `s` of type `α` that is a measurable set, for any measure `μ` on `α`, the measure of the image of `s` under the function `Subtype.val` when the preimage of `μ` under `Subtype.val` is taken, is equal to the restriction of the measure `μ` to the set `s`. In mathematical terms, given a measurable space, a measurable set within that space, and a measure on that space, the measure of the image of the set under the map `Subtype.val` is the same as the measure of the set itself restricted to the set.
More concisely: Given a measurable space $(X, \Sigma,\mu)$, a measurable set $S \in \Sigma$, and the subtype $t : S \hookrightarrow X$, the measure $\mu(t(\cdot))$ is equal to the restriction of $\mu$ to $S$, denoted $\mu\vert_S$.
|
MeasureTheory.Measure.restrict_apply'
theorem MeasureTheory.Measure.restrict_apply' :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasurableSet s → ↑↑(μ.restrict s) t = ↑↑μ (t ∩ s)
This theorem states that, given two sets `s` and `t` of a certain type `α` (which exists in a measurable space equipped with a measure (`μ`)), if `s` is a measurable set, then the outer measure of `t` with respect to the restriction of the measure to `s` is equal to the outer measure of the intersection of `t` and `s` under the measure `μ`. This gives an alternative version of `Measure.restrict_apply`, where the measurability requirement is placed on `s` rather than `t`. In mathematical terms, it says that for a measurable set `s`, $\mu'(t) = \mu(t \cap s)$, where $\mu'$ is the measure restricted to `s`.
More concisely: For a measurable set `s` in a measurable space with measure `μ`, the outer measure of `t` under the restriction of `μ` to `s` equals the outer measure of `t ∩ s`.
|
MeasureTheory.Measure.restrict_restrict'
theorem MeasureTheory.Measure.restrict_restrict' :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasurableSet t → (μ.restrict t).restrict s = μ.restrict (s ∩ t)
This theorem states that for any type `α`, any measurable space `m0` over `α`, any measure `μ` on that measurable space, and any two sets `s` and `t` of the type `α`, if `t` is a measurable set, then the restriction of the restriction of the measure `μ` to the set `t` to the set `s` is equivalent to the restriction of the measure `μ` to the intersection of the sets `s` and `t`. In other words, restricting a measure twice in a row is the same as restricting it once to the intersection of the two sets.
More concisely: For any measurable space `(α, m0)`, measure `μ`, and sets `s` and `t` of type `α` with `t` measurable, the restriction of `μ` to `s` restricted to `t` equals the restriction of `μ` to `s ∩ t`.
|
Mathlib.MeasureTheory.Measure.Restrict._auxLemma.3
theorem Mathlib.MeasureTheory.Measure.Restrict._auxLemma.3 :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
(μ.restrict s = 0) = (↑↑μ s = 0)
This theorem pertains to the field of Measure Theory. For any type `α`, given a measurable space `m0` of this type, a measure `μ` on this measurable space, and a set `s` of the same type, the theorem states that the measure of the set `s` being restricted by `μ` equals zero if and only if the measure of the set `s` in `μ` is zero. In other words, the result of restricting the measure `μ` to the set `s` yields a zero measure if and only if the original measure of `s` under `μ` is zero.
More concisely: For any measurable space `(α, m0)` and measure `μ`, a set `s` has zero measure under `μ` if and only if the restricted measure `μ | s` is the zero measure.
|
MeasureTheory.ae_restrict_eq
theorem MeasureTheory.ae_restrict_eq :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → (μ.restrict s).ae = μ.ae ⊓ Filter.principal s
The theorem `MeasureTheory.ae_restrict_eq` states that for any type `α`, any measurable space `m0` on `α`, any measure `μ` on `α`, and any set `s` of `α`, if `s` is a measurable set, then the "almost everywhere" filter of the measure restricted to `s` is equal to the intersection of the "almost everywhere" filter of the measure `μ` and the principal filter of `s`. In simpler terms, this theorem tells us about the relationship between the "almost everywhere" concept when applied to a measure restricted to a measurable subset and the original measure.
More concisely: For any measurable space `(α, ℱ, μ)`, measurable set `s ∈ ℱ`, the almost everywhere filter of `μ` restricted to `s` equals the intersection of the almost everywhere filter of `μ` and the principal filter of `s`.
|
Mathlib.MeasureTheory.Measure.Restrict._auxLemma.11
theorem Mathlib.MeasureTheory.Measure.Restrict._auxLemma.11 :
∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {p : α → Prop},
(∀ᵐ (a : α) ∂μ, p a) = (↑↑μ {a | ¬p a} = 0)
This theorem states that for any type `α` that has a `MeasurableSpace` instance, a measure `μ` on that `α`, and a predicate `p` on `α`, the condition that `p` holds almost everywhere (i.e., for `μ`-almost every `a` in `α`) is equivalent to the measure of the set of all `a` in `α` for which `p` does not hold being zero.
More concisely: For any measurable space `(α, Σ, μ)`, predicate `p` on `α`, the condition that `p` holds almost everywhere (i.e., for `μ`-almost all `a` in `α`) is equivalent to the measure of the set of `a` in `α` where `p` does not hold being zero.
|
MeasureTheory.ae_imp_of_ae_restrict
theorem MeasureTheory.ae_imp_of_ae_restrict :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
(∀ᵐ (x : α) ∂μ.restrict s, p x) → ∀ᵐ (x : α) ∂μ, x ∈ s → p x
This theorem, `MeasureTheory.ae_imp_of_ae_restrict`, states that for any type `α`, any `MeasurableSpace` on `α`, any `MeasureTheory.Measure` on `α`, any set `s` of `α`, and any property `p` defined on `α`, if almost everywhere in the measure restricted to set `s`, the property `p` holds, then almost everywhere in the original measure, if an element `x` is in the set `s`, the property `p` holds for `x`. In other words, if a property is almost universally true on a measure-restricted set, then it will also be almost universally true on the whole set, provided the elements are in the restricted set.
More concisely: If a property holds almost everywhere in the measure restriction of a set, then it holds almost everywhere in the original measure for elements in that set.
|
MeasurableEmbedding.map_comap
theorem MeasurableEmbedding.map_comap :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
MeasurableEmbedding f →
∀ (μ : MeasureTheory.Measure β),
MeasureTheory.Measure.map f (MeasureTheory.Measure.comap f μ) = μ.restrict (Set.range f)
This theorem states that for any two types `α` and `β`, each with their associated measurable spaces `m0` and `m1`, and a function `f` from `α` to `β` that is a measurable embedding, then for any measure `μ` on `β`, the measure induced by first applying the function `f` and then measuring (i.e., the pushforward measure) equals the restriction of the original measure `μ` to the range of the function `f`. This demonstrates how measures are preserved under the action of a measurable embedding.
More concisely: If `f: α → β` is a measurable embedding between measurable spaces `(α, m0)` and `(β, m1)`, and `μ` is a measure on `β`, then `f_*\mu = μ ∘ Restriction f`, where `f_*\mu` is the pushforward measure and `Restriction f` is the restriction of `μ` to the range of `f`.
|
MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ
theorem MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set ι}
{s : ι → Set α}, S.Countable → ⋃ i ∈ S, s i = Set.univ → (μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i))
The theorem `MeasureTheory.Measure.ext_iff_of_biUnion_eq_univ` asserts that for any type `α` and an indexing type `ι`, given a measurable space `m0` on `α` and two measures `μ` and `ν` on this space, along with a countable set `S` of indices and a function `s` that maps each index to a set in `α`, if the union of all sets `s i` for `i` in `S` constitutes the universal set, then the two measures `μ` and `ν` are equal if and only if they have the same restrictions on each of the sets `s i` for `i` in `S`. In mathematical terms, if the sets `s i` form a spanning collection of sets for the whole space and `μ` and `ν` are identical on each of these sets, then the two measures are identical over the whole space.
More concisely: For measurable spaces `(α, m0)`, measures `μ` and `ν`, indexing type `ι`, countable set `S`, and function `s : ι → α`, if the union of sets `s i` for `i` in `S` equals the universal set and measures `μ` and `ν` agree on each `s i`, then `μ` and `ν` are equal.
|
MeasureTheory.Measure.restrict_union_congr
theorem MeasureTheory.Measure.restrict_union_congr :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s t : Set α},
μ.restrict (s ∪ t) = ν.restrict (s ∪ t) ↔ μ.restrict s = ν.restrict s ∧ μ.restrict t = ν.restrict t
The theorem `MeasureTheory.Measure.restrict_union_congr` states that, for any type `α` with a defined `MeasurableSpace`, and for any two measures `μ` and `ν` over this type, as well as any two sets `s` and `t` of this type, if the restrictions of the two measures on the union of `s` and `t` are identical, then the restrictions of the two measures on `s` and `t` individually are also identical, and vice versa. In other words, two measures agree on all measurable subsets of the union of two sets if and only if they agree on all measurable subsets of each of the two sets individually.
More concisely: If two measures agree on all measurable subsets of the union of two sets in a measurable space, then they agree on all measurable subsets of each set individually. (Conversely, if they agree on all measurable subsets of each set, they agree on all measurable subsets of their union.)
|
MeasureTheory.Measure.restrict_congr_set
theorem MeasureTheory.Measure.restrict_congr_set :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
μ.ae.EventuallyEq s t → μ.restrict s = μ.restrict t
This theorem states that for any type `α` with a given measurable space `m0` and a measure `μ`, if we have two sets `s` and `t` of type `α`, then if `s` is equal to `t` almost everywhere (denoted by `s =ᶠ[MeasureTheory.Measure.ae μ] t`), the restriction of measure `μ` to set `s` is equal to the restriction of measure `μ` to set `t`. In other words, the measure of `s` and `t` is the same when we only consider points that belong to almost every set in the measure space.
More concisely: For measurable sets `s` and `t` of type `α` in a measurable space with measure `μ`, if `s =ᶠ[μ] t`, then `μ s = mu t`.
|
MeasureTheory.Measure.restrict_le_self
theorem MeasureTheory.Measure.restrict_le_self :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ.restrict s ≤ μ
This theorem states that for any type `α`, any `MeasurableSpace` on `α`, any measure `μ` from the Measure Theory on `α`, and any set `s` of type `α`, the restriction of the measure `μ` to the set `s` is always less than or equal to the original measure `μ`. This is a fundamental property in measure theory expressing that the measure of a subset does not exceed the measure of the whole set.
More concisely: For any MeasurableSpace $(X, \Sigma)$, any measure $\mu : \Sigma \rightarrow \mathbb{R}_{\ge 0}$, and any $s \in \Sigma$, we have $\mu(s) \le \mu(\Omega)$, where $\Omega$ is the universal set of $X$.
|
MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict
theorem MeasureTheory.Measure.restrict_sInf_eq_sInf_restrict :
∀ {α : Type u_2} {t : Set α} {m0 : MeasurableSpace α} {m : Set (MeasureTheory.Measure α)},
m.Nonempty → MeasurableSet t → (sInf m).restrict t = sInf ((fun μ => μ.restrict t) '' m)
This theorem states that the infimum of a set of measures and the restriction of a measure to a subset of the space commute. More specifically, for any type `α`, a set `t` of that type, a measurable space `m0`, and a set `m` of measures on that space, given that the set of measures is not empty and the set `t` is a measurable set, the restriction of the infimum measure over the set `m` to the set `t` is equal to the infimum of the set of measures obtained by restricting each measure in `m` to the set `t`. In other words, applying the restriction operation either before or after taking the infimum yields the same result.
More concisely: For any measurable space `(α, ℳ)`, a non-empty set `t ∈ ℳ` of measurable subsets, and a family `{μ_i : ℙ(t) -> ℝ}| i ∈ I` of restrictions of measures on `α` to `t`, the infimum of `{μ_i}` equals the restriction of the infimum of the measures on `α` to `t`. In other words, ∫ₕ(t, μ) dμ = ∫ₕ(t, ∫ₕ(α, μ) dμ) dμ for all measures μ on `α`.
|
MeasureTheory.Measure.restrict_map
theorem MeasureTheory.Measure.restrict_map :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
{f : α → β},
Measurable f →
∀ {s : Set β},
MeasurableSet s →
(MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
The theorem `MeasureTheory.Measure.restrict_map` states that for any two types `α` and `β` with their respective measurable spaces `m0` and `inst`, along with a measure `μ` on `α` and a measurable function `f` from `α` to `β`, the restriction of the pushforward measure of `μ` under `f` to a measurable set `s` in `β` is the same as the pushforward of the restriction of `μ` to the preimage of `s` under `f`. In other words, it characterizes the interaction between the operations of measure pushforward and restriction in terms of set functions and their preimages. This theorem requires the function `f` to be measurable, and it is stated for all measurable sets `s`.
More concisely: Given measurable spaces `(α, m0)` and `(β, inst)`, a measure `μ` on `α`, a measurable function `f : α -> β`, and a measurable set `s` in `β`, the pushforward measure of the restriction of `μ` to `f⁁⁻¹(s)` is equal to the restriction of the pushforward measure of `μ` under `f` to `s`.
|
MeasurableEmbedding.restrict_map
theorem MeasurableEmbedding.restrict_map :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
MeasurableEmbedding f →
∀ (μ : MeasureTheory.Measure α) (s : Set β),
(MeasureTheory.Measure.map f μ).restrict s = MeasureTheory.Measure.map f (μ.restrict (f ⁻¹' s))
The theorem `MeasurableEmbedding.restrict_map` states that for any types `α` and `β`, any measurable spaces `m0` and `m1` on `α` and `β respectively`, any function `f` from `α` to `β` that is a measurable embedding, any measure `μ` on `α`, and any set `s` of `β`, the measure obtained by first applying the map `f` to the measure `μ` and then restricting to the set `s` is the same as the measure obtained by first restricting `μ` to the preimage of `s` under `f` and then applying the map `f`. In mathematical notation, this can be written as `(f_*(μ)).restrict(s) = f_* (μ.restrict(f^(-1)(s)))`. This is a property about the interaction between the pushforward of a measure and the restriction of a measure.
More concisely: For any measurable spaces `m0` on `α`, `m1` on `β`, measurable embedding `f` from `α` to `β`, measure `μ` on `α`, and set `s` of `β`, `(f_* μ).restrict(s) = f_* (μ.restrict(f⁻¹(s)))`.
|
indicator_ae_eq_of_ae_eq_set
theorem indicator_ae_eq_of_ae_eq_set :
∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s t : Set α} {f : α → β}
[inst_1 : Zero β], μ.ae.EventuallyEq s t → μ.ae.EventuallyEq (s.indicator f) (t.indicator f)
The theorem `indicator_ae_eq_of_ae_eq_set` states that for all types `α` and `β`, given a measurable space on `α`, a measure `μ` on `α`, sets `s` and `t` of `α`, and a function `f` from `α` to `β`, if the two sets `s` and `t` are almost everywhere equal with respect to the measure `μ`, then the indicator functions of `s` and `t` with respect to `f` are also almost everywhere equal with respect to the measure `μ`. Here, an indicator function of a set, given a function, outputs the value of the function at a point if the point is in the set, and `0` otherwise. The term "almost everywhere" means that the property holds everywhere except possibly on a set of measure zero.
More concisely: Given measurable sets $s, t \subseteq \alpha$ and a measurable function $f:\alpha \to \beta$, if $s$ and $t$ are almost equal to each other with respect to the measure $\mu$ on $\alpha$, then their indicator functions $1\_s$ and $1\_t$ with respect to $f$ are almost everywhere equal with respect to $\mu$.
|
MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl
theorem MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (t : Set α) {p : α → Prop},
(∀ᵐ (x : α) ∂μ.restrict t, p x) → (∀ᵐ (x : α) ∂μ.restrict tᶜ, p x) → ∀ᵐ (x : α) ∂μ, p x
The theorem `MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl` states that for all types `α`, measurable spaces `m0` and measures `μ`, and for any set `t` and property `p` defined on `α`, if almost every element in the restriction of measure `μ` to set `t` satisfies property `p` and also if almost every element in the restriction of measure `μ` to the complement of `t` satisfies property `p`, then almost every element in the entire space under measure `μ` satisfies property `p`. This theorem, in essence, is about the properties of measurable spaces under restrictions and their complements.
More concisely: If two sets in a measurable space have almost every element satisfying a property with respect to a measure, then almost every element in their union satisfies the property.
|
MeasureTheory.Measure.restrict_zero
theorem MeasureTheory.Measure.restrict_zero :
∀ {α : Type u_2} {_m0 : MeasurableSpace α} (s : Set α), 0.restrict s = 0
This theorem, `MeasureTheory.Measure.restrict_zero`, states that for any given type `α` and any measurable space of type `α`, when we restrict the zero measure to any set `s` of type `α`, it remains the zero measure. This essentially means that the restriction of the zero measure to any set is still the zero measure. In mathematical terms, given a measure space (denoted by `α` and `_m0`), for all subsets `s` in that space, the restrict function applied to the zero measure and `s` will always yield the zero measure.
More concisely: For any measurable space `(α, _m0)` and subset `s` of `α`, the restriction of the zero measure `m0` to `s` is still the zero measure, i.e., `m0.restrict s = 0`.
|
MeasureTheory.Measure.ext_of_iUnion_eq_univ
theorem MeasureTheory.Measure.ext_of_iUnion_eq_univ :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : Countable ι]
{s : ι → Set α}, ⋃ i, s i = Set.univ → (∀ (i : ι), μ.restrict (s i) = ν.restrict (s i)) → μ = ν
This theorem, named `MeasureTheory.Measure.ext_of_iUnion_eq_univ`, states that given two measures, `μ` and `ν`, in a measurable space `α`, and a countable collection of subsets `s` indexed by `ι` such that the union of all these subsets equals the universal set, if the restrictions of `μ` and `ν` to each subset `s i` are equal for every index `i`, then the two measures `μ` and `ν` are equal. This is an alias for the reverse direction of `MeasureTheory.Measure.ext_iff_of_iUnion_eq_univ`.
More concisely: If two measures on a measurable space agree on every sub-SET in a countable collection whose UNION is the universal set, then the measures are equal.
|
MeasureTheory.ae_restrict_congr_set
theorem MeasureTheory.ae_restrict_congr_set :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : α → Prop},
μ.ae.EventuallyEq s t → ∀ {p : α → Prop}, (∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ.restrict t, p x
This theorem states that for any given type 'α', measurable space 'm0' defined on 'α', measure 'μ' defined on the measurable space, and sets 's' and 't' represented as properties of 'α', if 's' and 't' are almost everywhere equal with respect to measure 'μ', then any property 'p' of 'α' that is almost everywhere true on the set 's' (with respect to the measure restricted to 's') is also almost everywhere true on the set 't' (with respect to the measure restricted to 't'), and vice versa. Essentially, it states that almost everywhere equivalence of sets preserves the almost everywhere truth of propositions when the measure is restricted to these sets.
More concisely: If sets 's' and 't' of type 'α' are almost everywhere equal with respect to measurable space 'm0' and measure 'μ', then any property 'p' almost everywhere true on 's' is also almost everywhere true on 't', and vice versa.
|
MeasurableEmbedding.ae_map_iff
theorem MeasurableEmbedding.ae_map_iff :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
MeasurableEmbedding f →
∀ {p : β → Prop} {μ : MeasureTheory.Measure α},
(∀ᵐ (x : β) ∂MeasureTheory.Measure.map f μ, p x) ↔ ∀ᵐ (x : α) ∂μ, p (f x)
The theorem `MeasurableEmbedding.ae_map_iff` states that for any types `α` and `β`, measurable spaces `m0` and `m1` on `α` and `β` respectively, a function `f` from `α` to `β`, if `f` is a measurable embedding, then for any property `p` of elements in `β` and any measure `μ` on `α`, the property `p` holds almost everywhere for the measure induced by mapping `μ` via `f` if and only if the property `p` composed with `f` holds almost everywhere with respect to `μ`. "Almost everywhere" is a measure-theoretic concept meaning that the set of points where the property does not hold has measure zero.
More concisely: For measurable spaces (α, m0) and (β, m1), function f: α → β being a measurable embedding implies that m0-almost everywhere x in α has image under f that satisfies property p if and only if property p holds m1-almost everywhere for the image of x under f.
|
MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict
theorem MeasureTheory.Measure.restrict_toOuterMeasure_eq_toOuterMeasure_restrict :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → ↑(μ.restrict s) = (MeasureTheory.OuterMeasure.restrict s) ↑μ
This theorem states that for any type `α`, measurable space `m0`, measure `μ`, and set `s` in `α` that is measurable, the measure `μ` restricted to set `s` is equal to the restriction of the outer measure of `μ` to set `s`. In other words, the operation of restricting a measure to a set commutes with the operation of converting a measure to an outer measure. This is a property of measure theory, and it essentially states that the order in which you restrict a measure to a set and convert it to an outer measure doesn't matter - you will end up with the same result either way.
More concisely: For any measurable set `s` in a measurable space `(α, ℳ, μ)`, the restriction of `μ` to `s` equals the outer measure of `μ` restricted to `s`. In other words, `μ(s) = ℱ⁺(μ)(s)`, where `ℱ⁺` denotes the outer measure operation.
|
MeasureTheory.Measure.restrict_eq_self
theorem MeasureTheory.Measure.restrict_eq_self :
∀ {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s t : Set α},
s ⊆ t → ↑↑(μ.restrict t) s = ↑↑μ s
This theorem states that, for every type `α` with a measurable space structure `m0` and any measure `μ` on that space, and any two sets of elements of `α`, `s` and `t`, if `s` is a subset of `t`, then the measure of `s` when restricted to `t` is equal to the original measure of `s`. In mathematical terms, given any measure `μ` and sets `s` and `t` with `s ⊆ t`, we have `μ.restrict(t)(s) = μ(s)`.
More concisely: For every measurable space `(α, m0)` and measure `μ`, if `s ⊆ t` are sets in `α`, then `μ.restrict(t)(s) = μ(s)`.
|
MeasureTheory.self_mem_ae_restrict
theorem MeasureTheory.self_mem_ae_restrict :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasurableSet s → s ∈ (μ.restrict s).ae
This theorem states that for any type `α`, given a measurable space `m0` of `α`, a measure `μ` on the measurable space, and a set `s` of `α` that is measurable, the set `s` belongs to the "almost everywhere" filter of the measure restricted to `s`. In more intuitive terms, it says that under given conditions, a measurable set is almost everywhere in the restricted measure space of itself.
More concisely: For any measurable space `(α, m0)`, measurable set `s` of `α`, and measure `μ` on `m0`, `s` belongs to the "almost everywhere" filter of the restriction `μ | s`.
|
MeasureTheory.ae_restrict_uIoc_iff
theorem MeasureTheory.ae_restrict_uIoc_iff :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : LinearOrder α] {a b : α}
{P : α → Prop},
(∀ᵐ (x : α) ∂μ.restrict (Ι a b), P x) ↔
(∀ᵐ (x : α) ∂μ.restrict (Set.Ioc a b), P x) ∧ ∀ᵐ (x : α) ∂μ.restrict (Set.Ioc b a), P x
This theorem states that for any type `α` with a measurable space structure `m0`, a measure `μ`, a linear order structure, and any two elements `a` and `b` of `α`, as well as any property `P` from `α` to `Prop`, the property `P` holds almost everywhere (except for a set of measure zero) with respect to the measure `μ` restricted to the closed interval between `a` and `b` if and only if `P` holds almost everywhere with respect to the measure `μ` restricted to the left-open right-closed interval from `a` to `b` and the left-open right-closed interval from `b` to `a`. In mathematical terms, this theorem relates the concept of almost everywhere for different types of intervals.
More concisely: For any measurable space `(α, m0)`, measure `μ`, linear order `<`, and property `P` on `α`, if `P` holds almost everywhere in the closed interval `[a, b]` with respect to `μ`, then `P` holds almost everywhere in both the left-open right-closed intervals `(a, b]` and `[b, a]`.
|
indicator_ae_eq_restrict_compl
theorem indicator_ae_eq_restrict_compl :
∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
[inst_1 : Zero β], MeasurableSet s → (μ.restrict sᶜ).ae.EventuallyEq (s.indicator f) 0
The theorem `indicator_ae_eq_restrict_compl` states that for any type `α` and `β`, where `α` is equipped with a measurable space structure, and given a measure `μ` on `α`, a set `s` of `α`, and a function `f` from `α` to `β` such that `β` is equipped with a zero structure and `s` is a measurable set, the indicator function of `s` and `f` is almost everywhere equal to `0` on the measure space restricted to the complement of `s`. In other words, it says that outside the set `s`, the indicator function is `0` almost everywhere according to the measure `μ`.
More concisely: For any measurable set `s` and measurable function `f` from a measure space `(α, μ) to a zero-structured type `β`, the indicator function of `s` is almost everywhere equal to the zero function `0` on the complement of `s`.
|
MeasureTheory.Measure.restrict_eq_self_of_ae_mem
theorem MeasureTheory.Measure.restrict_eq_self_of_ae_mem :
∀ {α : Type u_2} {_m0 : MeasurableSpace α} ⦃s : Set α⦄ ⦃μ : MeasureTheory.Measure α⦄,
(∀ᵐ (x : α) ∂μ, x ∈ s) → μ.restrict s = μ
This theorem is about measure theory in the context of measurable spaces. It states that for any type `α` and any measurable space `_m0` of type `α`, given a set `s` of type `α` and a measure `μ` (from the measure theory) on `α`, if almost everywhere (with respect to the measure `μ`) an element `x` of type `α` belongs to the set `s`, then the restriction of the measure `μ` to the set `s` is equal to the measure `μ` itself. In other words, when almost every point in the space is in `s`, restricting the measure to `s` doesn't change the measure.
More concisely: If a set `s` is almost everywhere equal to a measurable space `μ` with respect to measure `μ`, then the restriction of `μ` to `s` is equal to `μ`.
|
MeasureTheory.ae_restrict_iff'₀
theorem MeasureTheory.ae_restrict_iff'₀ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
MeasureTheory.NullMeasurableSet s μ → ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
This theorem states that for any type `α`, measurable space `m0`, measure `μ`, set `s` of type `α`, and a property `p` from `α` to `Prop`, if `s` is a null measurable set with respect to measure `μ`, then the property `p` holds almost everywhere with respect to the measure restricted to `s` if and only if the property `p` holds almost everywhere in the measure `μ` under the condition that `x` belongs to `s`. Here, "almost everywhere" means for all but a subset of `α` of measure zero.
More concisely: For any measurable space `(α, m0)`, measure `μ`, set `s` of type `α`, and property `p` from `α` to `Prop`, if `s` is a null set with respect to `μ`, then `p` holds almost everywhere on `s` if and only if `p` holds almost everywhere on `α` for elements in `s`.
|
MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ
theorem MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set (Set α)},
S.Countable → S.sUnion = Set.univ → (μ = ν ↔ ∀ s ∈ S, μ.restrict s = ν.restrict s)
This theorem states that for any type `α`, any measurable space `m0` of type `α`, and any two measures `μ` and `ν` of that measurable space, given a set `S` of sets of type `α` such that `S` is countable and the union of all the sets in `S` equals the universal set, then `μ` is equal to `ν` if and only if for all sets `s` in `S`, the restriction of `μ` to `s` is equal to the restriction of `ν` to `s`. It essentially states that two measures are considered equal if they agree on the measures of all sets in a countable collection that spans the whole space.
More concisely: Two measures on a countable union of measurable sets are equal if and only if their restrictions to each set are equal.
|
MeasureTheory.Measure.restrict_apply_univ
theorem MeasureTheory.Measure.restrict_apply_univ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s : Set α),
↑↑(μ.restrict s) Set.univ = ↑↑μ s
This theorem states that for any type `α`, any measurable space `m0` defined on `α`, any measure `μ` of `MeasureTheory.Measure α`, and any set `s` of `Set α`, the measure of the universal set `Set.univ` restricted to the set `s` equals the measure of the set `s`. In other words, when we restrict our measure to a specific set, the measure of the entire universe is simply the measure of that set.
More concisely: For any measurable space `(α, m0)`, measure `μ` of type `MeasureTheory.Measure α`, and set `s` of type `Set α`, we have `μ (Set.univ) = μ s`.
|
MeasureTheory.ae_restrict_of_ae
theorem MeasureTheory.ae_restrict_of_ae :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
(∀ᵐ (x : α) ∂μ, p x) → ∀ᵐ (x : α) ∂μ.restrict s, p x
This theorem, named `MeasureTheory.ae_restrict_of_ae`, states that for any type `α`, any measurable space `m0` of type `α`, any measure `μ` of type `α`, any set `s` of type `α`, and any property `p` applicable to `α`, if `p` holds almost everywhere (i.e., outside a set of measure zero) with respect to measure `μ`, then `p` also holds almost everywhere with respect to the measure `μ` restricted to set `s`. In other words, restricting the measure to a subset does not affect the almost everywhere validity of a property.
More concisely: If a property holds almost everywhere with respect to a measure on a set, then it also holds almost everywhere with respect to the measure restricted to that set.
|
MeasureTheory.Measure.restrict_iUnion_le
theorem MeasureTheory.Measure.restrict_iUnion_le :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Countable ι]
{s : ι → Set α}, μ.restrict (⋃ i, s i) ≤ MeasureTheory.Measure.sum fun i => μ.restrict (s i)
This theorem, `MeasureTheory.Measure.restrict_iUnion_le`, states that for any type `α`, index type `ι`, measurable space `m0` on `α`, and measure `μ` on `α`, given an indexed family of sets `s : ι → Set α`, the measure restricted to the union of these sets, `μ.restrict (⋃ i, s i)`, is less than or equal to the sum of the measures restricted to each individual set, `MeasureTheory.Measure.sum fun i => μ.restrict (s i)`. In other words, the measure of a union of sets is less than or equal to the sum of the measures of the individual sets. This is a formal statement of the concept of subadditivity in measure theory.
More concisely: The measure of a union of measurable sets is less than or equal to the sum of the measures of the individual sets in a measurable space.
|
MeasureTheory.Measure.restrict_union
theorem MeasureTheory.Measure.restrict_union :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
Disjoint s t → MeasurableSet t → μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
This theorem relates to measure theory in the field of mathematics. It states that for any set of elements of type `α` (with `α` having an associated measurable space and measure), if two subsets `s` and `t` are disjoint (meaning the infimum, or greatest lower bound, of the two sets is the bottom element) and if the set `t` is measurable, then the measure of the union of `s` and `t` (restricted to the elements in `s` union `t`) is equal to the sum of the measures of `s` and `t`, each restricted to their own elements. This theorem captures the intuitive idea of the measure of the union of two disjoint, measurable sets being the sum of the individual measures.
More concisely: Given measurable sets `s` and `t` with no elements in common (disjoint), the measure of their union equals the sum of their individual measures.
|
MeasurableEmbedding.comap_apply
theorem MeasurableEmbedding.comap_apply :
∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} {m1 : MeasurableSpace β} {f : α → β},
MeasurableEmbedding f →
∀ (μ : MeasureTheory.Measure β) (s : Set α), ↑↑(MeasureTheory.Measure.comap f μ) s = ↑↑μ (f '' s)
This theorem, `MeasurableEmbedding.comap_apply`, states that for any types `α` and `β`, any measurable spaces `m0` and `m1` over `α` and `β` respectively, and any function `f` from `α` to `β`, if `f` is a measurable embedding, then for any measure `μ` on `β` and any set `s` of `α`, the measure of `s` under the pushforward measure induced by `f` from `μ`, is equal to the measure of the image of `s` under `f` in the measure `μ`. In essence, it provides a relationship between measures on the original and image sets under a measurable embedding.
More concisely: For any measurable spaces `m0` over `α`, `m1` over `β`, measurable embedding `f` from `α` to `β`, and measure `μ` on `β`, the pushforward measure of `μ` under `f` of a set `s` in `m0` equals the measure of the image of `s` under `f`.
|
MeasureTheory.ae_restrict_mem₀
theorem MeasureTheory.ae_restrict_mem₀ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
MeasureTheory.NullMeasurableSet s μ → ∀ᵐ (x : α) ∂μ.restrict s, x ∈ s
The theorem `MeasureTheory.ae_restrict_mem₀` states that for any type `α`, given a measurable space `m0` over `α`, a measure `μ` on this space, and a set `s` of type `α` that is a null measurable set with respect to measure `μ`, almost every element `x` from `α` with respect to the restriction of measure `μ` to set `s` is an element of `s`. In simpler terms, the theorem is saying that under these conditions, the set `s` almost entirely consists of elements that are in `s` when we consider the measure restricted to `s`.
More concisely: Given a measurable space `(α, ℳ, μ)`, if `μ(s) = 0` for a set `s ∈ ℳ`, then almost every element `x ∈ α` belongs to `s` with respect to the restriction `μ|s` of `μ` to `s`.
|
MeasureTheory.Measure.restrict_zero_set
theorem MeasureTheory.Measure.restrict_zero_set :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, ↑↑μ s = 0 → μ.restrict s = 0
This theorem, named `MeasureTheory.Measure.restrict_zero_set`, states that for any given type `α`, a measurable space `m0` of type `α`, a measure `μ` in the measure theory of type `α`, and a set `s` of type `α`, if the measure `μ` of the set `s` is zero (denoted as `↑↑μ s = 0`), then the restriction of the measure `μ` to the set `s` is also zero (denoted as `μ.restrict s = 0`). In simpler terms, if a set has a measure of zero, then any measure restricted to that set is also zero.
More concisely: If a measurable set has zero measure in a given measure space, then its restriction to that set has measure zero as well.
|
MeasureTheory.Measure.restrict_union₀
theorem MeasureTheory.Measure.restrict_union₀ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.AEDisjoint μ s t →
MeasureTheory.NullMeasurableSet t μ → μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
This theorem states that for any type `α`, given a measurable space `m0` on `α`, a measure `μ` on that measurable space, and two sets `s` and `t` of type `α`, if `s` and `t` are almost everywhere disjoint with respect to the measure `μ` and the set `t` is null measurable with respect to the measure `μ`, then the measure of the union of `s` and `t` restricted by `μ` is equal to the sum of the measures of `s` and `t` respectively restricted by `μ`. In other words, this theorem provides a way to measure the union of two sets that are almost everywhere disjoint and where one of the sets is null measurable.
More concisely: Given measurable spaces `(α, m0)`, a measure `μ`, and sets `s` and `t` of type `α` with `s ∩ t` null with respect to `μ`, the measure of `s ∪ t` restricted by `μ` equals the sum of the measures of `s` and `t` restricted by `μ`.
|
MeasureTheory.Measure.restrict_restrict_of_subset
theorem MeasureTheory.Measure.restrict_restrict_of_subset :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
s ⊆ t → (μ.restrict t).restrict s = μ.restrict s
This theorem is about the measure theory in mathematics. It states that for any type `α`, given a measurable space `m0` of this type, a measure `μ` on this measurable space, and two sets `s` and `t` of this type, if set `s` is a subset of set `t`, then restricting the measure `μ` to set `t` and then further restricting it to set `s` is equivalent to directly restricting the measure `μ` to set `s`.
In other words, the restriction of the restriction of a measure is the restriction of the measure itself, provided that the subset relationship holds between the sets.
More concisely: For any measurable space `(α, m0)` and measure `μ`, if `s ≤ t` are subsets of `α`, then `μ!(t) | s = μ!(s)`.
|
MeasureTheory.ae_restrict_iff
theorem MeasureTheory.ae_restrict_iff :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {p : α → Prop},
MeasurableSet {x | p x} → ((∀ᵐ (x : α) ∂μ.restrict s, p x) ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → p x)
The theorem `MeasureTheory.ae_restrict_iff` states that for any type `α`, measurable space `m0`, measure `μ`, set `s` of `α`, and a property `p` of `α`, if the set of elements that satisfy the property `p` is a measurable set, then a property `p` holds almost everywhere (`∀ᵐ (x : α)`) under the restriction of the measure `μ` to the set `s` if and only if (`↔`) the property `p` holds almost everywhere under the measure `μ` whenever the element `x` is in the set `s`. This theorem essentially captures the relationship between a property holding almost everywhere under a restricted measure and the same property holding almost everywhere under the original measure conditional on set membership.
More concisely: For any measurable space `(α, Σ, μ)`, set `s ∈ Σ`, and property `p(x) : Prop` such that `{x : α | p x} ∈ Σ`, the property `p` holds almost everywhere in `s` if and only if it holds almost everywhere in `α` for elements `x` in `s`.
|
MeasureTheory.Measure.ext_of_biUnion_eq_univ
theorem MeasureTheory.Measure.ext_of_biUnion_eq_univ :
∀ {α : Type u_2} {ι : Type u_6} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set ι}
{s : ι → Set α}, S.Countable → ⋃ i ∈ S, s i = Set.univ → (∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)) → μ = ν
This theorem, named `MeasureTheory.Measure.ext_of_biUnion_eq_univ`, states that for any type `α` and index type `ι`, given a measurable space `m0` on `α` and two measures `μ` and `ν` on this space, along with a countable set `S` of indices and a function `s` mapping each index to a set in `α`, if the union of all the sets `s i` for `i` in `S` equals the universal set, and the restrictions of the measures `μ` and `ν` to each set `s i` are equal for all `i` in `S`, then the measures `μ` and `ν` are equal. In simpler terms, if two measures agree on a spanning collection of sets that covers the entire space, then they are equal.
More concisely: If for any measurable space with measurable sets indexed by a countable index type, the measures agree on each index's set and the union of all sets equals the universal set, then the measures are equal.
|
MeasureTheory.Measure.restrict_add
theorem MeasureTheory.Measure.restrict_add :
∀ {α : Type u_2} {_m0 : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) (s : Set α),
(μ + ν).restrict s = μ.restrict s + ν.restrict s
This theorem states that for any given types `α`, for any `MeasurableSpace α` and for any two measures `μ` and `ν` on this measurable space, and for any set `s` of type `α`, the restriction of the sum of the two measures `μ` and `ν` to the set `s` is equal to the sum of the restrictions of `μ` and `ν` to `s`. In other words, this theorem is a property of measures stating that restricting the sum of two measures to a set equals the sum of the individual measures restricted to that set.
More concisely: For any measurable spaces `(α, Σ)`, measures `μ, ν` on `Σ`, and set `s ∈ Σ`, the restriction of `μ + ν` to `s` equals the sum of the restrictions of `μ` and `ν` to `s`.
|
MeasureTheory.Measure.restrict_apply_self
theorem MeasureTheory.Measure.restrict_apply_self :
∀ {α : Type u_2} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : Set α), ↑↑(μ.restrict s) s = ↑↑μ s
This theorem states that for any type `α`, any measurable space `m0` over `α`, any measure `μ` from measure theory over `α`, and any set `s` of type `α`, the measure of the set `s` when restricted to `s` itself is the same as the original measure of the set `s`. In other words, restricting the measure to the set doesn't change the measure of the set.
More concisely: For any measurable space `(α, m)`, measure `μ`, and set `s` in `α`, the measure `μ` of `s` is equal to the measure of `s` under the restriction of `μ` to `s`.
|
MeasureTheory.Measure.ext_of_generateFrom_of_iUnion
theorem MeasureTheory.Measure.ext_of_generateFrom_of_iUnion :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (C : Set (Set α)) (B : ℕ → Set α),
m0 = MeasurableSpace.generateFrom C →
IsPiSystem C →
⋃ i, B i = Set.univ → (∀ (i : ℕ), B i ∈ C) → (∀ (i : ℕ), ↑↑μ (B i) ≠ ⊤) → (∀ s ∈ C, ↑↑μ s = ↑↑ν s) → μ = ν
This theorem states that, given a type `α` and a measurable space `m0` over `α`, two measures `μ` and `ν` on this measurable space are equal under the following conditions:
1. `m0` equals the smallest measure space containing a collection of basic sets `C`.
2. `C` is a π-system, that is, a collection of subsets of `α` that is closed under binary intersection of non-disjoint sets.
3. There exists a sequence of sets `B : ℕ → Set α` such that their union covers the whole set (`Set.univ`) and each set `B i` is in `C`.
4. Additionally, for each `i`, the measure `μ` of `B i` is finite.
5. Finally, for all sets `s` in `C`, `μ` and `ν` agree, i.e., `μ s = ν s`.
In simpler terms, if you have two measures that agree on a π-system of sets, and those sets can be combined to cover the entire space in a way that each measure of the sets is finite, then those two measures are equal.
More concisely: Given a measurable space with a π-system of sets `C` that is closed under finite intersections, if two measures agree on all sets in `C` and there exists a sequence of sets in `C` whose finite unions cover the entire space and have finite measure under each measure, then the two measures are equal.
|
MeasureTheory.Measure.le_restrict_apply
theorem MeasureTheory.Measure.le_restrict_apply :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t : Set α),
↑↑μ (t ∩ s) ≤ ↑↑(μ.restrict s) t
The theorem, `MeasureTheory.Measure.le_restrict_apply`, states that for any given type `α`, a measurable space `m0` on `α`, a measure `μ` on the measurable space `α`, and any two sets `s` and `t` of type `α`, the measure of the intersection of sets `t` and `s` is less than or equal to the measure of `t` when `μ` is restricted to `s`. In mathematical terms, this can be written as: `μ(t ∩ s) ≤ (μ restricted to s)(t)`. This theorem basicallly confines the measure to the specified set `s`.
More concisely: For any measurable space `(α, m0)`, measure `μ` on `α`, and sets `s` and `t` of `α`, we have `μ(t ∩ s) ≤ μ(s)(t)`.
|
MeasureTheory.Measure.restrict_restrict₀
theorem MeasureTheory.Measure.restrict_restrict₀ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.NullMeasurableSet s (μ.restrict t) → (μ.restrict t).restrict s = μ.restrict (s ∩ t)
This theorem is about the restriction of measures in measure theory. It states that for any type `α` equipped with a `MeasurableSpace` structure, any measure `μ` on `α`, and any two sets `s` and `t` of type `α`, if `s` is a Null Measurable Set with respect to the restriction of `μ` to `t`, then the restriction of the restriction of `μ` to `t` to `s` is equal to the restriction of `μ` to the intersection of `s` and `t`. In other words, restricting the measure twice (first on `t` then on `s`) is the same as restricting it once on the intersection of `s` and `t`, provided `s` is a Null Measurable Set under the restricted measure.
More concisely: If `μ` is a measure on a measurable space `(α, Σ)` and `s` is a Null Measurable Set in `t ∈ Σ`, then the restriction of `μ` to `s` under `t` equals the restriction of `μ` to `s ∩ t`.
|
MeasureTheory.Measure.restrict_restrict
theorem MeasureTheory.Measure.restrict_restrict :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasurableSet s → (μ.restrict t).restrict s = μ.restrict (s ∩ t)
The theorem `MeasureTheory.Measure.restrict_restrict` states that for any type `α` with a measurable space `m0` and a measure `μ`, and for any sets `s` and `t` of type `α`, if `s` is a measurable set, then restricting the measure `μ` first to the set `t` and then to the set `s` is the same as directly restricting the measure `μ` to the intersection of the sets `s` and `t`. This is written in Lean 4 as `(μ.restrict t).restrict s = μ.restrict (s ∩ t)`.
More concisely: For any measurable space `(α, m0)` and measure `μ`, if `s` is a measurable set in `α`, then `(μ.restrict s).restrict t = μ.restrict (s ∩ t)`.
|
MeasureTheory.Measure.restrict_apply
theorem MeasureTheory.Measure.restrict_apply :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasurableSet t → ↑↑(μ.restrict s) t = ↑↑μ (t ∩ s)
This theorem states that for any type `α`, equipped with a measurable space `m0` and a measure `μ`, and for any sets `s` and `t` of type `α`, if `t` is a measurable set, then the measure of `t` with respect to the restriction of the measure to `s` equals the outer measure of the intersection of `t` and `s`. There's a different version of this theorem where `s` is required to be measurable instead of `t`, known as `Measure.restrict_apply'`.
More concisely: For any measurable set `t` of type `α` in a measurable space `(α, m0)` with measure `μ`, the measure of `t` under the restriction of `μ` to a set `s` equals the outer measure of `t ∩ s`.
|
MeasureTheory.Measure.ext_of_sUnion_eq_univ
theorem MeasureTheory.Measure.ext_of_sUnion_eq_univ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {S : Set (Set α)},
S.Countable → S.sUnion = Set.univ → (∀ s ∈ S, μ.restrict s = ν.restrict s) → μ = ν
This theorem, known as an **alias** of the reverse direction of `MeasureTheory.Measure.ext_iff_of_sUnion_eq_univ`, states that for any type `α` with a measurable space `m0`, and any two measures `μ` and `ν` on this measurable space, if we have a countable set `S` of subsets of `α` such that the union of all sets in `S` forms the universal set of `α`, then if `μ` and `ν` have the same restrictions on each set in `S`, it follows that `μ` and `ν` are equal. In other words, this theorem provides a characterization of equality of measures in terms of their restrictions to a spanning collection of sets.
More concisely: Given measurable spaces `(α, m0)` and measures `μ` and `ν`, if there is a countable set `S` of subsets of `α` whose union equals `α`, and `μ(X) = ν(X)` for all `X ∈ S`, then `μ = ν`.
|
MeasureTheory.Measure.restrict_apply₀'
theorem MeasureTheory.Measure.restrict_apply₀' :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
MeasureTheory.NullMeasurableSet s μ → ↑↑(μ.restrict s) t = ↑↑μ (t ∩ s)
This theorem states that for any type `α`, given a measurable space `m0` on `α`, a measure `μ`, and two sets `s` and `t` of type `α`, if `s` is a `NullMeasurableSet` with respect to measure `μ`, the measure of `t` restricted to `s` is equal to the measure of the intersection of `t` and `s`. In other words, when we restrict the measure `μ` to the null measurable set `s` and apply this restricted measure to set `t`, it is the same as applying the original measure `μ` to the intersection of `t` and `s`.
More concisely: For any measurable space `(α, m0)`, measure `μ`, and null measurable sets `s` and `t` in `α`, the restricted measure `μ`|`s` of set `t` equals the measure of their intersection `s ∩ t`.
|
MeasureTheory.ae_eventually_not_mem
theorem MeasureTheory.ae_eventually_not_mem :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : ℕ → Set α},
∑' (i : ℕ), ↑↑μ (s i) ≠ ⊤ → ∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, x ∉ s n
This theorem is a version of the Borel-Cantelli lemma. It states that given a sequence of sets `sᵢ` in a measurable space `α` with a measure `μ`, if the series of the measures of the sets `sᵢ` is not infinite (i.e., `∑' (i : ℕ), ↑↑μ (s i) ≠ ⊤`), then almost all elements `x` in the space (with respect to the measure `μ`) are not in almost all of the sets `sᵢ`. Here "almost all" is in terms of measure, meaning that the set of exceptions has measure zero. And "almost all" sets `sᵢ` refers to a condition that holds for all sets in the sequence `sᵢ` from some point onward, formalized as `∀ᶠ (n : ℕ) in Filter.atTop`.
More concisely: If the sum of the measures of a sequence of sets in a measurable space is finite, then almost all elements belong to only finitely many sets in the sequence.
|
MeasureTheory.Measure.restrict_apply_le
theorem MeasureTheory.Measure.restrict_apply_le :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (s t : Set α), ↑↑(μ.restrict s) t ≤ ↑↑μ t
This theorem states that for any type `α` equipped with a measurable space structure `m0` and any measure `μ` on this space, for any sets `s` and `t` of type `α`, the measure of the restriction of `μ` to `s` calculated on `t` is less than or equal to the measure of `t` itself under `μ`. In other words, restricting a measure to a subset doesn't increase the measure of any other set.
More concisely: For any measurable spaces `(α, m0)`, measures `μ`, sets `s ⊆ α`, and subsets `t ⊆ α`, we have `μ s t ≤ μ t`.
|
MeasureTheory.measure_setOf_frequently_eq_zero
theorem MeasureTheory.measure_setOf_frequently_eq_zero :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ℕ → α → Prop},
∑' (i : ℕ), ↑↑μ {x | p i x} ≠ ⊤ → ↑↑μ {x | ∃ᶠ (n : ℕ) in Filter.atTop, p n x} = 0
This theorem is a version of the Borel-Cantelli lemma in measure theory. It states that if we have a sequence of predicates, `p_i`, on a measurable space and the sum of the measures of the sets `{x | p_i x}` is finite (i.e., it does not equal infinity), then the measure of the set of elements `x` for which `p_i x` holds frequently as `i` tends to infinity (or equivalently, `p_i x` holds for infinitely many `i`) is equal to zero. In other words, if the measures of the sets where each predicate in the sequence holds is not infinite, then the measure of the set where the predicates hold frequently is zero.
More concisely: If a sequence of measurable sets in a measure space has finite total measure, then the measure of their intersection, containing elements where infinitely many sets in the sequence intersect, is zero.
|
MeasureTheory.Measure.restrict_univ
theorem MeasureTheory.Measure.restrict_univ :
∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.restrict Set.univ = μ
The `MeasureTheory.Measure.restrict_univ` theorem is a statement about measure theory in the context of a measurable space. For any given type `α`, if `m0` is a measurable space on `α` and `μ` is a measure on that measurable space, the theorem postulates that restricting the measure `μ` to the universal set of `α` (which includes all elements of `α`) is equivalent to the original measure `μ`. In other words, restricting a measure to the entire set doesn't change the measure.
More concisely: For any measurable space (α, M, m0) and measure μ on m0, the restriction of μ to the universal set of α is equal to μ itself.
|