Theorems · Definition · measure theory
MeasureTheory.Measure.singularPart
{α : Type u_2} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → MeasureTheory.Measure αIf a pair of measures HaveLebesgueDecomposition, then singularPart chooses the
measure from HaveLebesgueDecomposition, otherwise it returns the zero measure. For sigma-finite
measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).
- Cited by
- 71 results in Mathlib
- Foundations
- Depth 207 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
Cited by72
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.haveLebesgueDecomposition_addstatement · cited by 35
- MeasureTheory.Measure.withDensity_rnDeriv_eqproof · cited by 31
- MeasureTheory.Measure.mutuallySingular_singularPartstatement · cited by 27
- MeasureTheory.SignedMeasure.singularPartproof · cited by 13
- MeasureTheory.Measure.withDensity_rnDeriv_leproof · cited by 9
- MeasureTheory.Measure.rnDeriv_add'proof · cited by 8
- MeasureTheory.Measure.singularPart_lestatement and proof · cited by 7
- MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eqproof · cited by 6
- MeasureTheory.Measure.eq_singularPartstatement and proof · cited by 6
- MeasureTheory.Measure.rnDeriv_selfproof · cited by 6
- MeasureTheory.Measure.haveLebesgueDecomposition_specstatement · cited by 6
- MeasureTheory.Measure.singularPart_defstatement · cited by 5