MeasureTheory.Measure.MutuallySingular.add_left_iff
theorem MeasureTheory.Measure.MutuallySingular.add_left_iff :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν : MeasureTheory.Measure α},
(μ₁ + μ₂).MutuallySingular ν ↔ μ₁.MutuallySingular ν ∧ μ₂.MutuallySingular ν
The theorem `MeasureTheory.Measure.MutuallySingular.add_left_iff` states that for any type `α`, any measurable space `m0` of type `α`, and any three measures `μ₁`, `μ₂`, `ν` of type `α`, the measure `μ₁ + μ₂` is mutually singular with the measure `ν` if and only if both `μ₁` and `μ₂` are mutually singular with `ν`. In mathematical terms, two measures are said to be mutually singular if there exists a measurable set such that one measure assigns it a measure of zero and the other measure assigns its complement a measure of zero.
More concisely: For any measurable spaces `(α, m0)` and measures `μ₁, μ₂, ν` on `α`, `μ₁ + μ₂` is mutually singular with `ν` if and only if both `μ₁` and `μ₂` are mutually singular with `ν`.
|
MeasureTheory.Measure.MutuallySingular.symm
theorem MeasureTheory.Measure.MutuallySingular.symm :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
ν.MutuallySingular μ → μ.MutuallySingular ν
The theorem `MeasureTheory.Measure.MutuallySingular.symm` states that for any type `α` and `m0` being a measurable space associated with `α`, if two measures `μ` and `ν` are mutually singular in the sense that there exists a measurable set such that the measure of that set by `ν` is zero and the measure of the complement of the set by `μ` is also zero, then the mutually singularity property is symmetric; meaning that, `μ` and `ν` can be swapped and they will still be mutually singular.
More concisely: If measures `μ` and `ν` on measurable space `(α, m0)` are mutually singular, then swapping `μ` and `ν` preserves the mutually singularity property.
|
MeasureTheory.Measure.MutuallySingular.mono_ac
theorem MeasureTheory.Measure.MutuallySingular.mono_ac :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ₁ μ₂ ν₁ ν₂ : MeasureTheory.Measure α},
μ₁.MutuallySingular ν₁ → μ₂.AbsolutelyContinuous μ₁ → ν₂.AbsolutelyContinuous ν₁ → μ₂.MutuallySingular ν₂
The theorem `MeasureTheory.Measure.MutuallySingular.mono_ac` states that for any type `α` and any measurable space `m0` over `α`, if we have two pairs of measures, `(μ₁, ν₁)` and `(μ₂, ν₂)`, such that `μ₁` and `ν₁` are mutually singular, `μ₂` is absolutely continuous with respect to `μ₁`, and `ν₂` is absolutely continuous with respect to `ν₁`, then `μ₂` and `ν₂` are also mutually singular.
In terms of measure theory, a pair of measures is said to be mutually singular if there exists a measurable set such that one measure is zero on this set and the other is zero on the complement of this set. A measure is absolutely continuous with respect to another measure if whenever the latter measure assigns zero to a set, so does the former. Thus, the theorem is essentially saying that the property of mutual singularity is preserved under absolute continuity.
More concisely: If two measures `μ₁` and `ν₁` are mutually singular over a measurable space `m0`, and `μ₂` is absolutely continuous with respect to `μ₁` while `ν₂` is absolutely continuous with respect to `ν₁`, then `μ₂` and `ν₂` are mutually singular.
|
MeasureTheory.Measure.MutuallySingular.zero_right
theorem MeasureTheory.Measure.MutuallySingular.zero_right :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.MutuallySingular 0
The theorem `MeasureTheory.Measure.MutuallySingular.zero_right` states that for any measure space `α` and any measure `μ` defined on this space, the measure `μ` and the zero measure are mutually singular. In the context of measure theory, two measures are said to be mutually singular if there exists a measurable set such that one measure is zero on this set and the other measure is zero on the complement of this set. In this case, any measure `μ` and the zero measure are mutually singular because you can consider the whole set as the measurable set where the zero measure is zero, and consequently, the `μ` measure is zero at the complement of the whole set which is the empty set.
More concisely: For any measure space and measure, the measure and the zero measure are mutually singular.
|
MeasureTheory.Measure.MutuallySingular.smul
theorem MeasureTheory.Measure.MutuallySingular.smul :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (r : ENNReal),
ν.MutuallySingular μ → (r • ν).MutuallySingular μ
This theorem states that for any measure space `α` with its measurable sets `m0`, any two measures `μ` and `ν`, and an extended nonnegative real number `r`, if the measures `ν` and `μ` are mutually singular, then the measures `r` times `ν` (denoted as `r • ν`) and `μ` are also mutually singular. In mathematical terms, this means that if there exists a measurable set `s` such that `ν(s) = 0` and `μ(sᶜ) = 0`, then there also exists a measurable set such that `(r • ν)(s) = 0` and `μ(sᶜ) = 0`, where `sᶜ` represents the complement of set `s`.
More concisely: If measures `μ` and `ν` on measurable space `α` are mutually singular, then `r` times `ν` and `μ` are also mutually singular for any extended nonnegative real number `r`.
|
MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet
theorem MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (h : μ.MutuallySingular ν),
MeasurableSet h.nullSet
The theorem `MeasureTheory.Measure.MutuallySingular.measurableSet_nullSet` asserts that for any two measures `μ` and `ν` over a measurable space `α`, if `μ` and `ν` are mutually singular, then the null set associated with this mutual singularity is a measurable set. In other words, there exists a set that can be measured such that it is null under the measure `μ`, and its complement is null under the measure `ν`.
More concisely: If measures `μ` and `ν` over measurable space `α` are mutually singular, then their associated null sets are measurable.
|
MeasureTheory.Measure.MutuallySingular.zero_left
theorem MeasureTheory.Measure.MutuallySingular.zero_left :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α},
MeasureTheory.Measure.MutuallySingular 0 μ
The theorem `MeasureTheory.Measure.MutuallySingular.zero_left` states that for any type `α` equipped with a measurable space structure `m0` and any measure `μ` on that type, the zero measure and the measure `μ` are mutually singular. In the context of measure theory, this means that there exists a measurable set `s` such that the zero measure of `s` is 0 (which is always true for the zero measure) and the measure `μ` of the complement of `s` is also 0.
More concisely: For any measurable space `(α, m0)` and measure `μ` on `α`, the zero measure and `μ` are mutually singular, i.e., there exists a measurable set `s` with `μ(s^c) = 0` and `m0(s) = 0`.
|
MeasureTheory.Measure.MutuallySingular.add_left
theorem MeasureTheory.Measure.MutuallySingular.add_left :
∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν₁ ν₂ : MeasureTheory.Measure α},
ν₁.MutuallySingular μ → ν₂.MutuallySingular μ → (ν₁ + ν₂).MutuallySingular μ
This theorem, `MeasureTheory.Measure.MutuallySingular.add_left`, asserts that if two measures `ν₁` and `ν₂` are each mutually singular with a measure `μ` in a given measurable space, then the sum of `ν₁` and `ν₂` is also mutually singular with `μ`. In terms of measure theory, two measures are said to be mutually singular if there exists a measurable set for which one measure is zero while the complement of the set is zero for the other measure. So, the theorem essentially states that the property of mutual singularity with respect to a given measure is preserved under the addition of the mutually singular measures.
More concisely: If measures `ν₁` and `ν₂` are mutually singular with measure `μ` in a measurable space, then `ν₁ + ν₂` is mutually singular with `μ`.
|