Theorems · Inductive type · measure theory
MeasureTheory.SignedMeasure.HaveLebesgueDecomposition
{α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.SignedMeasure α → MeasureTheory.Measure α → PropA signed measure s is said to HaveLebesgueDecomposition with respect to a measure μ
if the positive part and the negative part of s both HaveLebesgueDecomposition with
respect to μ.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound
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 · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
- MeasureTheory.SignedMeasurestatement · cited by 108
Cited by14
Results whose statement or proof uses this declaration.
- MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eqstatement and proof · cited by 6
- MeasureTheory.SignedMeasure.singularPart_addstatement and proof · cited by 2
- MeasureTheory.SignedMeasure.haveLebesgueDecomposition_mkstatement · cited by 1
- MeasureTheory.SignedMeasure.rnDeriv_addstatement and proof · cited by 1
- MeasureTheory.SignedMeasure.rnDeriv_negstatement and proof · cited by 1
- MeasureTheory.SignedMeasure.eq_rnDerivproof · cited by 0
- MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.casesOnstatement and proof · cited by 0
- MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.casesOnstatement and proof · cited by 0
- MeasureTheory.ComplexMeasure.HaveLebesgueDecomposition.recOnstatement and proof · cited by 0
- MeasureTheory.SignedMeasure.HaveLebesgueDecomposition.recOnstatement and proof · cited by 0
- MeasureTheory.SignedMeasure.not_haveLebesgueDecomposition_iffstatement and proof · cited by 0
- MeasureTheory.SignedMeasure.rnDeriv_smulstatement and proof · cited by 0