MeasureTheory.Measure.toSignedMeasure_apply_measurable
theorem MeasureTheory.Measure.toSignedMeasure_apply_measurable :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
{i : Set α}, MeasurableSet i → ↑μ.toSignedMeasure i = (↑↑μ i).toReal
The theorem `MeasureTheory.Measure.toSignedMeasure_apply_measurable` states that for any given measure space `α`, with a measurable set `i` within it and a finite measure `μ`, the value of the signed measure acquired by converting `μ` is equal to the real value of `μ` evaluated at `i`. This holds true if `i` is a measurable set. In other words, if we convert a finite measure into a signed measure, then for any measurable set in the measure space, the value of the signed measure at that set is the same as the real value of the original measure at that set.
More concisely: For any measurable set `i` in a measure space and finite measure `μ`, the signed measure obtained from `μ` agrees with `μ` on `i`.
|
MeasureTheory.VectorMeasure.neg_apply
theorem MeasureTheory.VectorMeasure.neg_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
[inst_2 : TopologicalAddGroup M] (v : MeasureTheory.VectorMeasure α M) (i : Set α), ↑(-v) i = -↑v i
The theorem `MeasureTheory.VectorMeasure.neg_apply` states that for any measurable space `α` and any set `i` of type `α`, and a vector measure `v` on `α` with values in a topological additive commutative group `M`, the measure of the set `i` under the negation of `v` equals the negation of the measure of the set `i` under `v`. In other words, negative of a vector measure applied to a set is equal to the negative of the measure of the set under the original vector measure. This holds for all measurable spaces and all vector measures taking values in a space that forms a topological additive commutative group.
More concisely: For any measurable space, set, vector measure, and topological additive commutative group, the negative of the measure of a set under a vector measure is equal to the measure of the set under the negation of the vector measure.
|
MeasureTheory.VectorMeasure.coe_smul
theorem MeasureTheory.VectorMeasure.coe_smul :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
{R : Type u_4} [inst_2 : Semiring R] [inst_3 : DistribMulAction R M] [inst_4 : ContinuousConstSMul R M] (r : R)
(v : MeasureTheory.VectorMeasure α M), ↑(r • v) = r • ↑v
The theorem `MeasureTheory.VectorMeasure.coe_smul` states that for any semiring `R`, any measurable space `α`, any additively commutative monoid `M` equipped with a topological space and a continuous scalar multiplication by `R`, any scalar `r` in `R`, and any vector measure `v` on `α` with values in `M`, the scalar multiplication of `r` and `v` (denoted `r • v`) is the same as the scalar multiplication of `r` and the coercion of `v` to a function (denoted `r • ↑v`). In other words, scalar multiplication interacts with the coercion to a function in the expected way when dealing with vector measures.
More concisely: For any semiring R, measurable space α, additively commutative monoid M with a topological space and continuous scalar multiplication, scalar r in R, and vector measure v on α with values in M, the scalar multiplication r • v equals the scalar multiplication r • ↑v.
|
MeasureTheory.VectorMeasure.neg_le_neg
theorem MeasureTheory.VectorMeasure.neg_le_neg :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : OrderedAddCommGroup M]
[inst_2 : TopologicalAddGroup M] (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
MeasurableSet i → v.restrict i ≤ w.restrict i → (-w).restrict i ≤ (-v).restrict i
The theorem `MeasureTheory.VectorMeasure.neg_le_neg` states that for any measurable space `α`, topological space `M` that is also an ordered additive commutative group and topological additive group, if we have two vector measures `v` and `w`, and a measurable set `i`, then if the restriction of `v` to `i` is less than or equal to the restriction of `w` to `i`, then the restriction of the negation of `w` to `i` is less than or equal to the restriction of the negation of `v` to `i`. In mathematical terms, if $v|_i \leq w|_i$, then $-w|_i \leq -v|_i$.
More concisely: For measurable sets i in a measurable space α, if vector measure v restriced to i is less than or equal to w's restriction, then the negation of w's restriction is less than or equal to the negation of v's restriction. In symbols: $-w|\_i \leq -v|\_i$ given $v|\_i \leq w|\_i$.
|
MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable
theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {i : Set α},
MeasurableSet i → ↑μ.toENNRealVectorMeasure i = ↑↑μ i
This theorem states that for any type `α`, any `MeasurableSpace α`, any measure `μ` of type `MeasureTheory.Measure α`, and any set `i` of type `Set α`, if `i` is a measurable set, then applying the function `MeasureTheory.Measure.toENNRealVectorMeasure` to the measure `μ` and then applying the result to `i` is equivalent to applying the measure `μ` to `i` and then lifting it twice to the extended non-negative reals (`↑↑μ i`). In other words, converting a measure to an extended non-negative real vector measure doesn't change the measure of a measurable set.
More concisely: For any measurable set `i` of type `α` in a measurable space `α` with measure `μ`, the extended non-negative real vector measure `MeasureTheory.Measure.toENNRealVectorMeasure μ` applied to `i` equals the measure `μ` applied to `i` lifted twice to the extended non-negative reals (`↑↑μ i`).
|
MeasureTheory.VectorMeasure.zero_apply
theorem MeasureTheory.VectorMeasure.zero_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
(i : Set α), ↑0 i = 0
This theorem states that for any type α, with a corresponding measurable space `m`, and any type M, which forms an additive commutative monoid and a topological space, the zero vector measure applied to any set `i` of type α is zero. In other words, if we have a measure space and a specific set within that space, the measure of that set under the zero vector measure is always zero, regardless of the specific elements in the set.
More concisely: For any measurable space (α, m), and any additive commutative monoid and topological space M, the zero vector measure assigns a measure of 0 to any set in α.
|
MeasureTheory.VectorMeasure.restrict_apply
theorem MeasureTheory.VectorMeasure.restrict_apply :
∀ {α : Type u_1} [inst : MeasurableSpace α] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
(v : MeasureTheory.VectorMeasure α M) {i : Set α},
MeasurableSet i → ∀ {j : Set α}, MeasurableSet j → ↑(v.restrict i) j = ↑v (j ∩ i)
This theorem states that for any measure space `α`, type `M` that has both an addition operation (forming a commutative monoid) and a topological structure, a vector measure `v` on `α` with values in `M`, and any measurable set `i` in `α`, the restriction of the vector measure `v` to the set `i` behaves as expected: for any measurable set `j`, the measure of `j` under the restricted measure equals the measure of the intersection of `j` and `i` under the original measure `v`. In mathematical terms, if `v` is a vector measure and `i` and `j` are measurable sets, then the measure of `j` under the restriction of `v` to `i` is equal to the measure of `j ∩ i` under `v`.
More concisely: For any measurable sets `i` and `j` in a measure space `α` with a commutative monoid and topology, and any vector measure `v` on `α` with values in the monoid, the measure of `j` under the restriction of `v` to `i` equals the measure of `j ∩ i` under `v`.
|
MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply
theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i j : Set α}
(hi : MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i)
(hi₁ : MeasurableSet i), MeasurableSet j → ↑↑(s.toMeasureOfZeroLE i hi₁ hi) j = ↑⟨↑s (i ∩ j), ⋯⟩
This theorem states that for any measurable space `α`, any signed measure `s` on `α`, and any two sets `i` and `j` in `α`, if the restriction of the zero vector measure to set `i` is less than or equal to the restriction of measure `s` to set `i` and if set `i` is measurable, then for any measurable set `j`, the measure of set `j` under the measure obtained from the function `toMeasureOfZeroLE` applied to measure `s` and set `i` is equal to the signed measure of the intersection of sets `i` and `j` under measure `s`.
In mathematical terms, for a signed measure `s`, sets `i` and `j` where `i` is measurable and the zero measure restricted to `i` is less than or equal to `s` restricted to `i`, the measure of `j` under `toMeasureOfZeroLE` applied to `s` and `i` is exactly the signed measure of the intersection of `i` and `j` under `s`.
More concisely: For any measurable spaces `α`, measurable sets `i` and `j`, and signed measure `s` on `α` such that the restriction of the zero measure to `i` is less than or equal to the restriction of `s` to `i`, the measure of `j` under the measure obtained from `s` and `i` via the function `toMeasureOfZeroLE` equals the signed measure of `i ∩ j` under `s`.
|
MeasureTheory.VectorMeasure.sub_apply
theorem MeasureTheory.VectorMeasure.sub_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommGroup M] [inst_1 : TopologicalSpace M]
[inst_2 : TopologicalAddGroup M] (v w : MeasureTheory.VectorMeasure α M) (i : Set α), ↑(v - w) i = ↑v i - ↑w i
The theorem `MeasureTheory.VectorMeasure.sub_apply` states that for any type `α`, a measurable space `m` over `α`, a type `M` with an additive commutative group structure, a topological space structure, and a topological additive group structure, and two vector measures `v` and `w` from `α` to `M`, the measure of the set `i` under the difference of `v` and `w` is equal to the difference of the measures of `i` under `v` and `w`. In other words, it is stating that the measure of a set under the subtraction of two vector measures is the same as subtracting the measures of the set under the individual vector measures. This can be written in mathematical notation as $(v - w)(i) = v(i) - w(i)$.
More concisely: For measurable spaces (α, m), additive commutative groups (M) with topological and topological additive group structures, and measurable vector functions v and w from α to M, the difference of their applications to a set i equals their individual applications to i, i.e., (v - w)(i) = v(i) - w(i).
|
MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat
theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
[inst_2 : T2Space M] (v : MeasureTheory.VectorMeasure α M) {f : ℕ → Set α},
(∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → ↑v (⋃ i, f i) = ∑' (i : ℕ), ↑v (f i)
This theorem, `MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat`, states that given a measurable space `α`, a type `M` with an addition commutative monoid structure and a topology such that every singleton set is a closed set (i.e., `M` is a T2 space), and a vector measure `v` from `α` to `M`, if we have a sequence of measurable sets `f : ℕ → Set α` such that each pair of sets in the sequence is disjoint, then the measure of the countable union of these sets (`⋃ i, f i`) under the vector measure `v` is equal to the sum of the measures of each individual set in the sequence (i.e., `∑' (i : ℕ), ↑v (f i)`). This is a generalization of the additivity property of measures to vector measures and disjoint countable unions of measurable sets.
More concisely: Given a measurable space, a T2 space with a commutative monoid structure and every singleton set closed, and a vector measure, the measure of the disjoint countable union of measurable sets under the vector measure equals the sum of the measures of each individual set.
|
MeasureTheory.VectorMeasure.zero_le_restrict_subset
theorem MeasureTheory.VectorMeasure.zero_le_restrict_subset :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M]
[inst_1 : OrderedAddCommMonoid M] (v : MeasureTheory.VectorMeasure α M) {i j : Set α},
MeasurableSet i →
j ⊆ i →
MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i →
MeasureTheory.VectorMeasure.restrict 0 j ≤ v.restrict j
This theorem states that for any measurable space `α`, with a given topological space `M` and an ordered additive commutative monoid `M`, for any vector measure `v` on `α` with values in `M`, and for any two sets `i` and `j` of `α` such that `i` is measurable and `j` is a subset of `i`, if the restriction of the zero vector measure to `i` is less than or equal to the restriction of `v` to `i`, then the restriction of the zero vector measure to `j` is also less than or equal to the restriction of `v` to `j`. In simpler terms, if the zero measure on a larger set is dominated by a vector measure, then the same holds for any subset of that larger set.
More concisely: For any measurable space `α`, if a vector measure `v` on `α` with values in an ordered additive commutative monoid `M` satisfies the restriction of `v` on a measurable set `i` dominates the zero vector measure on `i`, then the restriction of `v` on any subset `j` of `i` also dominates the zero vector measure on `j`.
|
MeasureTheory.VectorMeasure.empty
theorem MeasureTheory.VectorMeasure.empty :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
(v : MeasureTheory.VectorMeasure α M), ↑v ∅ = 0
This theorem states that for any given measure space `α` which is equipped with a measurable space structure `m`, and any topological additive commutative monoid `M`, the vector measure `v` of the empty set is equal to zero. It's a property in measure theory which indicates that an empty set doesn't contribute to the value of a measure, in this case a vector measure.
More concisely: For any measure space `α` with measure `m` and any topological additive commutative monoid `M`, the vector measure `v` of the empty set is the zero vector.
|
MeasureTheory.VectorMeasure.map_apply
theorem MeasureTheory.VectorMeasure.map_apply :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {M : Type u_3}
[inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {f : α → β},
Measurable f → ∀ {s : Set β}, MeasurableSet s → ↑(v.map f) s = ↑v (f ⁻¹' s)
This theorem, named `MeasureTheory.VectorMeasure.map_apply`, states that for all types `α`, `β` and `M`, given a measurable space over `α` and `β`, an addition-commutative monoid over `M`, and a topological space over `M`, for any vector measure `v` of type `α` to `M`, and any function `f` from `α` to `β` that is measurable, then for any set `s` of type `β` that is measurable, the measure of the set `s` under the map of the vector measure `v` by the function `f` is equal to the measure of the preimage of the set `s` under the function `f` with respect to the vector measure `v`. In mathematical terms, for a measurable function `f: α → β` and a measurable set `s ⊆ β`, the measure of `s` under the mapped measure is the same as the measure of the preimage of `s` under the original measure.
More concisely: For any measurable function between measurable spaces and any measurable set, the measure of the set under the mapped measure is equal to the measure of the preimage of the set under the original measure.
|
MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
[inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
{v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
(∀ ⦃s : Set α⦄, MeasurableSet s → ↑w s = 0 → ↑v s = 0) → v.AbsolutelyContinuous w
The theorem `MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk` states that for any measurable space `α`, given vector measures `v` and `w` whose values lie in topological add-commutative monoids `M` and `N` respectively, if for every measurable set `s`, the measure of `s` under `w` being zero implies the measure of `s` under `v` is also zero, then the vector measure `v` is absolutely continuous with respect to the vector measure `w`. In terms of measure theory, this means that `v` disregards sets that `w` considers negligible.
More concisely: If for every measurable set in a measurable space, the measure of the set under `w` being zero implies the measure of the set under `v` is also zero, then `v` is absolutely continuous with respect to `w`.
|
MeasureTheory.VectorMeasure.m_iUnion
theorem MeasureTheory.VectorMeasure.m_iUnion :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
(v : MeasureTheory.VectorMeasure α M) {f : ℕ → Set α},
(∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Disjoint on f) → HasSum (fun i => ↑v (f i)) (↑v (⋃ i, f i))
This theorem, `MeasureTheory.VectorMeasure.m_iUnion`, states that for all measurable spaces `α` and all types `M` where `M` has an additive commutative monoid structure and a topological structure, and given a vector measure `v` over `α` and `M`, and a sequence of sets `f` indexed by natural numbers, if each of the sets `f i` is measurable and the sets are pairwise disjoint, then the sum of the vector measure `v` over each individual set `f i` is equal to the vector measure `v` over the union of all the sets `f i`. In other words, the total measure of a countable collection of disjoint measurable sets is the sum of the measures of each set. This corresponds to the property of σ-additivity in measure theory.
More concisely: For any measurable space, if a vector measure is defined on a countable collection of pairwise disjoint, measurable sets, then the vector measure of their union equals the sum of the measures of each individual set.
|
MeasureTheory.VectorMeasure.ext
theorem MeasureTheory.VectorMeasure.ext :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
{s t : MeasureTheory.VectorMeasure α M}, (∀ (i : Set α), MeasurableSet i → ↑s i = ↑t i) → s = t
The theorem `MeasureTheory.VectorMeasure.ext` states that for any measurable space `α` and any type `M` that has an additive commutative monoid structure and a topological space structure, two vector measures `s` and `t` on `α` with values in `M` are equal if and only if they assign the same measure to every measurable set `i`. In other words, if for every measurable set `i`, the measure of `i` according to `s` is equal to the measure of `i` according to `t`, then `s` and `t` are the same vector measure.
More concisely: Two vector measures on a measurable space with values in an additive commutative monoid and topological space have equal values on all measurable sets if and only if they are equal.
|
MeasureTheory.VectorMeasure.ennrealToMeasure_apply
theorem MeasureTheory.VectorMeasure.ennrealToMeasure_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α ENNReal} {s : Set α},
MeasurableSet s → ↑↑v.ennrealToMeasure s = ↑v s
This theorem states that for any type `α`, given a measurable space `m` over `α`, a vector measure `v` over the extended nonnegative real numbers (`ENNReal`), and a set `s` of type `α`, if `s` is a measurable set, then the measure of `s` under the measure corresponding to the vector measure `v` is equal to the vector measure `v` of the set `s`. In mathematical terms, we could write this as: if `s` is a measurable set in a measurable space `M`, and `v` is a vector measure over `[0, ∞]`, then the measure under `v` of the set `s` is equal to `v(s)`.
More concisely: For any measurable space `(α, M)`, measurable set `s` ∋ο M, and vector measure `v` over `[0, ∞]`, `v(s) = ∫x ∈ s d(v x)`.
|
MeasureTheory.VectorMeasure.of_union
theorem MeasureTheory.VectorMeasure.of_union :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
[inst_2 : T2Space M] {v : MeasureTheory.VectorMeasure α M} {A B : Set α},
Disjoint A B → MeasurableSet A → MeasurableSet B → ↑v (A ∪ B) = ↑v A + ↑v B
The theorem `MeasureTheory.VectorMeasure.of_union` states that for any type `α` with a associated measurable space `m`, a type `M` which is an additive commutative monoid as well as a topological space, and a T2 (Hausdorff) space, given a vector measure `v` over `α` with values in `M`, and two disjoint sets `A` and `B` that are both measurable, the measure of the union of `A` and `B` with respect to the vector measure `v` is equal to the sum of the measures of `A` and `B` individually. This is a generalization of the principle that the measure of the union of two disjoint sets is the sum of their individual measures.
More concisely: For any measurable spaces `(α, m)`, additive commutative monoid and T2 space `M`, vector measure `v` over `α` with values in `M`, and disjoint measurable sets `A` and `B`, the measure of `A ∪ B` is equal to `v(A) + v(B)`.
|
MeasureTheory.VectorMeasure.trim_measurableSet_eq
theorem MeasureTheory.VectorMeasure.trim_measurableSet_eq :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
{n : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α M} (hle : m ≤ n) {i : Set α},
MeasurableSet i → ↑(v.trim hle) i = ↑v i
This theorem states that for any type `α`, given two measure spaces `m` and `n` on `α`, a vector measure `v` of `α` into a type `M` (which is an additive commutative monoid and has a topology), and a subset `i` of `α`, if `m` is less than or equal to `n` (in the sense of being a sub-σ-algebra), and if `i` is a measurable set (in the ambient measure space on `α`), then the restriction of the vector measure `v` onto the sub-σ-algebra `m` evaluated on `i` is equal to the original vector measure `v` evaluated on `i`. In mathematical terms, this theorem asserts that restricting a vector measure to a sub-σ-algebra does not change its values on measurable sets.
More concisely: For any measure spaces `m ≤ n` on type `α`, any measurable subset `i` of `α`, and any additive commutative monoid-valued vector measure `v` on `α`, the restriction of `v` to `m` on `i` equals `v` on `i`.
|
MeasureTheory.VectorMeasure.MutuallySingular.symm
theorem MeasureTheory.VectorMeasure.MutuallySingular.symm :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
[inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N]
{v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
v.MutuallySingular w → w.MutuallySingular v
This theorem states that for any type `α` with a `MeasurableSpace` structure, types `M` and `N` that are additive commutative monoids and topological spaces, and any `v` and `w` which are vector measures on `α` with values in `M` and `N` respectively, if `v` and `w` are mutually singular, then `w` and `v` are also mutually singular. Mutually singular, in measure theory, means that the measures are 'completely disjoint': they do not assign positive measure to any of the same sets. The theorem says this relationship is symmetric: if `v` is mutually singular with respect to `w`, then `w` is also mutually singular with respect to `v`.
More concisely: For any measure spaces `(α, Σ, μ)` and `(α, Σ, ν)`, if `μ` and `ν` are mutually singular measure theories (i.e., there exist disjoint sets `A, B ∈ Σ` such that `μ(A) = ν(B) = 0` and `μ(C) = 0 ↔ ν(C∖B) = 0` for all `C ∈ Σ`), then `ν` is mutually singular with respect to `μ`.
|
MeasureTheory.VectorMeasure.add_apply
theorem MeasureTheory.VectorMeasure.add_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
[inst_2 : ContinuousAdd M] (v w : MeasureTheory.VectorMeasure α M) (i : Set α), ↑(v + w) i = ↑v i + ↑w i
The theorem `MeasureTheory.VectorMeasure.add_apply` states that for any type `α`, a measurable space `m` on `α`, a type `M` that is an additive commutative monoid and a topological space with continuous addition, and given two vector measures `v` and `w` on `α` with values in `M`, and a set `i` of `α`, the measure of the union of `v` and `w` applied to `i` is equal to the sum of the measure of `v` applied to `i` and the measure of `w` applied to `i`. This illustrates a fundamental property of measures, which is the additivity over disjoint sets.
More concisely: For any measurable space, additive commutative monoid valued vector measures `v` and `w` on a measurable space `(α, m)`, the measure of their union is equal to the sum of their individual measures: `∫(i: α) m (v i + w i) = ∫(i: α) m v i + ∫(i: α) m w i`.
|
MeasureTheory.VectorMeasure.restrict_zero
theorem MeasureTheory.VectorMeasure.restrict_zero :
∀ {α : Type u_1} [inst : MeasurableSpace α] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
{i : Set α}, MeasureTheory.VectorMeasure.restrict 0 i = 0
This theorem states that for any measurable space `α`, any type `M` with an additive commutative monoid structure and a topology, and any set `i` of `α`, the restriction of the zero vector measure to the set `i` is the zero vector measure. In simple terms, if we take a vector measure that assigns zero to every set and restrict it to a particular set, we still get a vector measure that assigns zero to every subset.
More concisely: For any measurable space `α`, any additive commutative monoid `M` with a topology, and any set `i` in `α`, the restriction of the zero vector measure on `M` to `i` is the zero vector measure on `i`.
|
MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le
theorem MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
[inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
(∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j) → v.restrict i ≤ w.restrict i
This theorem states that for any measurable space 'α', topological space 'M' and 'i' belonging to the set 'α', if for any measurable subset 'j' of 'i', the measure of 'j' according to vector measure 'v' is less than or equal to the measure of 'j' according to vector measure 'w', then the restriction of vector measure 'v' to the set 'i' is less than or equal to the restriction of vector measure 'w' to the set 'i'. In other words, if 'v' measures all measurable subsets of 'i' to be less than or equal to 'w', then the measure of 'i' itself according to 'v' is also less than or equal to its measure according to 'w'.
More concisely: If for all measurable subsets j of i in measurable space α, the vector measure v(j) ≤ w(j), then v(i) ≤ w(i).
|
MeasureTheory.VectorMeasure.restrict_le_restrict_iff
theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iff :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
[inst_2 : PartialOrder M] (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
MeasurableSet i → (v.restrict i ≤ w.restrict i ↔ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → ↑v j ≤ ↑w j)
This theorem states that for any types `α` and `M`, a measurable space over `α` denoted by `m`, a topological space over `M`, and an additive commutative monoid over `M` with a partial order, given vector measures `v` and `w` over `α` and `M`, and a set `i` of type `α` that is measurable, the restriction of the vector measure `v` to the set `i` is less than or equal to the restriction of the vector measure `w` to the same set if and only if for all subsets `j` of `i` that are measurable, the measure of `j` under `v` is less than or equal to the measure of `j` under `w`. In terms of measure theory, it provides a condition to compare the restrictions of two vector measures on a given measurable set.
More concisely: For measurable sets i in a measurable space over type α, and vector measures v and w over i and a topological space M with an additive commutative monoid and partial order, if the measure of every measurable subset j of i satisfies v(j) ≤ w(j), then the restriction of v to i is less than or equal to the restriction of w to i.
|
MeasureTheory.Measure.toSignedMeasure_sub_apply
theorem MeasureTheory.Measure.toSignedMeasure_sub_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : MeasureTheory.IsFiniteMeasure μ]
[inst_1 : MeasureTheory.IsFiniteMeasure ν] {i : Set α},
MeasurableSet i → ↑(μ.toSignedMeasure - ν.toSignedMeasure) i = (↑↑μ i).toReal - (↑↑ν i).toReal
This theorem states that for any type `α`, measurable space `m`, measures `μ` and `ν`, and set `i` in `α`, if `i` is a measurable set and both `μ` and `ν` are finite measures, then the value of the signed measure formed by subtracting the signed measure of `ν` from the signed measure of `μ` at set `i` is equal to the difference of the real values of `μ` and `ν` at set `i`. This effectively describes the property of difference operation in the context of signed measures.
More concisely: For any measurable sets `i` in a measurable space with finite measures `μ` and `ν`, the signed measure `μ - ν` of `i` equals the real number `μ(i) - ν(i)`.
|
MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict
theorem MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M]
[inst_1 : OrderedAddCommMonoid M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i → 0 ≤ ↑v i
The theorem `MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict` states that for any measurable space `α`, a topological space `M` that is also an ordered additive commutative monoid, a vector measure `v` over `α` and `M`, and a set `i` of `α`, if the restriction of the zero vector measure to the set `i` is less than or equal to the restriction of `v` to `i`, then the measure `v` applied to `i` is nonnegative. In other words, the restriction of a vector measure can be used to infer nonnegativity of the measure on a certain set.
More concisely: If the restriction of a vector measure over a measurable space to a set is less than or equal to the zero measure, then the measure of that set is nonnegative.
|
MeasureTheory.VectorMeasure.restrict_not_measurable
theorem MeasureTheory.VectorMeasure.restrict_not_measurable :
∀ {α : Type u_1} [inst : MeasurableSpace α] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
(v : MeasureTheory.VectorMeasure α M) {i : Set α}, ¬MeasurableSet i → v.restrict i = 0
The theorem `MeasureTheory.VectorMeasure.restrict_not_measurable` states that for any given measurable space `α`, any type `M` with an additive commutative monoid structure and a topological space structure, any vector measure `v` from `α` to `M`, and any set `i` in `α`, if the set `i` is not measurable, then the restriction of the vector measure `v` onto the set `i` is equal to the zero measure. In other words, we cannot restrict a vector measure onto a set that is not measurable; if we try to do so, we just get the zero measure.
More concisely: If `α` is a measurable space, `M` is a type with additive commutative monoid and topological space structures, `v` is a vector measure from `α` to `M`, and `i` is a non-measurable set in `α`, then `v.restrict i = ⫀m : M, ∫x : i, v x = m`.
|
MeasureTheory.VectorMeasure.neg_le_neg_iff
theorem MeasureTheory.VectorMeasure.neg_le_neg_iff :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : OrderedAddCommGroup M]
[inst_2 : TopologicalAddGroup M] (v w : MeasureTheory.VectorMeasure α M) {i : Set α},
MeasurableSet i → ((-w).restrict i ≤ (-v).restrict i ↔ v.restrict i ≤ w.restrict i)
This theorem states that for any measurable space `α`, any topological space `M` which is also an ordered additive commutative group and a topological additive group, and any two vector measures `v` and `w` from `α` to `M`, as well as any set `i` in `α` that is measurable, the restriction of the negation of `w` to `i` is less than or equal to the restriction of the negation of `v` to `i` if and only if the restriction of `v` to `i` is less than or equal to the restriction of `w` to `i`.
In mathematical terms, it says that for all measurable set `i`, $(-w)|_i \leq (-v)|_i$ if and only if $v|_i \leq w|_i$, where $v|_i$ and $w|_i$ denote the restrictions of the vector measures `v` and `w` to the set `i`, respectively.
More concisely: For any measurable sets `i` in a measurable space `α`, the negation of vector measure `w` restricted to `i` is less than or equal to the negation of vector measure `v` restricted to `i` if and only if `v` restricted to `i` is less than or equal to `w` restricted to `i`.
|
MeasureTheory.VectorMeasure.not_measurable
theorem MeasureTheory.VectorMeasure.not_measurable :
∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
(v : MeasureTheory.VectorMeasure α M) {i : Set α}, ¬MeasurableSet i → ↑v i = 0
The theorem `MeasureTheory.VectorMeasure.not_measurable` states that for any type `α`, given a measurable space `m` on `α`, any type `M` which is a commutative additive monoid and also a topological space, and any vector measure `v` from `α` to `M`, if a set `i` of type `α` is not a measurable set, then the application of the vector measure `v` to this set `i` is equal to zero. In other words, the vector measure of a non-measurable set is zero.
More concisely: If `i` is a non-measurable subset of a measurable space `m` on type `α`, then the vector measure `v` from `α` to the commutative additive monoid and topological space `M` of any measurable function `v` is equal to the zero vector when applied to `i`.
|