Theorems · Definition · measure theory
MeasureTheory.JordanDecomposition.negPart
{α : Type u_2} → [inst : MeasurableSpace α] → MeasureTheory.JordanDecomposition α → MeasureTheory.Measure αNegative part of the Jordan decomposition
- Cited by
- 44 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- 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.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
- MeasureTheory.JordanDecompositionstatement and proof · cited by 40
Cited by50
Results whose statement or proof uses this declaration.
- MeasureTheory.SignedMeasure.rnDerivproof · cited by 13
- MeasureTheory.SignedMeasure.singularPartproof · cited by 13
- MeasureTheory.JordanDecomposition.toSignedMeasureproof · cited by 13
- MeasureTheory.SignedMeasure.totalVariationproof · cited by 13
- MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecompositionproof · cited by 10
- MeasureTheory.SignedMeasure.integrable_rnDerivproof · cited by 9
- MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eqproof · cited by 6
- MeasureTheory.JordanDecomposition.toSignedMeasure_injectiveproof · cited by 6
- MeasureTheory.SignedMeasure.toJordanDecomposition_specstatement · cited by 5
- MeasureTheory.JordanDecomposition.smul_negPartstatement · cited by 5
- MeasureTheory.SignedMeasure.null_of_totalVariation_zeroproof · cited by 3
- MeasureTheory.SignedMeasure.rnDeriv_defstatement · cited by 3