Theorems · Definition · measure theory
MeasureTheory.Measure.rnDeriv
{α : Type u_2} → {m : MeasurableSpace α} → MeasureTheory.Measure α → MeasureTheory.Measure α → α → ENNRealIf a pair of measures HaveLebesgueDecomposition, then rnDeriv chooses the
measurable function from HaveLebesgueDecomposition, otherwise it returns the zero function.
For sigma-finite measures, μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν).
- Cited by
- 234 results in Mathlib
- Foundations
- Depth 207 from the axioms, rests on 4,865 definitions · 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
- ENNRealstatement · cited by 9,879
Cited by239
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.measurable_rnDerivstatement · cited by 75
- MeasureTheory.llrproof · cited by 59
- MeasureTheory.Measure.haveLebesgueDecomposition_addstatement · cited by 35
- MeasureTheory.pdfproof · cited by 32
- MeasureTheory.Measure.withDensity_rnDeriv_eqstatement and proof · cited by 31
- ProbabilityTheory.Kernel.rnDerivAuxproof · cited by 22
- MeasureTheory.Measure.rnDeriv_lt_topstatement and proof · cited by 21
- ProbabilityTheory.preCDFproof · cited by 15
- MeasureTheory.condLExp_of_not_sigmaFiniteproof · cited by 14
- MeasureTheory.SignedMeasure.rnDerivproof · cited by 13
- MeasureTheory.Measure.rnDeriv_withDensitystatement · cited by 13
- ProbabilityTheory.Kernel.rnDeriv_eq_rnDeriv_measurestatement · cited by 13
Showing the 200 most cited of 239.