RadonNikodym

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

Statistics

Metric	Count
Definitions mutuallySingularSet, mutuallySingularSetSlice, rnDeriv, rnDerivAux, singularPart	5
Theorems eq_rnDeriv, eq_rnDeriv_measure, eq_singularPart, eq_singularPart_measure, instIsFiniteKernelSingularPart, instIsFiniteKernelWithDensityRnDeriv, lintegral_rnDeriv, measurableSet_absolutelyContinuous, measurableSet_mutuallySingular, measurableSet_mutuallySingularSet, measurableSet_mutuallySingularSetSlice, measurable_rnDeriv, measurable_rnDerivAux, measurable_rnDerivAux_right, measurable_rnDeriv_right, measurable_singularPart, measurable_singularPart_fun, measurable_singularPart_fun_right, measure_mutuallySingularSetSlice, mem_mutuallySingularSetSlice, mutuallySingular_singularPart, notMem_mutuallySingularSetSlice, rnDerivAux_le_one, rnDerivAux_nonneg, rnDeriv_add, rnDeriv_add_singularPart, rnDeriv_def, rnDeriv_def', rnDeriv_eq_one_iff_eq, rnDeriv_eq_rnDeriv_measure, rnDeriv_eq_top_iff, rnDeriv_eq_top_iff', rnDeriv_lt_top, rnDeriv_ne_top, rnDeriv_pos, rnDeriv_self, rnDeriv_singularPart, rnDeriv_toReal_pos, rnDeriv_withDensity, setLIntegral_rnDeriv, setLIntegral_rnDerivAux, setLIntegral_rnDeriv_le, singularPart_compl_mutuallySingularSetSlice, singularPart_def, singularPart_eq_singularPart_measure, singularPart_eq_zero_iff_absolutelyContinuous, singularPart_eq_zero_iff_apply_eq_zero, singularPart_eq_zero_iff_measure_eq_zero, singularPart_of_subset_compl_mutuallySingularSetSlice, singularPart_of_subset_mutuallySingularSetSlice, singularPart_self, withDensity_one_sub_rnDerivAux, withDensity_rnDerivAux, withDensity_rnDeriv_eq, withDensity_rnDeriv_eq_zero_iff_apply_eq_zero, withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, withDensity_rnDeriv_eq_zero_iff_mutuallySingular, withDensity_rnDeriv_le, withDensity_rnDeriv_mutuallySingularSetSlice, withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice, withDensity_rnDeriv_of_subset_mutuallySingularSetSlice	61
Total	66

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
mutuallySingularSet 📖	CompOp	2 math math: rnDeriv_eq_top_iff, measurableSet_mutuallySingularSet
mutuallySingularSetSlice 📖	CompOp	11 math math: withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, notMem_mutuallySingularSetSlice, rnDeriv_eq_top_iff', singularPart_eq_zero_iff_apply_eq_zero, singularPart_eq_zero_iff_measure_eq_zero, withDensity_rnDeriv_eq_zero_iff_apply_eq_zero, measurableSet_mutuallySingularSetSlice, singularPart_compl_mutuallySingularSetSlice, withDensity_rnDeriv_mutuallySingularSetSlice, mem_mutuallySingularSetSlice, measure_mutuallySingularSetSlice
rnDeriv 📖	CompOp	37 math math: ProbabilityTheory.posterior_eq_withDensity, rnDeriv_add_singularPart, withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, rnDeriv_eq_one_iff_eq, measurable_singularPart_fun_right, instIsFiniteKernelWithDensityRnDeriv, ProbabilityTheory.rnDeriv_posterior_symm, rnDeriv_singularPart, rnDeriv_def', rnDeriv_eq_rnDeriv_measure, rnDeriv_eq_top_iff', rnDeriv_ne_top, rnDeriv_eq_top_iff, measurable_rnDeriv, rnDeriv_toReal_pos, rnDeriv_pos, measurable_singularPart_fun, measurable_rnDeriv_right, withDensity_rnDeriv_of_subset_mutuallySingularSetSlice, withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice, withDensity_rnDeriv_le, rnDeriv_lt_top, withDensity_rnDeriv_eq_zero_iff_mutuallySingular, withDensity_rnDeriv_eq_zero_iff_apply_eq_zero, lintegral_rnDeriv, withDensity_rnDeriv_eq, setLIntegral_rnDeriv, ProbabilityTheory.rnDeriv_posterior, withDensity_rnDeriv_mutuallySingularSetSlice, singularPart_def, eq_rnDeriv, rnDeriv_add, rnDeriv_self, ProbabilityTheory.rnDeriv_posterior_ae_prod, rnDeriv_withDensity, rnDeriv_def, setLIntegral_rnDeriv_le
rnDerivAux 📖	CompOp	14 math math: measurable_rnDerivAux, notMem_mutuallySingularSetSlice, measurable_singularPart_fun_right, rnDeriv_def', rnDerivAux_le_one, measurable_singularPart_fun, withDensity_rnDerivAux, withDensity_one_sub_rnDerivAux, rnDerivAux_nonneg, mem_mutuallySingularSetSlice, singularPart_def, measurable_rnDerivAux_right, rnDeriv_def, setLIntegral_rnDerivAux
singularPart 📖	CompOp	14 math math: rnDeriv_add_singularPart, mutuallySingular_singularPart, rnDeriv_singularPart, singularPart_eq_zero_iff_apply_eq_zero, eq_singularPart, singularPart_eq_zero_iff_measure_eq_zero, singularPart_self, singularPart_eq_singularPart_measure, singularPart_of_subset_compl_mutuallySingularSetSlice, singularPart_eq_zero_iff_absolutelyContinuous, singularPart_compl_mutuallySingularSetSlice, singularPart_def, instIsFiniteKernelSingularPart, singularPart_of_subset_mutuallySingularSetSlice

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_rnDeriv 📖	mathematical	ProbabilityTheory.Kernel instAdd withDensity IsFiniteKernel.isSFiniteKernel Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasureTheory.Measure.MutuallySingular DFunLike.coe MeasureTheory.Measure instFunLike	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass rnDeriv	—	IsFiniteKernel.isSFiniteKernel Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass eq_rnDeriv_measure Filter.EventuallyEq.symm rnDeriv_eq_rnDeriv_measure
eq_rnDeriv_measure 📖	mathematical	ProbabilityTheory.Kernel instAdd withDensity IsFiniteKernel.isSFiniteKernel Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasureTheory.Measure.MutuallySingular DFunLike.coe MeasureTheory.Measure instFunLike	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv	—	IsFiniteKernel.isSFiniteKernel coe_add Pi.add_apply withDensity_apply add_comm MeasureTheory.Measure.eq_rnDeriv₀ MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure Measurable.aemeasurable Measurable.comp measurable_prodMk_left
eq_singularPart 📖	mathematical	ProbabilityTheory.Kernel instAdd withDensity IsFiniteKernel.isSFiniteKernel Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasureTheory.Measure.MutuallySingular DFunLike.coe MeasureTheory.Measure instFunLike	singularPart	—	IsFiniteKernel.isSFiniteKernel eq_singularPart_measure singularPart_eq_singularPart_measure
eq_singularPart_measure 📖	mathematical	ProbabilityTheory.Kernel instAdd withDensity IsFiniteKernel.isSFiniteKernel Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasureTheory.Measure.MutuallySingular DFunLike.coe MeasureTheory.Measure instFunLike	MeasureTheory.Measure.singularPart	—	IsFiniteKernel.isSFiniteKernel coe_add Pi.add_apply withDensity_apply add_comm MeasureTheory.Measure.eq_singularPart Measurable.comp measurable_prodMk_left
instIsFiniteKernelSingularPart 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel singularPart IsFiniteKernel.isSFiniteKernel	—	IsFiniteKernel.isSFiniteKernel bound_lt_top rnDeriv_add_singularPart LE.le.trans self_le_add_left ENNReal.instCanonicallyOrderedAdd Eq.le measure_le_bound
instIsFiniteKernelWithDensityRnDeriv 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel withDensity IsFiniteKernel.isSFiniteKernel rnDeriv	—	IsFiniteKernel.isSFiniteKernel bound_lt_top withDensity_apply' measurable_rnDeriv MeasureTheory.setLIntegral_univ MeasureTheory.lintegral_congr_ae rnDeriv_eq_rnDeriv_measure LE.le.trans MeasureTheory.Measure.lintegral_rnDeriv_le measure_le_bound
lintegral_rnDeriv 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	MeasureTheory.lintegral rnDeriv Set ENNReal MeasureTheory.Measure.instFunLike Set.univ	—	MeasureTheory.setLIntegral_univ setLIntegral_rnDeriv MeasurableSet.univ
measurableSet_absolutelyContinuous 📖	mathematical	—	MeasurableSet setOf MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	IsFiniteKernel.isSFiniteKernel measurable_kernel_prodMk_left measurableSet_mutuallySingularSet MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space
measurableSet_mutuallySingular 📖	mathematical	—	MeasurableSet setOf MeasureTheory.Measure.MutuallySingular DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	IsFiniteKernel.isSFiniteKernel measurable_kernel_prodMk_left MeasurableSet.compl measurableSet_mutuallySingularSet MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space
measurableSet_mutuallySingularSet 📖	mathematical	—	MeasurableSet Prod.instMeasurableSpace mutuallySingularSet	—	measurable_rnDerivAux measurableSet_Ici BorelSpace.opensMeasurable Real.borelSpace instClosedIciTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid
measurableSet_mutuallySingularSetSlice 📖	mathematical	—	MeasurableSet mutuallySingularSetSlice	—	measurable_prodMk_left measurableSet_mutuallySingularSet
measurable_rnDeriv 📖	mathematical	—	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace rnDeriv	—	rnDeriv_def Measurable.div measurableDiv₂_of_mul_inv ENNReal.instMeasurableMul₂ ENNReal.instMeasurableInv Measurable.ennreal_ofReal measurable_rnDerivAux Measurable.sub ContinuousSub.measurableSub₂ Real.borelSpace instSecondCountableTopologyReal IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal measurable_const
measurable_rnDerivAux 📖	mathematical	—	Measurable Real Prod.instMeasurableSpace Real.measurableSpace rnDerivAux	—	Measurable.ennreal_toReal measurable_from_prod_countable_right' MeasureTheory.Measure.measurable_rnDeriv MeasureTheory.Measure.ext mem_of_mem_measurableAtom measurable_coe MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated measurable_density MeasurableSet.univ
measurable_rnDerivAux_right 📖	mathematical	—	Measurable Real Real.measurableSpace rnDerivAux	—	Measurable.fun_comp measurable_rnDerivAux Measurable.prodMk measurable_const measurable_id'
measurable_rnDeriv_right 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace rnDeriv	—	Measurable.fun_comp measurable_rnDeriv Measurable.prodMk measurable_const measurable_id'
measurable_singularPart 📖	mathematical	—	Measurable MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace MeasureTheory.Measure.singularPart DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	MeasureTheory.Measure.measurable_of_measurable_coe IsFiniteKernel.isSFiniteKernel singularPart_eq_singularPart_measure IsSFiniteKernel.add singularPart_def measurable_coe
measurable_singularPart_fun 📖	mathematical	—	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace ENNReal.instSub ENNReal.ofNNReal Real.toNNReal rnDerivAux ProbabilityTheory.Kernel instAdd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real Real.instSub Real.instOne rnDeriv	—	Measurable.sub ENNReal.instMeasurableSub₂ Measurable.coe_nnreal_ennreal Measurable.real_toNNReal measurable_rnDerivAux Measurable.mul ENNReal.instMeasurableMul₂ Measurable.const_sub ContinuousSub.measurableSub Real.borelSpace IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal measurable_rnDeriv
measurable_singularPart_fun_right 📖	mathematical	—	Measurable ENNReal ENNReal.measurableSpace ENNReal.instSub ENNReal.ofNNReal Real.toNNReal rnDerivAux ProbabilityTheory.Kernel instAdd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real Real.instSub Real.instOne rnDeriv	—	Measurable.comp measurable_singularPart_fun measurable_prodMk_left
measure_mutuallySingularSetSlice 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike mutuallySingularSetSlice instZeroENNReal	—	IsSFiniteKernel.add IsFiniteKernel.isSFiniteKernel withDensity_apply' Measurable.ennreal_ofReal Measurable.const_sub ContinuousSub.measurableSub Real.borelSpace IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal measurable_rnDerivAux MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.lintegral_eq_zero_iff measurable_rnDerivAux_right Filter.EventuallyEq.eq_1 MeasureTheory.ae_restrict_iff MeasurableSet.preimage MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space MeasureTheory.ae_of_all AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add withDensity_one_sub_rnDerivAux
mem_mutuallySingularSetSlice 📖	mathematical	—	Set Set.instMembership mutuallySingularSetSlice Real Real.instLE Real.instOne rnDerivAux ProbabilityTheory.Kernel instAdd	—	mutuallySingularSetSlice.eq_1 Set.mem_setOf
mutuallySingular_singularPart 📖	mathematical	—	MeasureTheory.Measure.MutuallySingular DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike singularPart IsFiniteKernel.isSFiniteKernel	—	MeasureTheory.Measure.MutuallySingular.symm IsFiniteKernel.isSFiniteKernel measurableSet_mutuallySingularSetSlice measure_mutuallySingularSetSlice singularPart_compl_mutuallySingularSetSlice
notMem_mutuallySingularSetSlice 📖	mathematical	—	Set Set.instMembership mutuallySingularSetSlice Real Real.instLT rnDerivAux ProbabilityTheory.Kernel instAdd Real.instOne	—	—
rnDerivAux_le_one 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder	Filter.EventuallyLE Real Real.instLE MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe instFunLike rnDerivAux Pi.instOne Real.instOne	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv_le_one_of_le MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure Filter.univ_mem' ENNReal.toReal_le_of_le_ofReal zero_le_one Real.instZeroLEOneClass ENNReal.ofReal_one MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated density_le_one Eq.trans_le fst_map_id_prod measurable_const
rnDerivAux_nonneg 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder	Real Real.instLE Real.instZero rnDerivAux	—	rnDerivAux.eq_1 ENNReal.toReal_nonneg MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated density_nonneg Eq.trans_le fst_map_id_prod measurable_const
rnDeriv_add 📖	mathematical	—	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike rnDeriv instAdd Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv_add ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite ProbabilityTheory.IsSFiniteKernel.sFinite IsFiniteKernel.isSFiniteKernel MeasureTheory.IsFiniteMeasure.toSigmaFinite MeasureTheory.Measure.HaveLebesgueDecomposition.add_left rnDeriv_eq_rnDeriv_measure ProbabilityTheory.IsFiniteKernel.add Filter.univ_mem' Pi.add_apply coe_add
rnDeriv_add_singularPart 📖	mathematical	—	ProbabilityTheory.Kernel instAdd withDensity IsFiniteKernel.isSFiniteKernel rnDeriv singularPart	—	ext IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.ext Set.inter_union_diff measurableSet_mutuallySingularSetSlice MeasureTheory.measure_union Disjoint.mono Set.inter_subset_right le_rfl Set.disjoint_sdiff_right MeasurableSet.diff singularPart_of_subset_mutuallySingularSetSlice MeasurableSet.inter singularPart_of_subset_compl_mutuallySingularSetSlice Set.diff_subset_iff Set.union_compl_self add_zero withDensity_rnDeriv_of_subset_mutuallySingularSetSlice zero_add withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice add_comm
rnDeriv_def 📖	mathematical	—	rnDeriv ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofReal rnDerivAux ProbabilityTheory.Kernel instAdd Real Real.instSub Real.instOne	—	—
rnDeriv_def' 📖	mathematical	—	rnDeriv ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid ENNReal.ofReal rnDerivAux ProbabilityTheory.Kernel instAdd Real Real.instSub Real.instOne	—	rnDeriv_def
rnDeriv_eq_one_iff_eq 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	Filter.Eventually ENNReal rnDeriv AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv_eq_one_iff_eq MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite ProbabilityTheory.IsSFiniteKernel.sFinite IsFiniteKernel.isSFiniteKernel MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure Filter.eventually_congr Filter.mp_mem rnDeriv_eq_rnDeriv_measure Filter.univ_mem' Pi.one_apply
rnDeriv_eq_rnDeriv_measure 📖	mathematical	—	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike rnDeriv MeasureTheory.Measure.rnDeriv	—	eq_rnDeriv_measure IsFiniteKernel.isSFiniteKernel rnDeriv_add_singularPart measurable_rnDeriv mutuallySingular_singularPart
rnDeriv_eq_top_iff 📖	mathematical	—	rnDeriv Top.top ENNReal instTopENNReal Set Set.instMembership mutuallySingularSet	—	rnDeriv_def AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid zero_add LT.lt.trans_le zero_lt_one Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike
rnDeriv_eq_top_iff' 📖	mathematical	—	rnDeriv Top.top ENNReal instTopENNReal Set Set.instMembership mutuallySingularSetSlice	—	rnDeriv_eq_top_iff mutuallySingularSet.eq_1 mutuallySingularSetSlice.eq_1 Set.mem_setOf
rnDeriv_lt_top 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder rnDeriv Top.top instTopENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv_ne_top MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure rnDeriv_eq_rnDeriv_measure Filter.univ_mem' Ne.lt_top
rnDeriv_ne_top 📖	mathematical	—	Filter.Eventually ENNReal rnDeriv Top.top instTopENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass rnDeriv_lt_top Filter.univ_mem' LT.lt.ne
rnDeriv_pos 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal rnDeriv MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv_pos MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite ProbabilityTheory.IsSFiniteKernel.sFinite IsFiniteKernel.isSFiniteKernel MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.Measure.AbsolutelyContinuous.ae_le rnDeriv_eq_rnDeriv_measure Filter.univ_mem'
rnDeriv_self 📖	mathematical	—	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike rnDeriv Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	Filter.EventuallyEq.trans MeasureTheory.Measure.instOuterMeasureClass rnDeriv_eq_rnDeriv_measure MeasureTheory.Measure.rnDeriv_self MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
rnDeriv_singularPart 📖	mathematical	—	Filter.EventuallyEq ENNReal MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike rnDeriv singularPart IsFiniteKernel.isSFiniteKernel Pi.instZero instZeroENNReal	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.rnDeriv_eq_zero MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite ProbabilityTheory.IsSFiniteKernel.sFinite instIsFiniteKernelSingularPart MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure mutuallySingular_singularPart rnDeriv_eq_rnDeriv_measure Filter.univ_mem'
rnDeriv_toReal_pos 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	Filter.Eventually Real Real.instLT Real.instZero ENNReal.toReal rnDeriv MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.AbsolutelyContinuous.ae_le rnDeriv_ne_top rnDeriv_pos Filter.univ_mem' ENNReal.instCanonicallyOrderedAdd
rnDeriv_withDensity 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike rnDeriv withDensity IsFiniteKernel.isSFiniteKernel	—	IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.instOuterMeasureClass rnDeriv_eq_rnDeriv_measure Measurable.of_uncurry_left Filter.mp_mem MeasureTheory.Measure.rnDeriv_withDensity MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure Filter.univ_mem' withDensity_apply
setLIntegral_rnDeriv 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict rnDeriv Set ENNReal MeasureTheory.Measure.instFunLike	—	MeasureTheory.setLIntegral_congr_fun_ae Filter.Eventually.mono MeasureTheory.Measure.instOuterMeasureClass rnDeriv_eq_rnDeriv_measure MeasureTheory.withDensity_apply MeasureTheory.Measure.withDensity_rnDeriv_eq MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite ProbabilityTheory.IsSFiniteKernel.sFinite IsFiniteKernel.isSFiniteKernel MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
setLIntegral_rnDerivAux 📖	mathematical	MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike instAdd ENNReal.ofReal rnDerivAux Set ENNReal MeasureTheory.Measure.instFunLike	—	le_add_of_nonneg_right instAddLeftMono bot_le MeasureTheory.Measure.absolutelyContinuous_of_le MeasureTheory.Measure.setLIntegral_rnDeriv MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite ProbabilityTheory.IsSFiniteKernel.sFinite IsFiniteKernel.isSFiniteKernel MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure ProbabilityTheory.IsFiniteKernel.add IsSFiniteKernel.add MeasureTheory.setLIntegral_congr_fun_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.Measure.rnDeriv_lt_top Filter.univ_mem' ENNReal.ofReal_toReal LT.lt.ne MeasurableSpace.CountableOrCountablyGenerated.countableOrCountablyGenerated setLIntegral_density Eq.trans_le fst_map_id_prod measurable_const MeasurableSet.univ map_apply' Measurable.prodMk measurable_id' MeasurableSet.prod Set.ext Set.mk_preimage_prod_left
setLIntegral_rnDeriv_le 📖	mathematical	MeasurableSet	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike rnDeriv Set MeasureTheory.Measure.instFunLike	—	MeasureTheory.setLIntegral_congr_fun_ae Filter.Eventually.mono MeasureTheory.Measure.instOuterMeasureClass rnDeriv_eq_rnDeriv_measure MeasureTheory.withDensity_apply' ProbabilityTheory.IsSFiniteKernel.sFinite IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.withDensity_rnDeriv_le
singularPart_compl_mutuallySingularSetSlice 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike singularPart Compl.compl Set.instCompl mutuallySingularSetSlice instZeroENNReal	—	IsSFiniteKernel.add singularPart_def withDensity_apply' measurable_singularPart_fun MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.lintegral_eq_zero_iff measurable_singularPart_fun_right Filter.EventuallyEq.eq_1 MeasureTheory.ae_restrict_iff measurableSet_preimage MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space MeasureTheory.ae_of_all rnDeriv_def ENNReal.ofReal_div_of_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_eq_inv_mul ENNReal.ofReal_mul LT.lt.le mul_assoc mul_inv_cancel₀ LT.lt.ne' one_mul tsub_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub Pi.zero_apply
singularPart_def 📖	mathematical	—	singularPart withDensity ProbabilityTheory.Kernel instAdd IsSFiniteKernel.add ENNReal ENNReal.instSub ENNReal.ofNNReal Real.toNNReal rnDerivAux Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring Real Real.instSub Real.instOne rnDeriv	—	IsSFiniteKernel.add
singularPart_eq_singularPart_measure 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike singularPart IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.singularPart	—	eq_singularPart_measure IsFiniteKernel.isSFiniteKernel rnDeriv_add_singularPart measurable_rnDeriv mutuallySingular_singularPart
singularPart_eq_zero_iff_absolutelyContinuous 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike singularPart IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.instZero MeasureTheory.Measure.AbsolutelyContinuous	—	IsFiniteKernel.isSFiniteKernel rnDeriv_add_singularPart coe_add Pi.add_apply add_zero withDensity_absolutelyContinuous MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular MeasureTheory.Measure.AbsolutelyContinuous.add_left_iff mutuallySingular_singularPart
singularPart_eq_zero_iff_apply_eq_zero 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike singularPart MeasureTheory.Measure.instZero Set ENNReal MeasureTheory.Measure.instFunLike mutuallySingularSetSlice instZeroENNReal	—	MeasureTheory.Measure.measure_univ_eq_zero Set.union_compl_self MeasureTheory.measure_union disjoint_compl_right MeasurableSet.compl measurableSet_mutuallySingularSetSlice singularPart_compl_mutuallySingularSetSlice add_zero
singularPart_eq_zero_iff_measure_eq_zero 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike singularPart IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.instZero Set ENNReal MeasureTheory.Measure.instFunLike mutuallySingularSetSlice instZeroENNReal	—	IsFiniteKernel.isSFiniteKernel rnDeriv_add_singularPart withDensity_rnDeriv_mutuallySingularSetSlice zero_add measurableSet_mutuallySingularSetSlice singularPart_eq_zero_iff_apply_eq_zero
singularPart_of_subset_compl_mutuallySingularSetSlice 📖	mathematical	Set Set.instHasSubset Compl.compl Set.instCompl mutuallySingularSetSlice	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike singularPart IsFiniteKernel.isSFiniteKernel instZeroENNReal	—	MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass IsFiniteKernel.isSFiniteKernel singularPart_compl_mutuallySingularSetSlice
singularPart_of_subset_mutuallySingularSetSlice 📖	mathematical	MeasurableSet Set Set.instHasSubset mutuallySingularSetSlice	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike singularPart IsFiniteKernel.isSFiniteKernel	—	IsFiniteKernel.isSFiniteKernel IsSFiniteKernel.add singularPart_def withDensity_apply' measurable_singularPart_fun MeasureTheory.setLIntegral_congr_fun_ae le_add_of_nonneg_right instAddLeftMono bot_le Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass rnDerivAux_le_one ProbabilityTheory.IsFiniteKernel.add Filter.univ_mem' le_antisymm Real.toNNReal_one sub_self Real.toNNReal_zero MulZeroClass.zero_mul tsub_zero ENNReal.instOrderedSub MeasureTheory.Measure.restrict_add MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter one_mul MeasureTheory.measure_mono_null measure_mutuallySingularSetSlice add_zero
singularPart_self 📖	mathematical	—	singularPart IsFiniteKernel.isSFiniteKernel ProbabilityTheory.Kernel instZero	—	ext IsFiniteKernel.isSFiniteKernel zero_apply singularPart_eq_zero_iff_absolutelyContinuous MeasureTheory.Measure.AbsolutelyContinuous.refl
withDensity_one_sub_rnDerivAux 📖	mathematical	—	withDensity ProbabilityTheory.Kernel instAdd IsSFiniteKernel.add IsFiniteKernel.isSFiniteKernel ENNReal.ofNNReal Real.toNNReal Real Real.instSub Real.instOne rnDerivAux	—	le_add_of_nonneg_right instAddLeftMono bot_le IsSFiniteKernel.add IsFiniteKernel.isSFiniteKernel withDensity.congr_simp ENNReal.ofReal_sub rnDerivAux_nonneg ENNReal.ofReal_one withDensity_sub_add_cancel measurable_const Measurable.ennreal_ofReal measurable_rnDerivAux Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass rnDerivAux_le_one ProbabilityTheory.IsFiniteKernel.add Filter.univ_mem' withDensity_one' ext MeasureTheory.Measure.ext MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure add_comm withDensity_rnDerivAux
withDensity_rnDerivAux 📖	mathematical	—	withDensity ProbabilityTheory.Kernel instAdd IsSFiniteKernel.add IsFiniteKernel.isSFiniteKernel ENNReal.ofNNReal Real.toNNReal rnDerivAux	—	ext IsSFiniteKernel.add IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.ext withDensity_apply' Measurable.coe_nnreal_ennreal Measurable.real_toNNReal measurable_rnDerivAux setLIntegral_rnDerivAux
withDensity_rnDeriv_eq 📖	mathematical	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	withDensity IsFiniteKernel.isSFiniteKernel rnDeriv	—	IsFiniteKernel.isSFiniteKernel withDensity_apply measurable_rnDeriv MeasureTheory.Measure.instOuterMeasureClass rnDeriv_eq_rnDeriv_measure MeasureTheory.withDensity_congr_ae MeasureTheory.Measure.withDensity_rnDeriv_eq MeasureTheory.Measure.haveLebesgueDecomposition_of_sigmaFinite ProbabilityTheory.IsSFiniteKernel.sFinite MeasureTheory.IsFiniteMeasure.toSigmaFinite ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
withDensity_rnDeriv_eq_zero_iff_apply_eq_zero 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike withDensity IsFiniteKernel.isSFiniteKernel rnDeriv MeasureTheory.Measure.instZero Set ENNReal MeasureTheory.Measure.instFunLike Compl.compl Set.instCompl mutuallySingularSetSlice instZeroENNReal	—	IsFiniteKernel.isSFiniteKernel MeasureTheory.Measure.measure_univ_eq_zero Set.union_compl_self MeasureTheory.measure_union disjoint_compl_right MeasurableSet.compl measurableSet_mutuallySingularSetSlice withDensity_rnDeriv_mutuallySingularSetSlice zero_add
withDensity_rnDeriv_eq_zero_iff_measure_eq_zero 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike withDensity IsFiniteKernel.isSFiniteKernel rnDeriv MeasureTheory.Measure.instZero Set ENNReal MeasureTheory.Measure.instFunLike Compl.compl Set.instCompl mutuallySingularSetSlice instZeroENNReal	—	IsFiniteKernel.isSFiniteKernel rnDeriv_add_singularPart singularPart_compl_mutuallySingularSetSlice add_zero MeasurableSet.compl measurableSet_mutuallySingularSetSlice withDensity_rnDeriv_eq_zero_iff_apply_eq_zero
withDensity_rnDeriv_eq_zero_iff_mutuallySingular 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike withDensity IsFiniteKernel.isSFiniteKernel rnDeriv MeasureTheory.Measure.instZero MeasureTheory.Measure.MutuallySingular	—	IsFiniteKernel.isSFiniteKernel rnDeriv_add_singularPart coe_add Pi.add_apply zero_add mutuallySingular_singularPart MeasureTheory.Measure.MutuallySingular.self_iff MeasureTheory.Measure.MutuallySingular.mono_ac MeasureTheory.Measure.MutuallySingular.add_left_iff MeasureTheory.Measure.AbsolutelyContinuous.rfl withDensity_absolutelyContinuous
withDensity_rnDeriv_le 📖	mathematical	—	MeasureTheory.Measure Preorder.toLE PartialOrder.toPreorder MeasureTheory.Measure.instPartialOrder DFunLike.coe ProbabilityTheory.Kernel instFunLike withDensity IsFiniteKernel.isSFiniteKernel rnDeriv	—	MeasureTheory.Measure.le_intro IsFiniteKernel.isSFiniteKernel withDensity_apply' measurable_rnDeriv setLIntegral_rnDeriv_le
withDensity_rnDeriv_mutuallySingularSetSlice 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike withDensity IsFiniteKernel.isSFiniteKernel rnDeriv mutuallySingularSetSlice instZeroENNReal	—	IsFiniteKernel.isSFiniteKernel withDensity_apply' measurable_rnDeriv MeasureTheory.setLIntegral_measure_zero measure_mutuallySingularSetSlice
withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice 📖	mathematical	MeasurableSet Set Set.instHasSubset Compl.compl Set.instCompl mutuallySingularSetSlice	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike withDensity IsFiniteKernel.isSFiniteKernel rnDeriv	—	IsFiniteKernel.isSFiniteKernel IsSFiniteKernel.add instIsSFiniteKernelWithDensityOfNNReal rnDeriv_def' withDensity_one_sub_rnDerivAux withDensity_mul Measurable.real_toNNReal Measurable.const_sub ContinuousSub.measurableSub Real.borelSpace IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal measurable_rnDerivAux measurable_rnDeriv withDensity_apply' Measurable.mul ENNReal.instMeasurableMul₂ Measurable.coe_nnreal_ennreal rnDeriv_def MeasureTheory.setLIntegral_congr_fun ENNReal.ofNNReal_toNNReal ENNReal.ofReal_div_of_pos IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid div_eq_inv_mul ENNReal.ofReal_mul LT.lt.le mul_assoc mul_inv_cancel₀ sub_eq_zero LT.lt.ne' one_mul setLIntegral_rnDerivAux
withDensity_rnDeriv_of_subset_mutuallySingularSetSlice 📖	mathematical	Set Set.instHasSubset mutuallySingularSetSlice	DFunLike.coe MeasureTheory.Measure ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike withDensity IsFiniteKernel.isSFiniteKernel rnDeriv instZeroENNReal	—	MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass IsFiniteKernel.isSFiniteKernel withDensity_rnDeriv_mutuallySingularSetSlice

---

← Back to Index