Theorems · Definition · measure theory
MeasureTheory.SignedMeasure
(α : Type u_3) → [MeasurableSpace α] → Type (max u_3 0)
A SignedMeasure is an ℝ-vector measure.
- Cited by
- 108 results in Mathlib
- Foundations
- Depth 114 from the axioms, rests on 2,963 definitions · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.VectorMeasureproof · cited by 451
Cited by129
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.toSignedMeasurestatement · cited by 36
- MeasureTheory.SignedMeasure.toJordanDecompositionstatement and proof · cited by 34
- MeasureTheory.SignedMeasure.rnDerivstatement and proof · cited by 13
- MeasureTheory.SignedMeasure.singularPartstatement and proof · cited by 13
- MeasureTheory.JordanDecomposition.toSignedMeasurestatement · cited by 13
- MeasureTheory.SignedMeasure.totalVariationstatement and proof · cited by 13
- MeasureTheory.Measure.toSignedMeasure_apply_measurablestatement · cited by 11
- MeasureTheory.SignedMeasure.toMeasureOfZeroLEstatement and proof · cited by 11
- MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecompositionstatement and proof · cited by 10
- MeasureTheory.SignedMeasure.HaveLebesgueDecompositionstatement · cited by 10
- MeasureTheory.SignedMeasure.toMeasureOfLEZerostatement and proof · cited by 10
- MeasureTheory.SignedMeasure.integrable_rnDerivstatement and proof · cited by 9