Theorems · Inductive type · measure theory
MeasureTheory.JordanDecomposition
(α : Type u_2) → [MeasurableSpace α] → Type u_2
A Jordan decomposition of a measurable space is a pair of mutually singular, finite measures.
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
Cited by52
Results whose statement or proof uses this declaration.
- MeasureTheory.JordanDecomposition.negPartstatement and proof · cited by 44
- MeasureTheory.JordanDecomposition.posPartstatement and proof · cited by 43
- MeasureTheory.SignedMeasure.toJordanDecompositionstatement · cited by 34
- MeasureTheory.JordanDecomposition.toSignedMeasurestatement and proof · cited by 13
- MeasureTheory.JordanDecomposition.toSignedMeasure_injectivestatement and proof · cited by 6
- MeasureTheory.JordanDecomposition.real_smul_defstatement and proof · cited by 5
- MeasureTheory.JordanDecomposition.smul_negPartstatement and proof · cited by 5
- MeasureTheory.JordanDecomposition.smul_posPartstatement and proof · cited by 5
- MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSubstatement · cited by 5
- MeasureTheory.JordanDecomposition.mutuallySingularstatement and proof · cited by 3
- MeasureTheory.SignedMeasure.toJordanDecomposition_negstatement · cited by 3
- MeasureTheory.JordanDecomposition.neg_negPartstatement and proof · cited by 3