Theorems · Definition · measure theory
MeasureTheory.ComplexMeasure.rnDeriv
{α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.ComplexMeasure α → MeasureTheory.Measure α → α → ℂThe Radon-Nikodym derivative between a complex measure and a positive measure.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 209 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Complexstatement · cited by 5,565
- MeasureTheory.SignedMeasure.rnDerivproof · cited by 13
- MeasureTheory.ComplexMeasurestatement and proof · cited by 13
- MeasureTheory.ComplexMeasure.improof · cited by 7
- MeasureTheory.ComplexMeasure.reproof · cited by 7
Cited by2
Results whose statement or proof uses this declaration.
- MeasureTheory.ComplexMeasure.integrable_rnDerivstatement · cited by 1
- MeasureTheory.ComplexMeasure.singularPart_add_withDensity_rnDeriv_eqstatement and proof · cited by 0