MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative
theorem MeasureTheory.SignedMeasure.of_symmDiff_compl_positive_negative :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i j : Set α},
MeasurableSet i →
MeasurableSet j →
MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧
MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ →
MeasureTheory.VectorMeasure.restrict 0 j ≤ MeasureTheory.VectorMeasure.restrict s j ∧
MeasureTheory.VectorMeasure.restrict s jᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 jᶜ →
↑s (symmDiff i j) = 0 ∧ ↑s (symmDiff iᶜ jᶜ) = 0
This theorem states that for any measurable space 'α' and any signed measure 's' on 'α', given two measurable sets 'i' and 'j', if the restriction of the zero measure to 'i' is less than or equal to the restriction of the measure 's' to 'i', and the restriction of measure 's' to the complement of 'i' is less than or equal to the restriction of the zero measure to the complement of 'i', and similarly for set 'j', then the measure 's' of the symmetric difference of 'i' and 'j', and the measure 's' of the symmetric difference of the complements of 'i' and 'j' are both zero.
In mathematical terms, the symmetric difference of two sets 'A' and 'B' is given by '(A \ B) U (B \ A)', and a Hahn decomposition of a signed measure is a partition of the space into two measurable sets such that the measure is positive on one set and negative on the complement. The theorem then states that the symmetric difference of two such decompositions has zero measure.
More concisely: Given any measurable spaces 'α' and signed measure 's', if the restrictions of 's' to the measurable sets 'i' and 'j', and their complements, satisfy the given conditions, then the measures of the symmetric differences between 'i' and 'j' and their complements have zero measure.
|
MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos
theorem MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos :
∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
↑s i < 0 →
∃ j,
MeasurableSet j ∧
j ⊆ i ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ ↑s j < 0
The theorem `MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos` states that for any measurable space `α`, and any signed measure `s` on `α`, if a set `i` has a negative measure under `s`, then there exists a measurable subset `j` of `i` such that the restriction of the measure `s` to `j` is less than or equal to the restriction of the zero measure to `j`, and the measure of `j` under `s` is negative. In simpler terms, if a set has a negative measure, it must contain a measurable subset that also has a negative measure.
More concisely: If a measurable set in a measurable space has a negative measure under a signed measure, then there exists a measurable subset with a negative measure and less than or equal measure under the restriction of the signed measure to that subset.
|
MeasureTheory.SignedMeasure.exists_compl_positive_negative
theorem MeasureTheory.SignedMeasure.exists_compl_positive_negative :
∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
∃ i,
MeasurableSet i ∧
MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧
MeasureTheory.VectorMeasure.restrict s iᶜ ≤ MeasureTheory.VectorMeasure.restrict 0 iᶜ
This theorem is an alternative formulation of the Hahn decomposition theorem using set complements. It states that for every signed measure `s` on a measurable space `α`, there exists a measurable set `i` such that the restriction of the zero vector measure to `i` is less than or equal to the restriction of `s` to `i`, and the restriction of `s` to the complement of `i` is less than or equal to the restriction of the zero vector measure to the complement of `i`. In other words, `s` is positive on `i` and negative on `i` complement.
More concisely: For every signed measure `s` on a measurable space `α`, there exists a measurable subset `i` such that `s(A) ≤ 0` for all `A ∉ i` and `s(A) ≥ 0` for all `A ∋ i`.
|
MeasureTheory.SignedMeasure.exists_isCompl_positive_negative
theorem MeasureTheory.SignedMeasure.exists_isCompl_positive_negative :
∀ {α : Type u_1} [inst : MeasurableSpace α] (s : MeasureTheory.SignedMeasure α),
∃ i j,
MeasurableSet i ∧
MeasureTheory.VectorMeasure.restrict 0 i ≤ MeasureTheory.VectorMeasure.restrict s i ∧
MeasurableSet j ∧
MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ IsCompl i j
This theorem is known as the Hahn decomposition theorem. It states that for any signed measure `s` defined on a measurable space `α`, there exist two complementary measurable sets `i` and `j` such that `i` is positive and `j` is negative with respect to the measure `s`. In more detail, the measure of set `i` with respect to the zero measure is less than or equal to the measure of `i` with respect to `s`, implying that `i` is positive. Similarly, the measure of `j` with respect to `s` is less than or equal to the measure of `j` with respect to the zero measure, implying that `j` is negative. The sets `i` and `j` are complementary, meaning that each element of `α` is in exactly one of `i` or `j`, and the union of `i` and `j` covers the whole of `α`.
More concisely: Given any signed measure `s` on a measurable space `α`, there exist complementary measurable sets `i` and `j` such that `i` is a positive set with respect to `s` (i.e., the measure of `i` with respect to the zero measure is less than or equal to its measure with respect to `s`) and `j` is a negative set with respect to `s` (i.e., the measure of `j` with respect to `s` is less than or equal to its measure with respect to the zero measure), and the union of `i` and `j` equals `α`.
|