Theorems · Definition · measure theory
MeasureTheory.JordanDecomposition.toSignedMeasure
{α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.JordanDecomposition α → MeasureTheory.SignedMeasure αThe signed measure associated with a Jordan decomposition.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 175 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- MeasurableSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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.SignedMeasurestatement · cited by 108
- MeasureTheory.JordanDecomposition.negPartproof · cited by 44
- MeasureTheory.JordanDecomposition.posPartproof · cited by 43
- MeasureTheory.JordanDecompositionstatement and proof · cited by 40
- MeasureTheory.Measure.toSignedMeasureproof · cited by 36
Cited by14
Results whose statement or proof uses this declaration.
- MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecompositionstatement · cited by 10
- MeasureTheory.JordanDecomposition.toSignedMeasure_injectivestatement and proof · cited by 6
- MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eqproof · cited by 2
- MeasureTheory.SignedMeasure.toJordanDecompositionEquivproof · cited by 2
- MeasureTheory.SignedMeasure.toJordanDecomposition_eqstatement and proof · cited by 1
- MeasureTheory.JordanDecomposition.toJordanDecomposition_toSignedMeasurestatement and proof · cited by 1
- MeasureTheory.JordanDecomposition.toSignedMeasure_negstatement and proof · cited by 1
- MeasureTheory.JordanDecomposition.toSignedMeasure_smulstatement and proof · cited by 1
- MeasureTheory.JordanDecomposition.toSignedMeasure_zerostatement · cited by 1
- MeasureTheory.Measure.jordanDecompositionOfToSignedMeasureSub_toSignedMeasurestatement · cited by 1
- MeasureTheory.JordanDecomposition.exists_compl_positive_negativestatement and proof · cited by 1
- MeasureTheory.SignedMeasure.singularPart_totalVariationproof · cited by 1