WithDensity

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

Statistics

Metric	Count
Definitions withDensity	1
Theorems withDensity, instIsSFiniteKernelWithDensityOfNNReal, integral_withDensity, isFiniteKernel_withDensity_of_bounded, isSFiniteKernel_withDensity_of_isFiniteKernel, lintegral_withDensity, withDensity_absolutelyContinuous, withDensity_add_left, withDensity_add_right, withDensity_apply, withDensity_apply', withDensity_congr_ae, withDensity_kernel_sum, withDensity_mul, withDensity_of_not_measurable, withDensity_one, withDensity_one', withDensity_sub_add_cancel, withDensity_tsum, withDensity_zero, withDensity_zero'	21
Total	22

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
withDensity 📖	CompOp	36 math math: rnDeriv_add_singularPart, withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, isSFiniteKernel_withDensity_of_isFiniteKernel, instIsFiniteKernelWithDensityRnDeriv, instIsSFiniteKernelWithDensityOfNNReal, lintegral_withDensity, withDensity_absolutelyContinuous, withDensity_one', withDensity_add_left, MeasureTheory.Measure.compProd_withDensity, withDensity_tsum, withDensity_rnDerivAux, withDensity_one_sub_rnDerivAux, withDensity_rnDeriv_of_subset_mutuallySingularSetSlice, withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice, withDensity_kernel_sum, withDensity_rnDeriv_le, withDensity_apply, withDensity_add_right, withDensity_rnDeriv_eq_zero_iff_mutuallySingular, withDensity_rnDeriv_eq_zero_iff_apply_eq_zero, withDensity_congr_ae, withDensity_one, withDensity_rnDeriv_eq, withDensity_rnDeriv_mutuallySingularSetSlice, withDensity_zero, singularPart_def, withDensity_apply', IsSFiniteKernel.withDensity, withDensity_mul, withDensity_zero', integral_withDensity, withDensity_sub_add_cancel, isFiniteKernel_withDensity_of_bounded, rnDeriv_withDensity, withDensity_of_not_measurable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsSFiniteKernelWithDensityOfNNReal 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel withDensity ENNReal.ofNNReal	—	IsSFiniteKernel.withDensity ENNReal.coe_ne_top
integral_withDensity 📖	mathematical	Measurable NNReal Prod.instMeasurableSpace NNReal.measurableSpace	MeasureTheory.integral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike withDensity ENNReal.ofNNReal 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 MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal NNReal.instDistribMulActionOfReal Module.toDistribMulAction Real Real.semiring ESeminormedAddCommMonoid.toAddCommMonoid NormedSpace.toModule Real.normedField	—	withDensity_apply Measurable.coe_nnreal_ennreal integral_withDensity_eq_integral_smul Measurable.fun_comp Measurable.prodMk measurable_const measurable_id'
isFiniteKernel_withDensity_of_bounded 📖	mathematical	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder	ProbabilityTheory.IsFiniteKernel withDensity IsFiniteKernel.isSFiniteKernel	—	IsFiniteKernel.isSFiniteKernel ENNReal.mul_lt_top Ne.lt_top bound_lt_top withDensity_apply' MeasureTheory.lintegral_mono MeasureTheory.Measure.restrict_univ MeasureTheory.lintegral_const le_imp_le_of_le_of_le mul_le_mul_right IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid measure_le_bound le_refl withDensity_of_not_measurable ProbabilityTheory.isFiniteKernel_zero
isSFiniteKernel_withDensity_of_isFiniteKernel 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel withDensity IsFiniteKernel.isSFiniteKernel	—	IsFiniteKernel.isSFiniteKernel Real.instIsStrictOrderedRing Nat.le_of_ceil_le LE.le.trans ENNReal.le_ofReal_iff_toReal_le Nat.cast_zero IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instZeroLEOneClass RCLike.charZero_rclike zero_le Nat.instCanonicallyOrderedAdd le_of_eq ENNReal.ofReal_natCast min_eq_left le_add_of_nonneg_right ENNReal.instIsOrderedAddMonoid zero_le_one IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing tsub_self ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub Pi.summable not_lt Finset.mem_range summable_of_ne_finset_zero SummationFilter.instHasSupportOfLeAtTop SummationFilter.instLeAtTopUnconditional tsum_apply SummationFilter.instNeBotUnconditional Pi.t2Space ENNReal.instT2Space ENNReal.tsum_eq_liminf_sum_nat CharP.cast_eq_zero CharP.ofCharZero ENNReal.instCharZero inf_of_le_right Finset.sum_range_succ add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.cast_add Nat.cast_one Filter.Tendsto.liminf_eq ENNReal.instOrderTopology Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.congr' Filter.EventuallyEq.eq_1 Filter.eventually_atTop tendsto_const_nhds instCountableNat withDensity_tsum Measurable.sub ENNReal.instMeasurableSub₂ Measurable.inf_const ContinuousInf.measurableInf ENNReal.borelSpace TopologicalLattice.toContinuousInf LinearOrder.topologicalLattice OrderTopology.to_orderClosedTopology isSFiniteKernel_sum isFiniteKernel_withDensity_of_bounded ENNReal.coe_ne_top tsub_le_self min_le_right withDensity_of_not_measurable ProbabilityTheory.isFiniteKernel_zero
lintegral_withDensity 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike withDensity Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	withDensity_apply MeasureTheory.lintegral_withDensity_eq_lintegral_mul Measurable.of_uncurry_left
withDensity_absolutelyContinuous 📖	mathematical	—	MeasureTheory.Measure.AbsolutelyContinuous DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike withDensity	—	withDensity_apply MeasureTheory.withDensity_absolutelyContinuous withDensity_of_not_measurable
withDensity_add_left 📖	mathematical	—	withDensity ProbabilityTheory.Kernel instAdd IsSFiniteKernel.add	—	IsSFiniteKernel.add ext MeasureTheory.Measure.ext withDensity_apply MeasureTheory.withDensity_add_measure withDensity_of_not_measurable zero_add
withDensity_add_right 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	withDensity Pi.instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ProbabilityTheory.Kernel instAdd	—	ext MeasureTheory.Measure.ext coe_add Pi.add_apply withDensity_apply Measurable.add ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd MeasureTheory.withDensity_add_right Measurable.fun_comp Measurable.prodMk measurable_const measurable_id'
withDensity_apply 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike withDensity MeasureTheory.Measure.withDensity	—	withDensity.eq_1
withDensity_apply' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike withDensity MeasureTheory.lintegral MeasureTheory.Measure.restrict	—	withDensity_apply MeasureTheory.withDensity_apply' ProbabilityTheory.IsSFiniteKernel.sFinite
withDensity_congr_ae 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	withDensity	—	MeasureTheory.Measure.instOuterMeasureClass ext MeasureTheory.Measure.ext withDensity_apply MeasureTheory.withDensity_congr_ae
withDensity_kernel_sum 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	withDensity sum isSFiniteKernel_sum	—	isSFiniteKernel_sum ext withDensity_apply MeasureTheory.withDensity_sum withDensity_of_not_measurable sum.congr_simp sum_zero
withDensity_mul 📖	mathematical	Measurable NNReal Prod.instMeasurableSpace NNReal.measurableSpace ENNReal ENNReal.measurableSpace	withDensity Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring ENNReal.ofNNReal instIsSFiniteKernelWithDensityOfNNReal	—	ext instIsSFiniteKernelWithDensityOfNNReal withDensity_apply Measurable.mul ENNReal.instMeasurableMul₂ Measurable.coe_nnreal_ennreal MeasureTheory.withDensity_mul Measurable.fun_comp Measurable.prodMk measurable_const measurable_id' Measurable.comp measurable_coe_nnreal_ennreal
withDensity_of_not_measurable 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	withDensity ProbabilityTheory.Kernel instZero	—	—
withDensity_one 📖	mathematical	—	withDensity Pi.instOne ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	ext MeasureTheory.Measure.ext withDensity_apply measurable_const MeasureTheory.withDensity_one
withDensity_one' 📖	mathematical	—	withDensity ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	withDensity_one
withDensity_sub_add_cancel 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace Filter.EventuallyLE Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	instAdd withDensity ENNReal.instSub	—	MeasureTheory.Measure.instOuterMeasureClass withDensity_add_right Measurable.sub ENNReal.instMeasurableSub₂ withDensity_congr_ae Measurable.add ContinuousAdd.measurableMul₂ ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instContinuousAdd Filter.mp_mem Filter.univ_mem' Pi.add_apply tsub_add_cancel_iff_le ENNReal.instCanonicallyOrderedAdd ENNReal.instOrderedSub
withDensity_tsum 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	withDensity tsum Pi.addCommMonoid ENNReal.instAddCommMonoid Pi.topologicalSpace ENNReal.instTopologicalSpace SummationFilter.unconditional sum	—	Pi.summable ENNReal.summable ext MeasureTheory.Measure.ext sum_apply' withDensity_apply' tsum_apply SummationFilter.instNeBotUnconditional Pi.t2Space ENNReal.instT2Space Measurable.ennreal_tsum' MeasureTheory.lintegral_tsum Measurable.aemeasurable Measurable.fun_comp Measurable.prodMk measurable_const measurable_id'
withDensity_zero 📖	mathematical	—	withDensity Pi.instZero ENNReal instZeroENNReal ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext withDensity_apply measurable_const MeasureTheory.withDensity_zero
withDensity_zero' 📖	mathematical	—	withDensity ENNReal instZeroENNReal ProbabilityTheory.Kernel instZero	—	withDensity_zero

ProbabilityTheory.Kernel.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
withDensity 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.withDensity	—	instCountableNat ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.isSFiniteKernel_sum ProbabilityTheory.Kernel.withDensity_kernel_sum ProbabilityTheory.Kernel.kernel_sum_seq ProbabilityTheory.Kernel.isSFiniteKernel_withDensity_of_isFiniteKernel

---

← Back to Index