MeasureTheory.SignedMeasure.subset_positive_null_set
theorem MeasureTheory.SignedMeasure.subset_positive_null_set :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v w : Set α},
MeasurableSet u →
MeasurableSet v →
MeasurableSet w →
MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u →
↑s w = 0 → w ⊆ u → v ⊆ w → ↑s v = 0
The theorem `MeasureTheory.SignedMeasure.subset_positive_null_set` states that for any type `α` equipped with a `MeasurableSpace` structure and a `SignedMeasure` `s` on `α`, given three sets `u`, `v`, `w` which are all measurable, if the restriction of the zero measure to `u` is less than or equal to the restriction of `s` to `u`, and if `w` is a null-set (i.e., `s` measures `w` as zero) with `w` being a subset of `u` and `v` being a subset of `w`, then `s` measures `v` as zero. In other words, a subset of a null-set, which itself is a subset of a positive set, has zero measure.
More concisely: If `u` is a measurable set in a measurable space `α` with signed measure `s`, `w` is a null-set (i.e., `s(w) = 0`) that is a subset of a measurable set `v` with `s(u) >= s(u∣_�emptyset)` and `w` is a subset of `u`, then `s(v) = 0`.
|
MeasureTheory.SignedMeasure.toJordanDecomposition_neg
theorem MeasureTheory.SignedMeasure.toJordanDecomposition_neg :
∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
(-s).toJordanDecomposition = -s.toJordanDecomposition
This theorem states that for any measurable space `α` and for any signed measure `s` on that space, the Jordan Decomposition of the negation of `s` is equal to the negation of the Jordan Decomposition of `s`. In other words, negating a signed measure and then finding its Jordan Decomposition is the same as first finding the Jordan Decomposition and then negating it. This property is akin to the distributive law in algebra.
More concisely: For any measurable space `α` and signed measure `s` on `α`, the negated Jordan Decomposition of `s` is equal to the Jordan Decomposition of the negation of `s`: `-(jordan_decomp s) = jordan_decomp (-s)`.
|
MeasureTheory.JordanDecomposition.smul_negPart
theorem MeasureTheory.JordanDecomposition.smul_negPart :
∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal),
(r • j).negPart = r • j.negPart
The theorem `MeasureTheory.JordanDecomposition.smul_negPart` states that for any measurable space `α`, any Jordan decomposition `j` of `α`, and any nonnegative real number `r`, the negative part of `r` scaled by `j` is equal to `r` scaled by the negative part of `j`. In other words, scaling a Jordan decomposition and then taking the negative part is the same as first taking the negative part and then scaling. This is a property of scalar multiplication and the negPart operation in the context of a Jordan decomposition in measure theory.
More concisely: For any measurable space `α`, Jordan decomposition `j`, and nonnegative real number `r`, `r * j.negPart = j.negPart * r`.
|
MeasureTheory.JordanDecomposition.real_smul_def
theorem MeasureTheory.JordanDecomposition.real_smul_def :
∀ {α : Type u_1} [inst : MeasurableSpace α] (r : ℝ) (j : MeasureTheory.JordanDecomposition α),
r • j = if 0 ≤ r then r.toNNReal • j else -((-r).toNNReal • j)
This theorem, from measure theory's Jordan Decomposition, defines the operation of real number scalar multiplication on a Jordan decomposition. For any measurable space `α`, real number `r`, and Jordan decomposition `j` of `α`, scalar multiplication of `j` by `r` (`r • j`) is defined as follows: if `r` is non-negative, then it's the multiplication of `j` by the non-negative real number reinterpretation of `r` (`Real.toNNReal r • j`), otherwise, it's the negative of multiplication of `j` by the non-negative real number reinterpretation of `-r` (`-(Real.toNNReal (-r) • j)`). The function `Real.toNNReal` reinterprets a real number as a non-negative real number, returning `0` if the number is less than `0`.
More concisely: For any measurable space `α`, real number `r`, and Jordan decomposition `j` of `α`, the scalar multiplication `r • j` is defined as `Real.toNNReal r • j` if `r` is non-negative, and `-(Real.toNNReal (-r) • j)` otherwise.
|
MeasureTheory.SignedMeasure.toJordanDecomposition.proof_1
theorem MeasureTheory.SignedMeasure.toJordanDecomposition.proof_1 :
∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
MeasurableSet ⋯.choose ∧
MeasureTheory.VectorMeasure.restrict 0 ⋯.choose ≤ MeasureTheory.VectorMeasure.restrict s ⋯.choose ∧
MeasureTheory.VectorMeasure.restrict s ⋯.chooseᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 ⋯.chooseᶜ
This theorem states that for any signed measure `s` on a measurable space `α`, there exists a measurable set (specifically, the one extracted by `Exists.choose`) with the following properties:
1. The restriction of the zero vector measure to this set is less than or equal to the restriction of `s` to the same set.
2. The restriction of `s` to the complement of this set is less than or equal to the restriction of the zero vector measure to the same complement set.
In other words, this theorem is establishing a particular property of a specific measurable set in relation to the provided signed measure and the zero vector measure.
More concisely: For any signed measure `s` on a measurable space, there exists a measurable set such that the restriction of `s` to the set is less than or equal to the restriction of the zero measure to the same set, and the reverse inequality holds for their complements.
|
MeasureTheory.JordanDecomposition.toSignedMeasure_injective
theorem MeasureTheory.JordanDecomposition.toSignedMeasure_injective :
∀ {α : Type u_1} [inst : MeasurableSpace α], Function.Injective MeasureTheory.JordanDecomposition.toSignedMeasure
The theorem states that the Jordan decomposition of a signed measure is unique. In other words, in the context of a measurable space, the function `MeasureTheory.JordanDecomposition.toSignedMeasure` is injective, which means that given any two Jordan decompositions, if their associated signed measures are the same, it implies that the two Jordan decompositions themselves are identical. This reflects that each signed measure has a unique Jordan decomposition.
More concisely: The Jordan decomposition of a signed measure is unique. That is, if two measures have the same Jordan decomposition, then they are equal.
|
MeasureTheory.JordanDecomposition.neg_negPart
theorem MeasureTheory.JordanDecomposition.neg_negPart :
∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α), (-j).negPart = j.posPart
The theorem `MeasureTheory.JordanDecomposition.neg_negPart` states that for all types `α` that have an instance of the `MeasurableSpace` type class, and for all Jordan decompositions `j` of measures on `α`, the negative part of the negation of `j` is equal to the positive part of `j`. In other words, for any measurable space and any Jordan decomposition of measures on that space, the "negative of the negative part" is equivalent to the "positive part".
More concisely: For any measurable space with a Jordan decomposition of measures, the negative of the negative measure part is equal to the positive measure part.
|
MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition
theorem MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition :
∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
s.toJordanDecomposition.toSignedMeasure = s
**The Jordan Decomposition Theorem**: In the context of a measurable space `α`, this theorem states that for any given signed measure `s`, it is possible to find a pair of mutually singular measures `μ` and `ν` such that `s` can be expressed as the difference `μ - ν`. Here, `μ` and `ν` correspond to the positive and negative parts, respectively, of the Jordan Decomposition of `s`. The function `MeasureTheory.JordanDecomposition.toSignedMeasure` is used to construct the signed measure associated with the Jordan Decomposition, i.e., the difference of the positive part and the negative part of the Jordan Decomposition of `s`. The theorem asserts the equality between this constructed signed measure and the original signed measure `s`.
More concisely: Given a signed measure `s` on a measurable space `α`, there exist mutually singular measures `μ` and `ν` such that `s = μ - ν`.
|
MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive
theorem MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_positive :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v : Set α},
MeasurableSet u →
MeasurableSet v →
MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u →
MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v →
↑s (symmDiff u v) = 0 → ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
This theorem states that for any measurable space `α` and any signed measure `s` on `α`, if `u` and `v` are two measurable sets such that the restrictions of the zero measure on `u` and `v` are less than or equal to the restrictions of `s` on `u` and `v` respectively, then if the measure `s` of the symmetric difference of `u` and `v` is zero, it follows that the measures of the sets obtained by subtracting `v` from `u` and `u` from `v` are both zero.
In more informal terms, if two "positive" sets (measured by `s`) have a symmetric difference of zero measure, then the difference between the two sets also has zero measure.
More concisely: If two measurable sets `u` and `v` in a measurable space `α` have zero symmetric difference measure with respect to a signed measure `s`, then subtracting `v` from `u` and `u` from `v` both have zero measure with respect to `s`.
|
Mathlib.MeasureTheory.Decomposition.Jordan._auxLemma.2
theorem Mathlib.MeasureTheory.Decomposition.Jordan._auxLemma.2 :
∀ {α : Type u_1} [inst : SubtractionMonoid α] {a : α}, (-a = 0) = (a = 0)
This theorem, named `Mathlib.MeasureTheory.Decomposition.Jordan._auxLemma.2`, states that for any type `α` that has a subtraction operation (forming a subtraction monoid), for any element `a` of type `α`, the negation of `a` is equal to zero if and only if `a` itself is equal to zero. In other words, in the context of this subtraction monoid, an element is zero if and only if its negative is zero.
More concisely: For any type `α` with subtraction operation, `a` is equal to zero if and only if the negation of `a` is equal to zero.
|
MeasureTheory.JordanDecomposition.smul_posPart
theorem MeasureTheory.JordanDecomposition.smul_posPart :
∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal),
(r • j).posPart = r • j.posPart
This theorem, named 'MeasureTheory.JordanDecomposition.smul_posPart', states that for any measurable space `α`, given a Jordan Decomposition `j` of that space and a nonnegative real number `r`, the positive part of the scaled (by `r`) Jordan Decomposition `(r • j)` is equal to the scaled positive part of the original Jordan Decomposition `(r • j.posPart)`. In other words, scaling a Jordan Decomposition and taking the positive part is the same as taking the positive part first and then scaling.
More concisely: For any measurable space `α`, given a Jordan Decomposition `j` and a nonnegative real number `r`, `r • j.posPart = (r • j).posPart`.
|
MeasureTheory.JordanDecomposition.neg_posPart
theorem MeasureTheory.JordanDecomposition.neg_posPart :
∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α), (-j).posPart = j.negPart
The theorem `MeasureTheory.JordanDecomposition.neg_posPart` states that, for any measurable space `α` and any Jordan decomposition `j` of `α`, the positive part of the negation of `j` is equal to the negative part of `j`. In other words, if we decompose a measure into its positive and negative parts, negating the measure and taking the positive part gives the same result as taking the negative part of the original measure.
More concisely: For any measurable space and Jordan decomposition, the negative part of the negation of the measure is equal to the negative part of the original measure.
|
MeasureTheory.JordanDecomposition.exists_compl_positive_negative
theorem MeasureTheory.JordanDecomposition.exists_compl_positive_negative :
∀ {α : Type u_1} [inst : MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α),
∃ S,
MeasurableSet S ∧
MeasureTheory.VectorMeasure.restrict j.toSignedMeasure S ≤ MeasureTheory.VectorMeasure.restrict 0 S ∧
MeasureTheory.VectorMeasure.restrict 0 Sᶜ ≤ MeasureTheory.VectorMeasure.restrict j.toSignedMeasure Sᶜ ∧
↑↑j.posPart S = 0 ∧ ↑↑j.negPart Sᶜ = 0
This theorem states that for any given Jordan decomposition in a measurable space, there exists a set S such that:
1. S is measurable.
2. The restriction of the signed measure from the Jordan decomposition to S is less than or equal to the restriction of the zero measure to S.
3. The restriction of the zero measure to the complement of S is less than or equal to the restriction of the signed measure from the Jordan decomposition to the complement of S.
4. The positive part of the Jordan decomposition applied to S is zero.
5. The negative part of the Jordan decomposition applied to the complement of S is zero.
In essence, the theorem establishes that a Jordan decomposition provides a Hahn decomposition, which is a way of decomposing a signed measure into positive and negative components.
More concisely: Given a Jordan decomposition of a signed measure on a measurable space, there exists a measurable set S such that the signed measure restricts to zero on both S and its complement, while the positive and negative parts of the decomposition have zero measure on the complement of S and S respectively.
|
MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_negative
theorem MeasureTheory.SignedMeasure.of_diff_eq_zero_of_symmDiff_eq_zero_negative :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v : Set α},
MeasurableSet u →
MeasurableSet v →
MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u →
MeasureTheory.VectorMeasure.restrict s v ≤ MeasureTheory.VectorMeasure.restrict 0 v →
↑s (symmDiff u v) = 0 → ↑s (u \ v) = 0 ∧ ↑s (v \ u) = 0
This theorem states that given a measurable space `α` and a signed measure `s` on `α`, along with two measurable sets `u` and `v` such that the restriction of `s` to `u` and `v` respectively are both less than or equal to the zero measure, if the measure of the symmetric difference of `u` and `v` under `s` is zero, then both the difference of `u` and `v` and the difference of `v` and `u` will also have zero measure under `s`.
In more mathematical terms, it says that if $\mu(u \Delta v) = 0$ for two negative sets $u$ and $v$ (where $\mu$ is a signed measure and $\Delta$ denotes symmetric difference), then $\mu(u \setminus v) = 0$ and $\mu(v \setminus u) = 0$ (where $\setminus$ denotes set difference).
More concisely: If two measurable sets $u$ and $v$ have zero symmetric difference under a signed measure $\mu$, and both restrictions of $\mu$ to $u$ and $v$ are less than or equal to the zero measure, then the set differences $u \setminus v$ and $v \setminus u$ have zero measure under $\mu$.
|
MeasureTheory.SignedMeasure.subset_negative_null_set
theorem MeasureTheory.SignedMeasure.subset_negative_null_set :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v w : Set α},
MeasurableSet u →
MeasurableSet v →
MeasurableSet w →
MeasureTheory.VectorMeasure.restrict s u ≤ MeasureTheory.VectorMeasure.restrict 0 u →
↑s w = 0 → w ⊆ u → v ⊆ w → ↑s v = 0
This theorem states that for any measurable space `α` and any signed measure `s` on `α`, if `u`, `v`, and `w` are measurable sets such that the restriction of `s` to `u` is less than or equal to the restriction of the zero measure to `u`, `w` is a null-set (i.e., `s` assigns it a measure of zero), `w` is a subset of `u`, and `v` is a subset of `w`, then `v` is also a null-set under `s`. In simpler terms, this theorem says that if a certain measurable set `w` is contained within a negative set `u` and has measure zero, then any subset `v` of `w` will also have measure zero.
More concisely: If `u` is a measurable set containing a null set `w` (i.e., `s(u) ≤ 0` and `w` is a subset of `u`), and `v` is a subset of `w`, then `v` is also a null set (`s(v) = 0`).
|