RadonNikodym

📁 Source: Mathlib/MeasureTheory/Measure/Decomposition/RadonNikodym.lean

Statistics

Metric	Count
Definitions	0
Theorems `map_withDensity_rnDeriv`, `rnDeriv_map`, `rnDeriv_map_aux`, `singularPart_map`, `mconv`, `absolutelyContinuous_iff_withDensity_rnDeriv_eq`, `integrableOn_toReal_rnDeriv`, `integral_toReal_rnDeriv`, `integral_toReal_rnDeriv'`, `inv_rnDeriv`, `inv_rnDeriv'`, `inv_rnDeriv_aux`, `lintegral_rnDeriv`, `lintegral_rnDeriv_le`, `rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular`, `rnDeriv_add_right_of_mutuallySingular`, `rnDeriv_add_right_of_mutuallySingular'`, `rnDeriv_eq_one_iff_eq`, `rnDeriv_eq_zero_of_mutuallySingular`, `rnDeriv_le_one_iff_le`, `rnDeriv_le_one_of_le`, `rnDeriv_mul_rnDeriv`, `rnDeriv_mul_rnDeriv'`, `rnDeriv_pos`, `rnDeriv_pos'`, `rnDeriv_withDensity_left`, `rnDeriv_withDensity_left_of_absolutelyContinuous`, `rnDeriv_withDensity_right`, `rnDeriv_withDensity_right_of_absolutelyContinuous`, `rnDeriv_withDensity_rnDeriv`, `rnDeriv_withDensity_withDensity_rnDeriv_left`, `rnDeriv_withDensity_withDensity_rnDeriv_right`, `setIntegral_toReal_rnDeriv`, `setIntegral_toReal_rnDeriv'`, `setIntegral_toReal_rnDeriv_eq_withDensity`, `setIntegral_toReal_rnDeriv_eq_withDensity'`, `setIntegral_toReal_rnDeriv_le`, `setLIntegral_rnDeriv`, `setLIntegral_rnDeriv'`, `setLIntegral_rnDeriv_le`, `withDensity_rnDeriv_eq`, `conv_eq_withDensity_lconvolution_rnDeriv`, `integrable_rnDeriv_smul_iff`, `integral_rnDeriv_smul`, `lintegral_rnDeriv_mul`, `mconv_eq_withDensity_mlconvolution_rnDeriv`, `rnDeriv_conv`, `rnDeriv_conv'`, `rnDeriv_mconv`, `rnDeriv_mconv'`, `setIntegral_rnDeriv_smul`, `setIntegral_rnDeriv_smul'`, `setLIntegral_rnDeriv_mul`	53
Total	53

MeasurableEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`map_withDensity_rnDeriv` 📖	mathematical	`MeasurableEmbedding`	`MeasureTheory.Measure.map` `MeasureTheory.Measure.withDensity` `MeasureTheory.Measure.rnDeriv`	—	`MeasureTheory.Measure.ext` `map_apply` `MeasureTheory.withDensity_apply` `measurable` `MeasureTheory.setLIntegral_map` `MeasureTheory.Measure.measurable_rnDeriv` `MeasureTheory.setLIntegral_congr_fun_ae` `Filter.mp_mem` `MeasureTheory.Measure.instOuterMeasureClass` `rnDeriv_map` `Filter.univ_mem'`
`rnDeriv_map` 📖	mathematical	`MeasurableEmbedding`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.rnDeriv` `MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.haveLebesgueDecomposition_add` `MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.map_add` `measurable` `sigmaFinite_map` `MeasureTheory.Measure.singularPart.instSigmaFinite` `MeasureTheory.Measure.withDensity.instSigmaFinite` `MeasureTheory.Measure.rnDeriv_add'` `Filter.EventuallyEq.trans` `Filter.EventuallyEq.eq_1` `ae_map_iff` `Filter.EventuallyEq.symm` `Filter.EventuallyEq.add` `MeasureTheory.Measure.rnDeriv_singularPart` `MeasureTheory.Measure.rnDeriv_eq_zero_of_mutuallySingular` `MeasureTheory.Measure.instSFiniteMap` `mutuallySingular_map` `MeasureTheory.Measure.mutuallySingular_singularPart` `MeasureTheory.Measure.AbsolutelyContinuous.rfl` `rnDeriv_map_aux` `MeasureTheory.withDensity_absolutelyContinuous`
`rnDeriv_map_aux` 📖	mathematical	`MeasurableEmbedding` `MeasureTheory.Measure.AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `MeasureTheory.Measure.instFunLike` `MeasureTheory.Measure.instOuterMeasureClass` `MeasureTheory.Measure.rnDeriv` `MeasureTheory.Measure.map`	—	`MeasureTheory.ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite` `Measurable.comp` `MeasureTheory.Measure.measurable_rnDeriv` `measurable` `lintegral_map` `MeasureTheory.Measure.setLIntegral_rnDeriv` `MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `Function.Injective.preimage_image` `injective` `sigmaFinite_map` `restrict_map` `MeasureTheory.Measure.instSFiniteMap` `absolutelyContinuous_map` `map_apply`
`singularPart_map` 📖	mathematical	`MeasurableEmbedding`	`MeasureTheory.Measure.singularPart` `MeasureTheory.Measure.map`	—	`MeasureTheory.Measure.haveLebesgueDecomposition_add` `MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.Measure.map_add` `measurable` `map_withDensity_rnDeriv` `MeasureTheory.Measure.eq_singularPart` `MeasureTheory.Measure.measurable_rnDeriv` `mutuallySingular_map` `MeasureTheory.Measure.mutuallySingular_singularPart`

MeasureTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`conv_eq_withDensity_lconvolution_rnDeriv` 📖	mathematical	`Measure.AbsolutelyContinuous`	`Measure.conv` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `Measure.withDensity` `lconvolution` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid` `Measure.rnDeriv`	—	`conv_withDensity_eq_lconvolution` `Measure.measurable_rnDeriv` `Measure.withDensity_rnDeriv_eq`
`integrable_rnDeriv_smul_iff` 📖	mathematical	`Measure.AbsolutelyContinuous`	`Integrable` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ENNReal.toReal` `Measure.rnDeriv`	—	`Measure.withDensity_rnDeriv_eq` `integrable_withDensity_iff_integrable_smul'` `Measure.measurable_rnDeriv` `Measure.rnDeriv_lt_top`
`integral_rnDeriv_smul` 📖	mathematical	`Measure.AbsolutelyContinuous`	`integral` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ENNReal.toReal` `Measure.rnDeriv`	—	`integral_withDensity_eq_integral_toReal_smul` `Measure.measurable_rnDeriv` `Measure.rnDeriv_lt_top` `Measure.withDensity_rnDeriv_eq`
`lintegral_rnDeriv_mul` 📖	mathematical	`Measure.AbsolutelyContinuous` `AEMeasurable` `ENNReal` `ENNReal.measurableSpace`	`lintegral` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Measure.rnDeriv`	—	`Measure.withDensity_rnDeriv_eq` `lintegral_withDensity_eq_lintegral_mul₀` `Measurable.aemeasurable` `Measure.measurable_rnDeriv`
`mconv_eq_withDensity_mlconvolution_rnDeriv` 📖	mathematical	`Measure.AbsolutelyContinuous`	`Measure.mconv` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `Measure.withDensity` `mlconvolution` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `Measure.rnDeriv`	—	`mconv_withDensity_eq_mlconvolution` `Measure.measurable_rnDeriv` `Measure.withDensity_rnDeriv_eq`
`rnDeriv_conv` 📖	mathematical	`Measure.AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.rnDeriv` `Measure.conv` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `lconvolution` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`HaveLebesgueDecomposition.conv` `Measure.instOuterMeasureClass` `withDensity_eq_iff` `Measurable.aemeasurable` `Measure.measurable_rnDeriv` `aemeasurable_lconvolution` `LT.lt.ne` `Measure.lintegral_rnDeriv_lt_top` `Measure.finite_of_finite_conv` `Measure.withDensity_rnDeriv_eq` `Measure.conv_absolutelyContinuous` `instSFiniteOfSigmaFinite` `IsFiniteMeasure.toSigmaFinite` `conv_eq_withDensity_lconvolution_rnDeriv`
`rnDeriv_conv'` 📖	mathematical	`Measure.AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.rnDeriv` `Measure.conv` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `lconvolution` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`Measure.instOuterMeasureClass` `withDensity_eq_iff_of_sigmaFinite` `Measurable.aemeasurable` `Measure.measurable_rnDeriv` `aemeasurable_lconvolution` `instSFiniteOfSigmaFinite` `conv_eq_withDensity_lconvolution_rnDeriv` `Measure.haveLebesgueDecomposition_of_sigmaFinite` `Measure.withDensity_rnDeriv_eq` `Measure.sfinite_conv_of_sfinite` `Measure.conv_absolutelyContinuous`
`rnDeriv_mconv` 📖	mathematical	`Measure.AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.rnDeriv` `Measure.mconv` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `mlconvolution` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`HaveLebesgueDecomposition.mconv` `Measure.instOuterMeasureClass` `withDensity_eq_iff` `Measurable.aemeasurable` `Measure.measurable_rnDeriv` `aemeasurable_mlconvolution` `LT.lt.ne` `Measure.lintegral_rnDeriv_lt_top` `Measure.finite_of_finite_mconv` `Measure.withDensity_rnDeriv_eq` `Measure.mconv_absolutelyContinuous` `instSFiniteOfSigmaFinite` `IsFiniteMeasure.toSigmaFinite` `mconv_eq_withDensity_mlconvolution_rnDeriv`
`rnDeriv_mconv'` 📖	mathematical	`Measure.AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `ae` `Measure` `Measure.instFunLike` `Measure.instOuterMeasureClass` `Measure.rnDeriv` `Measure.mconv` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `mlconvolution` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`Measure.instOuterMeasureClass` `withDensity_eq_iff_of_sigmaFinite` `Measurable.aemeasurable` `Measure.measurable_rnDeriv` `aemeasurable_mlconvolution` `instSFiniteOfSigmaFinite` `mconv_eq_withDensity_mlconvolution_rnDeriv` `Measure.haveLebesgueDecomposition_of_sigmaFinite` `Measure.withDensity_rnDeriv_eq` `Measure.sfinite_mconv_of_sfinite` `Measure.mconv_absolutelyContinuous`
`setIntegral_rnDeriv_smul` 📖	mathematical	`Measure.AbsolutelyContinuous` `MeasurableSet`	`integral` `Measure.restrict` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ENNReal.toReal` `Measure.rnDeriv`	—	`setIntegral_withDensity_eq_setIntegral_toReal_smul` `Measure.measurable_rnDeriv` `ae_restrict_of_ae` `Measure.rnDeriv_lt_top` `Measure.withDensity_rnDeriv_eq`
`setIntegral_rnDeriv_smul'` 📖	mathematical	`Measure.AbsolutelyContinuous`	`integral` `Measure.restrict` `Real` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `Real.semiring` `ESeminormedAddCommMonoid.toAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `ENNReal.toReal` `Measure.rnDeriv`	—	`setIntegral_withDensity_eq_setIntegral_toReal_smul'` `instSFiniteOfSigmaFinite` `Measure.measurable_rnDeriv` `ae_restrict_of_ae` `Measure.rnDeriv_lt_top` `Measure.withDensity_rnDeriv_eq` `Measure.haveLebesgueDecomposition_of_sigmaFinite`
`setLIntegral_rnDeriv_mul` 📖	mathematical	`Measure.AbsolutelyContinuous` `AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `MeasurableSet`	`lintegral` `Measure.restrict` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `Measure.rnDeriv`	—	`Measure.withDensity_rnDeriv_eq` `setLIntegral_withDensity_eq_lintegral_mul₀` `Measurable.aemeasurable` `Measure.measurable_rnDeriv`

MeasureTheory.HaveLebesgueDecomposition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mconv` 📖	mathematical	`MeasureTheory.Measure.AbsolutelyContinuous`	`MeasureTheory.Measure.HaveLebesgueDecomposition` `MeasureTheory.Measure.mconv` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`MeasureTheory.measurable_mlconvolution` `MeasureTheory.Measure.measurable_rnDeriv` `zero_add` `MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv`

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`absolutelyContinuous_iff_withDensity_rnDeriv_eq` 📖	mathematical	—	`AbsolutelyContinuous` `withDensity` `rnDeriv`	—	`withDensity_rnDeriv_eq` `MeasureTheory.withDensity_absolutelyContinuous`
`integrableOn_toReal_rnDeriv` 📖	mathematical	—	`MeasureTheory.IntegrableOn` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `SeminormedAddGroup.toContinuousENorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `Real.normedCommRing` `ENNReal.toReal` `rnDeriv`	—	`MeasureTheory.integrable_toReal_of_lintegral_ne_top` `Measurable.aemeasurable` `measurable_rnDeriv` `LT.lt.ne` `LE.le.trans_lt` `setLIntegral_rnDeriv_le` `Ne.lt_top`
`integral_toReal_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `ENNReal.toReal` `rnDeriv` `real` `Set.univ`	—	`MeasureTheory.setIntegral_univ` `setIntegral_toReal_rnDeriv`
`integral_toReal_rnDeriv'` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `ENNReal.toReal` `rnDeriv` `Real.instSub` `real` `Set.univ` `singularPart`	—	`MeasureTheory.measureReal_def` `ENNReal.toReal_sub_of_le` `singularPart_le` `MeasureTheory.measure_ne_top` `sub_apply` `singularPart.instIsFiniteMeasure` `MeasurableSet.univ` `measure_sub_singularPart` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.IsFiniteMeasure.toSigmaFinite` `setIntegral_toReal_rnDeriv_eq_withDensity` `MeasureTheory.setIntegral_univ`
`inv_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Pi.instInv` `ENNReal.instInv` `rnDeriv`	—	`instOuterMeasureClass` `Filter.mp_mem` `rnDeriv_withDensity_rnDeriv` `Filter.univ_mem'` `Filter.EventuallyEq.symm` `rnDeriv_withDensity` `measurable_rnDeriv` `Filter.EventuallyEq.trans` `inv_rnDeriv_aux` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `withDensity.instSigmaFinite` `haveLebesgueDecompositionRnDeriv` `absolutelyContinuous_withDensity_rnDeriv` `MeasureTheory.withDensity_absolutelyContinuous`
`inv_rnDeriv'` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Pi.instInv` `ENNReal.instInv` `rnDeriv`	—	`Filter.mp_mem` `instOuterMeasureClass` `inv_rnDeriv` `Filter.univ_mem'` `inv_inv`
`inv_rnDeriv_aux` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Pi.instInv` `ENNReal.instInv` `rnDeriv`	—	`withDensity_rnDeriv_eq` `MeasureTheory.withDensity_inv_same` `measurable_rnDeriv` `Filter.mp_mem` `instOuterMeasureClass` `AbsolutelyContinuous.ae_le` `rnDeriv_pos` `Filter.univ_mem'` `LT.lt.ne'` `rnDeriv_ne_top` `Filter.EventuallyEq.symm` `rnDeriv_withDensity` `Measurable.inv` `ENNReal.instMeasurableInv`
`lintegral_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`MeasureTheory.lintegral` `rnDeriv` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike` `Set.univ`	—	`MeasureTheory.setLIntegral_univ` `setLIntegral_rnDeriv'` `MeasurableSet.univ`
`lintegral_rnDeriv_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.lintegral` `rnDeriv` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike` `Set.univ`	—	`setLIntegral_rnDeriv_le` `MeasureTheory.setLIntegral_univ`
`rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular` 📖	mathematical	`AbsolutelyContinuous` `MutuallySingular`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instAdd`	—	`MutuallySingular.measurableSet_nullSet` `MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl` `instOuterMeasureClass` `MeasureTheory.ae.congr_simp` `MutuallySingular.restrict_nullSet` `MeasureTheory.ae_zero` `MeasureTheory.withDensity_eq_iff_of_sigmaFinite` `MeasureTheory.Restrict.sigmaFinite` `Measurable.aemeasurable` `measurable_rnDeriv` `restrict_add` `MutuallySingular.restrict_compl_nullSet` `add_zero` `MeasureTheory.restrict_withDensity` `MeasurableSet.compl` `withDensity_rnDeriv_eq` `AbsolutelyContinuous.add_right`
`rnDeriv_add_right_of_mutuallySingular` 📖	mathematical	`MutuallySingular`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instAdd`	—	`AbsolutelyContinuous.add_right` `AbsolutelyContinuous.rfl` `instOuterMeasureClass` `haveLebesgueDecomposition_add` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `rnDeriv_add'` `singularPart.instSigmaFinite` `withDensity.instSigmaFinite` `MeasureTheory.Add.sigmaFinite` `Filter.EventuallyEq.trans` `AbsolutelyContinuous.ae_le` `rnDeriv_add_right_of_mutuallySingular'` `mutuallySingular_singularPart` `rnDeriv_eq_zero_of_mutuallySingular` `withDensity.instSFinite` `MutuallySingular.withDensity` `MutuallySingular.symm` `rnDeriv_eq_zero` `Filter.mp_mem` `Filter.univ_mem'` `Pi.add_apply` `Filter.EventuallyEq.symm`
`rnDeriv_add_right_of_mutuallySingular'` 📖	mathematical	`MutuallySingular`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `instAdd`	—	`AbsolutelyContinuous.add_right` `AbsolutelyContinuous.rfl` `instOuterMeasureClass` `haveLebesgueDecomposition_add` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `rnDeriv_add'` `singularPart.instSigmaFinite` `withDensity.instSigmaFinite` `MeasureTheory.Add.sigmaFinite` `Filter.EventuallyEq.trans` `AbsolutelyContinuous.ae_le` `rnDeriv_add_right_of_absolutelyContinuous_of_mutuallySingular` `haveLebesgueDecompositionRnDeriv` `withDensity.instSFinite` `MeasureTheory.withDensity_absolutelyContinuous` `AbsolutelyContinuous.ae_eq` `mutuallySingular_singularPart` `MutuallySingular.singularPart` `rnDeriv_singularPart` `Filter.mp_mem` `Filter.univ_mem'` `Filter.EventuallyEq.symm`
`rnDeriv_eq_one_iff_eq` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`instOuterMeasureClass` `withDensity_rnDeriv_eq` `MeasureTheory.withDensity_congr_ae` `MeasureTheory.withDensity_one` `rnDeriv_self`
`rnDeriv_eq_zero_of_mutuallySingular` 📖	mathematical	`MutuallySingular` `AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `Pi.instZero` `instZeroENNReal`	—	`MutuallySingular.measurableSet_nullSet` `MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl` `instOuterMeasureClass` `AbsolutelyContinuous.ae_le` `rnDeriv_restrict` `Filter.EventuallyEq.eq_1` `MeasureTheory.ae_restrict_iff'` `Filter.mp_mem` `Filter.univ_mem'` `Set.indicator_of_mem` `Filter.EventuallyEq.trans` `MutuallySingular.restrict_nullSet` `rnDeriv_zero` `AbsolutelyContinuous.trans` `LE.le.absolutelyContinuous` `restrict_le_self` `MeasureTheory.ae.congr_simp` `MutuallySingular.restrict_compl_nullSet` `MeasureTheory.ae_zero`
`rnDeriv_le_one_iff_le` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyLE` `ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal` `instPartialOrder`	—	`instOuterMeasureClass` `withDensity_rnDeriv_eq` `MeasureTheory.withDensity_apply'` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.setLIntegral_one` `MeasureTheory.setLIntegral_mono_ae` `aemeasurable_const` `Filter.Eventually.mono` `rnDeriv_le_one_of_le`
`rnDeriv_le_one_of_le` 📖	mathematical	`MeasureTheory.Measure` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Filter.EventuallyLE` `ENNReal` `ENNReal.instPartialOrder` `MeasureTheory.ae` `instFunLike` `instOuterMeasureClass` `rnDeriv` `Pi.instOne` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `instAddCommMonoidWithOneENNReal`	—	`MeasureTheory.ae_le_of_forall_setLIntegral_le_of_sigmaFinite` `measurable_rnDeriv` `MeasureTheory.setLIntegral_one` `LE.le.trans` `setLIntegral_rnDeriv_le`
`rnDeriv_mul_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `rnDeriv`	—	`Filter.EventuallyEq.trans` `instOuterMeasureClass` `Filter.EventuallyEq.symm` `rnDeriv_withDensity_left` `Measurable.aemeasurable` `measurable_rnDeriv` `rnDeriv_ne_top` `withDensity_rnDeriv_eq` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `Filter.EventuallyEq.refl`
`rnDeriv_mul_rnDeriv'` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `rnDeriv`	—	`instOuterMeasureClass` `haveLebesgueDecomposition_spec` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `Filter.mp_mem` `rnDeriv_eq_zero_of_mutuallySingular` `singularPart.instSigmaFinite` `rnDeriv_withDensity_left_of_absolutelyContinuous` `Measurable.aemeasurable` `rnDeriv_add'` `withDensity.instSigmaFinite` `Filter.univ_mem'` `Pi.add_apply` `Pi.mul_apply` `Pi.zero_apply` `zero_add`
`rnDeriv_pos` 📖	mathematical	`AbsolutelyContinuous`	`Filter.Eventually` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `rnDeriv` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	—	`instOuterMeasureClass` `withDensity_rnDeriv_eq` `MeasureTheory.ae_withDensity_iff` `measurable_rnDeriv` `MeasureTheory.ae_of_all` `lt_of_le_of_ne` `zero_le` `ENNReal.instCanonicallyOrderedAdd`
`rnDeriv_pos'` 📖	mathematical	`AbsolutelyContinuous`	`Filter.Eventually` `ENNReal` `Preorder.toLT` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `instZeroENNReal` `rnDeriv` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	—	`AbsolutelyContinuous.ae_le` `absolutelyContinuous_withDensity_rnDeriv` `Filter.mp_mem` `instOuterMeasureClass` `MeasureTheory.withDensity_absolutelyContinuous` `rnDeriv_withDensity` `measurable_rnDeriv` `rnDeriv_pos` `haveLebesgueDecompositionRnDeriv` `Filter.univ_mem'`
`rnDeriv_withDensity_left` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Filter.Eventually` `Top.top` `instTopENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`Filter.EventuallyEq` `rnDeriv` `withDensity` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`instOuterMeasureClass` `MeasureTheory.withDensity_absolutelyContinuous` `rnDeriv_withDensity_left_of_absolutelyContinuous` `withDensity.instSigmaFinite` `rnDeriv_withDensity` `measurable_rnDeriv` `rnDeriv_withDensity_withDensity_rnDeriv_left` `Filter.mp_mem` `Filter.univ_mem'`
`rnDeriv_withDensity_left_of_absolutelyContinuous` 📖	mathematical	`AbsolutelyContinuous` `AEMeasurable` `ENNReal` `ENNReal.measurableSpace`	`Filter.EventuallyEq` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `withDensity` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`Filter.EventuallyEq.symm` `instOuterMeasureClass` `eq_rnDeriv₀` `AEMeasurable.mul` `ENNReal.instMeasurableMul₂` `Measurable.aemeasurable` `measurable_rnDeriv` `MutuallySingular.zero_left` `ext` `zero_add` `MeasureTheory.withDensity_apply` `withDensity_rnDeriv_eq` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀` `MeasureTheory.ae_restrict_of_ae` `rnDeriv_lt_top` `mul_comm`
`rnDeriv_withDensity_right` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Filter.Eventually` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Top.top` `instTopENNReal`	`Filter.EventuallyEq` `rnDeriv` `withDensity` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv`	—	`instOuterMeasureClass` `rnDeriv_withDensity_withDensity_rnDeriv_right` `Filter.EventuallyEq.symm` `rnDeriv_withDensity` `measurable_rnDeriv` `rnDeriv_withDensity_right_of_absolutelyContinuous` `haveLebesgueDecompositionRnDeriv` `MeasureTheory.withDensity_absolutelyContinuous` `Filter.mp_mem` `Filter.univ_mem'`
`rnDeriv_withDensity_right_of_absolutelyContinuous` 📖	mathematical	`AbsolutelyContinuous` `AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Filter.Eventually` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Top.top` `instTopENNReal`	`Filter.EventuallyEq` `rnDeriv` `withDensity` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring` `ENNReal.instInv`	—	`instOuterMeasureClass` `MeasureTheory.SigmaFinite.withDensity_of_ne_top` `AbsolutelyContinuous.ae_eq` `MeasureTheory.withDensity_absolutelyContinuous'` `Filter.EventuallyEq.symm` `eq_rnDeriv₀` `AEMeasurable.mul` `ENNReal.instMeasurableMul₂` `AEMeasurable.mono_ac` `AEMeasurable.inv` `ENNReal.instMeasurableInv` `MeasureTheory.withDensity_absolutelyContinuous` `Measurable.aemeasurable` `measurable_rnDeriv` `MutuallySingular.zero_left` `ext` `withDensity_rnDeriv_eq` `zero_add` `MeasureTheory.withDensity_apply` `MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀` `AEMeasurable.restrict` `MeasureTheory.ae_restrict_of_ae` `Filter.mp_mem` `Filter.univ_mem'` `Ne.lt_top` `ENNReal.mul_inv_cancel` `one_mul` `MeasureTheory.lintegral_congr_ae`
`rnDeriv_withDensity_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`Filter.EventuallyEq` `ENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `rnDeriv` `withDensity`	—	`instOuterMeasureClass` `haveLebesgueDecomposition_add` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `add_comm` `AbsolutelyContinuous.ae_eq` `absolutelyContinuous_withDensity_rnDeriv` `Filter.EventuallyEq.symm` `rnDeriv_add_right_of_mutuallySingular` `withDensity.instSigmaFinite` `singularPart.instSigmaFinite` `MutuallySingular.withDensity` `MutuallySingular.symm` `mutuallySingular_singularPart`
`rnDeriv_withDensity_withDensity_rnDeriv_left` 📖	mathematical	`Filter.Eventually` `ENNReal` `Top.top` `instTopENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass`	`Filter.EventuallyEq` `rnDeriv` `withDensity`	—	`instOuterMeasureClass` `haveLebesgueDecomposition_add` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `add_comm` `MeasureTheory.withDensity_add_measure` `MeasureTheory.SigmaFinite.withDensity_of_ne_top` `singularPart.instSigmaFinite` `MeasureTheory.ae_mono` `singularPart_le` `withDensity.instSigmaFinite` `withDensity_rnDeriv_le` `Filter.EventuallyEq.symm` `rnDeriv_add_of_mutuallySingular` `MutuallySingular.withDensity` `mutuallySingular_singularPart`
`rnDeriv_withDensity_withDensity_rnDeriv_right` 📖	mathematical	`AEMeasurable` `ENNReal` `ENNReal.measurableSpace` `Filter.Eventually` `instZeroENNReal` `MeasureTheory.ae` `MeasureTheory.Measure` `instFunLike` `instOuterMeasureClass` `Top.top` `instTopENNReal`	`Filter.EventuallyEq` `rnDeriv` `withDensity`	—	`instOuterMeasureClass` `haveLebesgueDecomposition_add` `haveLebesgueDecomposition_of_sigmaFinite` `MeasureTheory.instSFiniteOfSigmaFinite` `add_comm` `MeasureTheory.withDensity_absolutelyContinuous'` `AbsolutelyContinuous.ae_eq` `MeasureTheory.SigmaFinite.withDensity_of_ne_top` `Filter.EventuallyEq.symm` `rnDeriv_add_of_mutuallySingular` `withDensity.instSigmaFinite` `singularPart.instSigmaFinite` `MutuallySingular.symm` `MutuallySingular.withDensity` `mutuallySingular_singularPart`
`setIntegral_toReal_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `restrict` `ENNReal.toReal` `rnDeriv` `real`	—	`setIntegral_toReal_rnDeriv_eq_withDensity` `MeasureTheory.instSFiniteOfSigmaFinite` `withDensity_rnDeriv_eq` `haveLebesgueDecomposition_of_sigmaFinite`
`setIntegral_toReal_rnDeriv'` 📖	mathematical	`AbsolutelyContinuous` `MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `restrict` `ENNReal.toReal` `rnDeriv` `real`	—	`setIntegral_toReal_rnDeriv_eq_withDensity'` `withDensity_rnDeriv_eq` `MeasureTheory.measureReal_def`
`setIntegral_toReal_rnDeriv_eq_withDensity` 📖	mathematical	—	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `restrict` `ENNReal.toReal` `rnDeriv` `real` `withDensity`	—	`MeasureTheory.integral_toReal` `Measurable.aemeasurable` `measurable_rnDeriv` `MeasureTheory.ae_restrict_of_ae` `rnDeriv_lt_top` `MeasureTheory.measureReal_def` `ENNReal.toReal_eq_toReal_iff` `MeasureTheory.withDensity_apply'`
`setIntegral_toReal_rnDeriv_eq_withDensity'` 📖	mathematical	`MeasurableSet`	`MeasureTheory.integral` `Real` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `restrict` `ENNReal.toReal` `rnDeriv` `real` `withDensity`	—	`MeasureTheory.integral_toReal` `Measurable.aemeasurable` `measurable_rnDeriv` `MeasureTheory.ae_restrict_of_ae` `rnDeriv_lt_top` `MeasureTheory.measureReal_def` `ENNReal.toReal_eq_toReal_iff` `MeasureTheory.withDensity_apply`
`setIntegral_toReal_rnDeriv_le` 📖	mathematical	—	`Real` `Real.instLE` `MeasureTheory.integral` `Real.normedAddCommGroup` `NormedField.toNormedSpace` `Real.normedField` `restrict` `ENNReal.toReal` `rnDeriv` `real`	—	`MeasureTheory.measurableSet_toMeasurable` `MeasureTheory.measure_toMeasurable` `MeasureTheory.setIntegral_mono_set` `Real.instIsOrderedAddMonoid` `IsStrictOrderedModule.toIsOrderedModule` `IsStrictOrderedRing.toIsStrictOrderedModule` `Real.instIsStrictOrderedRing` `HasSolidNorm.orderClosedTopology` `instHasSolidNormReal` `integrableOn_toReal_rnDeriv` `MeasureTheory.ae_of_all` `instOuterMeasureClass` `HasSubset.Subset.eventuallyLE` `MeasureTheory.subset_toMeasurable` `setIntegral_toReal_rnDeriv_eq_withDensity'` `ENNReal.toReal_mono` `measure_mono_left` `withDensity_rnDeriv_le` `MeasureTheory.measureReal_def`
`setLIntegral_rnDeriv` 📖	mathematical	`AbsolutelyContinuous`	`MeasureTheory.lintegral` `restrict` `rnDeriv` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike`	—	`MeasureTheory.withDensity_apply'` `withDensity_rnDeriv_eq`
`setLIntegral_rnDeriv'` 📖	mathematical	`AbsolutelyContinuous` `MeasurableSet`	`MeasureTheory.lintegral` `restrict` `rnDeriv` `DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `instFunLike`	—	`MeasureTheory.withDensity_apply` `withDensity_rnDeriv_eq`
`setLIntegral_rnDeriv_le` 📖	mathematical	—	`ENNReal` `Preorder.toLE` `PartialOrder.toPreorder` `ENNReal.instPartialOrder` `MeasureTheory.lintegral` `restrict` `rnDeriv` `DFunLike.coe` `MeasureTheory.Measure` `Set` `instFunLike`	—	`LE.le.trans` `MeasureTheory.withDensity_apply_le` `le_iff'` `withDensity_rnDeriv_le`
`withDensity_rnDeriv_eq` 📖	mathematical	`AbsolutelyContinuous`	`withDensity` `rnDeriv`	—	`singularPart_eq_zero` `haveLebesgueDecomposition_add` `zero_add`

---

← Back to Index