MeasureTheory.measure_eq_zero_of_trim_eq_zero
theorem MeasureTheory.measure_eq_zero_of_trim_eq_zero :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0),
↑↑(μ.trim hm) s = 0 → ↑↑μ s = 0
The theorem `MeasureTheory.measure_eq_zero_of_trim_eq_zero` states that for any type `α`, any two measurable spaces `m` and `m0` on `α`, any measure `μ` on `α`, and any set `s` of `α`, if `m` is less than or equal to `m0` (`hm`), and if the trimmed measure of `μ` with respect to `m` is zero on `s`, then the original measure `μ` is also zero on `s`. Here, the trimming of a measure is a process that modifies the measure to make it compatible with a smaller sigma algebra.
More concisely: If `μ` is a measure on a measurable space `α`, `m` and `m0` are two measurable structures on `α` with `hm(m ≤ m0)` and the trimmed measure `μ∣m` is zero on set `s`, then `μ(s) = 0`.
|
MeasureTheory.trim_measurableSet_eq
theorem MeasureTheory.trim_measurableSet_eq :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0),
MeasurableSet s → ↑↑(μ.trim hm) s = ↑↑μ s
The theorem `MeasureTheory.trim_measurableSet_eq` states that for any type `α`, given two measurable spaces `m` and `m0` over `α`, a measure `μ` on `α`, and a set `s` of type `α`, if `m` is a sub-measurable-space of `m0` (denoted `m ≤ m0`), and if `s` is a measurable set, then the measure of `s` with respect to the trimmed measure (obtained by trimming `μ` using `m`) is equal to the measure of `s` with respect to the original measure `μ`.
In other words, trimming a measure does not change the measure of measurable sets in the original measure space.
More concisely: For any measurable spaces `m ≤ m0` over type `α`, measure `μ` on `α`, and measurable set `s` of type `α`, the trimmed measure of `s` using `m` equals the original measure of `s` with respect to `μ`.
|
MeasureTheory.Measure.trim.proof_1
theorem MeasureTheory.Measure.trim.proof_1 :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), m ≤ m0 → m ≤ μ.caratheodory
This theorem in measure theory states that for any given type `α`, any two measurable spaces `m` and `m0` over `α`, and a measure `μ` on `α`, if the measurable space `m` is a subset of the measurable space `m0`, then `m` is also a subset of the Carathéodory-measurable space associated with the measure `μ`. Here, the Carathéodory-measurable space is defined such that a set `s` is measurable if for all sets `t`, the measure of `t` equals the sum of the measures of the intersection of `t` with `s` and the difference of `t` and `s`.
More concisely: If `α` is a type, `μ` is a measure on `α`, and `m` is a measurable space over `α` that is a subset of another measurable space `m0` over `α`, then `m` is a subset of the Carathéodory-measurable space associated with `μ`.
|
MeasureTheory.sigmaFiniteTrim_mono
theorem MeasureTheory.sigmaFiniteTrim_mono :
∀ {α : Type u_1} {m m₂ m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (hm₂ : m₂ ≤ m)
[inst : MeasureTheory.SigmaFinite (μ.trim ⋯)], MeasureTheory.SigmaFinite (μ.trim hm)
This theorem states that for any type `α` and given three measurable spaces `m`, `m₂`, and `m0` on `α`, and a measure `μ` on `α`, if `m` is less than or equal to `m0` and `m₂` is less than or equal to `m`, then if the measure `μ` trimmed by the measurable space `m` (and additional parameters) is sigma-finite, it implies that the measure `μ` trimmed by the measurable space `m` alone is also sigma-finite. In other words, the sigma-finiteness of a trimmed measure is preserved under monotone functions of measurable spaces.
More concisely: If `μ` is a sigma-finite measure on a measurable space `α`, `m` and `m₂` are measurable spaces on `α` with `m ≤ m₀` and `m ≤ m₂`, then the trimmed measure `μℙm` is sigma-finite, where `μℙm` is the measure `μ` restricted to the measurable sets in `m`.
|
MeasureTheory.ae_eq_of_ae_eq_trim
theorem MeasureTheory.ae_eq_of_ae_eq_trim :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_2} {hm : m ≤ m0}
{f₁ f₂ : α → E}, (μ.trim hm).ae.EventuallyEq f₁ f₂ → μ.ae.EventuallyEq f₁ f₂
This theorem states that for any type `α`, given two measurable spaces `m` and `m0` over `α`, a measure `μ`, another type `E`, and a proof `hm` that `m` is a subset of or equal to `m0`, if two functions `f₁` and `f₂` from `α` to `E` are almost everywhere equal with respect to the filter of co-null sets of the trimmed measure `(μ.trim hm)`, then they are also almost everywhere equal with respect to the filter of co-null sets of the original measure `μ`. Here, "almost everywhere equal" is denoted by `=ᶠ[...]`, and means that `f₁` and `f₂` are equal except possibly on a set of measure zero.
More concisely: Given measurable spaces `m` and `m0` over type `α`, a measure `μ`, and a proof `hm` that `m` is a subset of or equal to `m0`, if functions `f₁` and `f₂` from `α` to `E` are almost everywhere equal with respect to the filter of co-null sets of the trimmed measure `(μ.trim hm)`, then they are also almost everywhere equal with respect to the filter of co-null sets of the original measure `μ`.
|
MeasureTheory.le_trim
theorem MeasureTheory.le_trim :
∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0),
↑↑μ s ≤ ↑↑(μ.trim hm) s
The theorem `MeasureTheory.le_trim` states that for any type `α`, any two measurable spaces `m` and `m0` over `α`, any measure `μ` over `α`, and any set `s` of type `α`, if the measurable space `m` is a subset or equal to the measurable space `m0`, then the measure of the set `s` under the measure `μ` is less than or equal to the measure of the set `s` under the trimmed measure `μ.trim hm`. The trimming operation on the measure is based on the inclusion relation between the two measurable spaces.
More concisely: For any measurable spaces `m` and `m0` over type `α`, measure `μ` over `α`, and set `s` of type `α`, if `m` is a subset or equal to `m0`, then `μ(s) ≤ μ.trim hm(s)`.
|