Documentation Verification Report

RadonNikodym

📁 Source: Mathlib/Probability/Kernel/Composition/RadonNikodym.lean

Statistics

Metric	Count
Definitions	0
Theorems `rnDeriv_compProd`, `rnDeriv_compProd_withDensity_rnDeriv`, `rnDeriv_measure_compProd_left`	3
Total	3

ProbabilityTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`rnDeriv_compProd` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous` `Prod.instMeasurableSpace` `MeasureTheory.Measure.compProd`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.compProd` `MeasureTheory.Measure.rnDeriv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Filter.EventuallyEq.trans` `MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.symm` `MeasureTheory.Measure.rnDeriv_mul_rnDeriv` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel` `Filter.mp_mem` `rnDeriv_measure_compProd_left` `Filter.univ_mem'` `Pi.mul_apply` `mul_comm`
`rnDeriv_compProd_withDensity_rnDeriv` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.compProd` `MeasureTheory.Measure.rnDeriv` `MeasureTheory.Measure.withDensity`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.haveLebesgueDecomposition_add` `MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `MeasureTheory.Measure.compProd_add_left` `MeasureTheory.Measure.singularPart.instSigmaFinite` `MeasureTheory.Measure.withDensity.instSFinite` `MeasureTheory.Measure.rnDeriv_add'` `MeasureTheory.Measure.instIsFiniteMeasureProdCompProdOfIsFiniteKernel` `MeasureTheory.Measure.singularPart.instIsFiniteMeasure` `MeasureTheory.Measure.withDensity.instIsFiniteMeasure` `MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular` `MeasureTheory.Measure.instSFiniteProdCompProd` `MeasureTheory.Measure.MutuallySingular.compProd_of_left` `MeasureTheory.Measure.mutuallySingular_singularPart` `MeasureTheory.Measure.AbsolutelyContinuous.rfl` `Filter.mp_mem` `Filter.univ_mem'` `zero_add`
`rnDeriv_measure_compProd_left` 📖	mathematical	—	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.compProd` `MeasureTheory.Measure.rnDeriv`	—	`MeasureTheory.Measure.instOuterMeasureClass` `Filter.EventuallyEq.symm` `rnDeriv_compProd_withDensity_rnDeriv` `MeasureTheory.withDensity_absolutelyContinuous` `MeasureTheory.Measure.withDensity.instIsFiniteMeasure` `MeasureTheory.Measure.ae_eq_compProd_of_ae_eq_fst` `instMeasurableEqOfSecondCountableTopologyOfT2Space` `BorelSpace.opensMeasurable` `ENNReal.borelSpace` `ENNReal.instSecondCountableTopology` `ENNReal.instT2Space` `MeasureTheory.Measure.measurable_rnDeriv` `MeasureTheory.Measure.rnDeriv_withDensity` `MeasureTheory.IsFiniteMeasure.toSigmaFinite`

---

← Back to Index