MeasureTheory.Measure.sub_eq_zero_of_le
theorem MeasureTheory.Measure.sub_eq_zero_of_le :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ ≤ ν → μ - ν = 0
This is a theorem in measure theory. It states that for any type `α`, any measurable space `m` of that type, and any two measures `μ` and `ν` on that measurable space, if `μ` is less than or equal to `ν`, then the difference between `μ` and `ν` is zero. In other words, in the context of measures, you can't subtract a larger measure from a smaller one; doing so will always result in zero.
More concisely: For any measurable spaces `(α, m)` and measures `μ` and `ν` on `m` with `μ ≤ ν`, we have `μ - ν = 0`.
|
MeasureTheory.Measure.sub_apply
theorem MeasureTheory.Measure.sub_apply :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} {s : Set α}
[inst : MeasureTheory.IsFiniteMeasure ν], MeasurableSet s → ν ≤ μ → ↑↑(μ - ν) s = ↑↑μ s - ↑↑ν s
This theorem, referred to as `MeasureTheory.Measure.sub_apply`, states that for a given type `α`, a measurable space `m` of type `α`, two measures `μ` and `ν` of the measurable space, and a set `s` of type `α`, if `ν` is a finite measure and the set `s` is measurable, then if `ν` is less than or equal to `μ`, the measure of the set `s` with respect to the measure `μ - ν` is equal to the measure of `s` with respect to `μ` minus the measure of `s` with respect to `ν`. This theorem is especially useful under specific conditions when there is knowledge of when `μ` is greater or equal to `ν` or `ν` is less than or equal to `μ`.
More concisely: For measurable sets `s` in a measurable space `m` with finite measures `ν` less than or equal to `μ` on `m`, the measure of `s` with respect to `μ - ν` equals the difference of the measures of `s` with respect to `μ` and `ν`.
|