Theorems · Definition · measure theory
MeasureTheory.SignedMeasure.totalVariation
{α : Type u_1} → [inst : MeasurableSpace α] → MeasureTheory.SignedMeasure α → MeasureTheory.Measure αThe total variation of a signed measure.
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 176 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.Measurestatement · cited by 10,939
- MeasureTheory.SignedMeasurestatement and proof · cited by 108
- MeasureTheory.JordanDecomposition.negPartproof · cited by 44
- MeasureTheory.JordanDecomposition.posPartproof · cited by 43
- MeasureTheory.SignedMeasure.toJordanDecompositionproof · cited by 34
Cited by13
Results whose statement or proof uses this declaration.
- MeasureTheory.SignedMeasure.null_of_totalVariation_zerostatement and proof · cited by 3
- MeasureTheory.SignedMeasure.mutuallySingular_ennreal_iffstatement and proof · cited by 2
- MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eqproof · cited by 2
- MeasureTheory.SignedMeasure.absolutelyContinuous_ennreal_iffstatement and proof · cited by 1
- MeasureTheory.SignedMeasure.enorm_le_totalVariationstatement and proof · cited by 1
- MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iffstatement and proof · cited by 1
- MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iffstatement · cited by 1
- MeasureTheory.SignedMeasure.norm_le_totalVariationstatement and proof · cited by 1
- MeasureTheory.SignedMeasure.singularPart_totalVariationstatement · cited by 1
- MeasureTheory.SignedMeasure.totalVariation_eq_variationstatement · cited by 0
- MeasureTheory.SignedMeasure.totalVariation_negstatement · cited by 0
- MeasureTheory.SignedMeasure.totalVariation_zerostatement · cited by 0