Density

📁 Source: Mathlib/Probability/Kernel/Disintegration/Density.lean

Statistics

Metric	Count
Definitions density, densityProcess	2
Theorems condExp_densityProcess, densityProcess_antitone_kernel_right, densityProcess_def, densityProcess_empty, densityProcess_fst_univ, densityProcess_fst_univ_ae, densityProcess_le_one, densityProcess_mono_kernel_left, densityProcess_mono_set, densityProcess_nonneg, density_ae_eq_limitProcess, density_fst_univ, density_le_one, density_mono_set, density_nonneg, eLpNorm_densityProcess_le, eLpNorm_density_le, integrable_density, integrable_densityProcess, integral_density, integral_densityProcess, lintegral_density, martingale_densityProcess, meas_countablePartitionSet_le_of_fst_le, measurable_countableFiltration_densityProcess, measurable_density, measurable_densityProcess, measurable_densityProcess_aux, measurable_densityProcess_countableFiltration_aux, measurable_densityProcess_left, measurable_densityProcess_right, measurable_density_left, measurable_density_right, memL1_limitProcess_densityProcess, setIntegral_density, setIntegral_densityProcess, setIntegral_densityProcess_of_le, setIntegral_densityProcess_of_mem, setIntegral_density_of_measurableSet, setLIntegral_density, stronglyAdapted_densityProcess, stronglyMeasurable_countableFiltration_densityProcess, tendsto_densityProcess_atTop_empty_of_antitone, tendsto_densityProcess_atTop_of_antitone, tendsto_densityProcess_fst_atTop_ae_of_monotone, tendsto_densityProcess_fst_atTop_univ_of_monotone, tendsto_densityProcess_limitProcess, tendsto_density_atTop_ae_of_antitone, tendsto_density_fst_atTop_ae_of_monotone, tendsto_eLpNorm_one_densityProcess_limitProcess, tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, tendsto_integral_density_of_antitone, tendsto_integral_density_of_monotone, tendsto_m_density, tendsto_setIntegral_densityProcess	55
Total	57

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
density 📖	CompOp	23 math math: tendsto_m_density, density_fst_univ, density_le_one, tendsto_density_atTop_ae_of_antitone, measurable_density, tendsto_integral_density_of_monotone, setIntegral_density_of_measurableSet, tendsto_integral_density_of_antitone, density_ae_eq_limitProcess, setLIntegral_density, integrable_density, isRatCondKernelCDF_density_Iic, integral_density, lintegral_density, tendsto_setIntegral_densityProcess, isRatCondKernelCDFAux_density_Iic, measurable_density_left, eLpNorm_density_le, density_nonneg, setIntegral_density, density_mono_set, measurable_density_right, tendsto_density_fst_atTop_ae_of_monotone
densityProcess 📖	CompOp	34 math math: tendsto_m_density, densityProcess_antitone_kernel_right, densityProcess_mono_set, densityProcess_mono_kernel_left, densityProcess_le_one, densityProcess_empty, setIntegral_densityProcess_of_mem, integrable_densityProcess, martingale_densityProcess, setIntegral_densityProcess_of_le, measurable_densityProcess, measurable_densityProcess_left, memL1_limitProcess_densityProcess, tendsto_densityProcess_atTop_empty_of_antitone, measurable_countableFiltration_densityProcess, densityProcess_fst_univ_ae, density_ae_eq_limitProcess, setIntegral_densityProcess, integral_densityProcess, densityProcess_nonneg, tendsto_densityProcess_fst_atTop_univ_of_monotone, tendsto_eLpNorm_one_densityProcess_limitProcess, tendsto_setIntegral_densityProcess, stronglyMeasurable_countableFiltration_densityProcess, condExp_densityProcess, tendsto_densityProcess_limitProcess, tendsto_densityProcess_fst_atTop_ae_of_monotone, eLpNorm_densityProcess_le, densityProcess_fst_univ, measurable_densityProcess_right, tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, densityProcess_def, stronglyAdapted_densityProcess, tendsto_densityProcess_atTop_of_antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condExp_densityProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe instFunLike MeasureTheory.condExp MeasureTheory.Filtration.seq Nat.instPreorder ProbabilityTheory.countableFiltration Real.normedAddCommGroup Real.instCompleteSpace InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal densityProcess	—	Filter.EventuallyEq.symm Real.instCompleteSpace MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq MeasureTheory.Filtration.le MeasureTheory.sigmaFinite_of_sigmaFiniteFiltration MeasureTheory.IsFiniteMeasure.sigmaFiniteFiltration ProbabilityTheory.IsFiniteKernel.isFiniteMeasure integrable_densityProcess MeasureTheory.Integrable.integrableOn setIntegral_densityProcess setIntegral_densityProcess_of_le MeasureTheory.StronglyMeasurable.aestronglyMeasurable stronglyMeasurable_countableFiltration_densityProcess
densityProcess_antitone_kernel_right 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	Real Real.instLE densityProcess	—	meas_countablePartitionSet_le_of_fst_le nonpos_iff_eq_zero ENNReal.instCanonicallyOrderedAdd LE.le.trans Eq.le ENNReal.zero_div ENNReal.toReal_mono eq_top_mono ENNReal.div_le_div le_refl MeasureTheory.Measure.measure_mono_left
densityProcess_def 📖	mathematical	—	densityProcess ENNReal.toReal ENNReal DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike SProd.sprod Set.instSProd MeasurableSpace.countablePartitionSet	—	—
densityProcess_empty 📖	mathematical	—	densityProcess Set Set.instEmptyCollection Real Real.instZero	—	Set.prod_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass ENNReal.zero_div
densityProcess_fst_univ 📖	mathematical	—	densityProcess fst Set.univ Real ENNReal DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike MeasurableSpace.countablePartitionSet instZeroENNReal LinearOrder.toDecidableEq ENNReal.instLinearOrder Real.instZero Real.instOne	—	densityProcess.eq_1 ENNReal.zero_div ENNReal.toReal_div div_zero fst_apply' MeasurableSpace.measurableSet_countablePartitionSet Set.ext ENNReal.div_self MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
densityProcess_fst_univ_ae 📖	mathematical	—	Filter.Eventually Real densityProcess fst Set.univ Real.instOne MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.ae_iff NeZero.charZero_one RCLike.charZero_rclike densityProcess_fst_univ MeasureTheory.measure_mono_null MeasurableSpace.countablePartitionSet_mem MeasurableSpace.mem_countablePartitionSet MeasureTheory.measure_biUnion Set.Finite.countable MeasurableSpace.finite_countablePartition MeasurableSpace.disjoint_countablePartition Set.iUnion_congr_Prop Set.iUnion_true MeasurableSpace.measurableSet_countablePartition Set.iUnion_of_empty instIsEmptyFalse Prop.countable
densityProcess_le_one 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	Real Real.instLE densityProcess Real.instOne	—	ENNReal.toReal_le_of_le_ofReal zero_le_one Real.instZeroLEOneClass ENNReal.div_le_of_le_mul ENNReal.ofReal_one one_mul meas_countablePartitionSet_le_of_fst_le
densityProcess_mono_kernel_left 📖	mathematical	ProbabilityTheory.Kernel Prod.instMeasurableSpace Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	Real Real.instLE densityProcess	—	ENNReal.toReal_div div_zero meas_countablePartitionSet_le_of_fst_le ENNReal.toReal_mono eq_top_mono ENNReal.div_le_div MeasureTheory.Measure.measure_mono_left le_refl
densityProcess_mono_set 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst Set Set.instHasSubset	Real Real.instLE densityProcess	—	eq_or_ne ENNReal.toReal_div div_zero ENNReal.toReal_mono eq_top_mono meas_countablePartitionSet_le_of_fst_le ENNReal.div_le_div MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.prod_mono subset_refl Set.instReflSubset le_refl
densityProcess_nonneg 📖	mathematical	—	Real Real.instLE Real.instZero densityProcess	—	ENNReal.toReal_nonneg
density_ae_eq_limitProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	Filter.EventuallyEq Real MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe instFunLike density MeasureTheory.Filtration.limitProcess Nat.instPreorder Real.instZero UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace densityProcess ProbabilityTheory.countableFiltration	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass tendsto_densityProcess_limitProcess Filter.univ_mem' Filter.Tendsto.limsup_eq instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
density_fst_univ 📖	mathematical	—	Filter.Eventually Real density fst Set.univ Real.instOne MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	MeasureTheory.Measure.instOuterMeasureClass densityProcess_fst_univ_ae Filter.mp_mem MeasureTheory.ae_all_iff instCountableNat Filter.univ_mem' Filter.limsup_const Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat
density_le_one 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	Real Real.instLE density Real.instOne	—	Filter.limsup_le_of_le Filter.isCoboundedUnder_le_of_le Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat densityProcess_nonneg Filter.Eventually.of_forall densityProcess_le_one
density_mono_set 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst Set Set.instHasSubset	Real Real.instLE density	—	Filter.limsup_le_limsup Filter.Eventually.of_forall densityProcess_mono_set Filter.isCoboundedUnder_le_of_le Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat densityProcess_nonneg Filter.isBoundedUnder_of densityProcess_le_one
density_nonneg 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	Real Real.instLE Real.instZero density	—	Filter.le_limsup_of_frequently_le Filter.Frequently.of_forall Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat densityProcess_nonneg Filter.isBoundedUnder_of densityProcess_le_one
eLpNorm_densityProcess_le 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	ENNReal ENNReal.instPartialOrder MeasureTheory.eLpNorm Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm densityProcess AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe MeasureTheory.Measure instFunLike Set MeasureTheory.Measure.instFunLike Set.univ	—	LE.le.trans MeasureTheory.eLpNorm_le_of_ae_bound MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid densityProcess_nonneg densityProcess_le_one inv_one ENNReal.rpow_one ENNReal.ofReal_one mul_one
eLpNorm_density_le 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	ENNReal ENNReal.instPartialOrder MeasureTheory.eLpNorm Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm density AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe MeasureTheory.Measure instFunLike Set MeasureTheory.Measure.instFunLike Set.univ	—	LE.le.trans MeasureTheory.eLpNorm_le_of_ae_bound MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid density_nonneg density_le_one inv_one ENNReal.rpow_one ENNReal.ofReal_one mul_one
integrable_density 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing density DFunLike.coe MeasureTheory.Measure instFunLike	—	MeasureTheory.memLp_one_iff_integrable Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_density_right LE.le.trans_lt eLpNorm_density_le MeasureTheory.measure_lt_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
integrable_densityProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.Integrable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace SeminormedAddGroup.toContinuousENorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing densityProcess DFunLike.coe MeasureTheory.Measure instFunLike	—	MeasureTheory.memLp_one_iff_integrable Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_densityProcess_right LE.le.trans_lt eLpNorm_densityProcess_le MeasureTheory.measure_lt_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
integral_density 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe MeasureTheory.Measure instFunLike density MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd Set.univ	—	MeasureTheory.setIntegral_univ setIntegral_density_of_measurableSet MeasurableSet.univ
integral_densityProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe MeasureTheory.Measure instFunLike densityProcess MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd Set.univ	—	MeasureTheory.setIntegral_univ setIntegral_densityProcess MeasurableSet.univ
lintegral_density 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.lintegral DFunLike.coe MeasureTheory.Measure instFunLike ENNReal.ofReal density Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike SProd.sprod Set.instSProd Set.univ	—	MeasureTheory.setLIntegral_univ setLIntegral_density MeasurableSet.univ
martingale_densityProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.Martingale Real Nat.instPreorder Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal Real.instCompleteSpace densityProcess ProbabilityTheory.countableFiltration DFunLike.coe MeasureTheory.Measure instFunLike	—	MeasureTheory.Measure.instOuterMeasureClass Real.instCompleteSpace stronglyAdapted_densityProcess condExp_densityProcess
meas_countablePartitionSet_le_of_fst_le 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst	ENNReal ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set MeasureTheory.Measure.instFunLike instFunLike SProd.sprod Set.instSProd MeasurableSpace.countablePartitionSet	—	fst_apply' MeasurableSpace.measurableSet_countablePartitionSet MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass
measurable_countableFiltration_densityProcess 📖	mathematical	MeasurableSet	Measurable Real MeasureTheory.Filtration.seq Nat.instPreorder ProbabilityTheory.countableFiltration Real.measurableSpace densityProcess	—	Measurable.ennreal_toReal Measurable.comp measurable_densityProcess_countableFiltration_aux measurable_prodMk_left
measurable_density 📖	mathematical	MeasurableSet	Measurable Real Prod.instMeasurableSpace Real.measurableSpace density	—	Measurable.limsup Real.borelSpace instOrderTopologyReal instSecondCountableTopologyReal measurable_densityProcess
measurable_densityProcess 📖	mathematical	MeasurableSet	Measurable Real Prod.instMeasurableSpace Real.measurableSpace densityProcess	—	Measurable.ennreal_toReal measurable_densityProcess_aux
measurable_densityProcess_aux 📖	mathematical	MeasurableSet	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike SProd.sprod Set.instSProd MeasurableSpace.countablePartitionSet	—	Measurable.mono measurable_densityProcess_countableFiltration_aux sup_le_sup le_rfl MeasurableSpace.comap_mono MeasureTheory.Filtration.le
measurable_densityProcess_countableFiltration_aux 📖	mathematical	MeasurableSet	Measurable ENNReal MeasurableSpace.prod MeasureTheory.Filtration.seq Nat.instPreorder ProbabilityTheory.countableFiltration ENNReal.measurableSpace DivInvMonoid.toDiv ENNReal.instDivInvMonoid DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike SProd.sprod Set.instSProd MeasurableSpace.countablePartitionSet	—	Measurable.div measurableDiv₂_of_mul_inv ENNReal.instMeasurableMul₂ ENNReal.instMeasurableInv measurable_from_prod_countable_left Finite.to_countable MeasurableSpace.instFinite_countablePartition measurableSingleton_of_standardBorel standardBorelSpace_of_discreteMeasurableSpace instDiscreteMeasurableSpace measurable_coe MeasurableSet.prod MeasurableSpace.measurableSet_countablePartition Subtype.prop Measurable.comp MeasurableSpace.countablePartitionSet_mem Measurable.prodMk measurable_fst ProbabilityTheory.measurable_countablePartitionSet_subtype measurable_snd
measurable_densityProcess_left 📖	mathematical	MeasurableSet	Measurable Real Real.measurableSpace densityProcess	—	Measurable.comp measurable_densityProcess Measurable.prodMk measurable_id measurable_const
measurable_densityProcess_right 📖	mathematical	MeasurableSet	Measurable Real Real.measurableSpace densityProcess	—	Measurable.comp measurable_densityProcess Measurable.prodMk measurable_const measurable_id
measurable_density_left 📖	mathematical	MeasurableSet	Measurable Real Real.measurableSpace density	—	Measurable.comp measurable_density measurable_prodMk_right
measurable_density_right 📖	mathematical	MeasurableSet	Measurable Real Real.measurableSpace density	—	Measurable.comp measurable_density measurable_prodMk_left
memL1_limitProcess_densityProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.MemLp Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Real.pseudoMetricSpace MeasureTheory.Filtration.limitProcess Nat.instPreorder Real.instZero densityProcess ProbabilityTheory.countableFiltration DFunLike.coe MeasureTheory.Measure instFunLike ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.Submartingale.memLp_limitProcess MeasureTheory.Martingale.submartingale Real.instCompleteSpace martingale_densityProcess LE.le.trans_eq eLpNorm_densityProcess_le ENNReal.coe_toNNReal MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
setIntegral_density 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure instFunLike density MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd	—	isFiniteKernel_of_isFiniteKernel_fst ProbabilityTheory.isFiniteKernel_of_le Set.setOf_exists MeasurableSpace.generateFrom_iUnion_measurableSet ProbabilityTheory.iSup_countableFiltration isPiSystem_iUnion_of_monotone MeasurableSpace.isPiSystem_measurableSet MeasureTheory.Filtration.mono MeasurableSpace.induction_on_inter MeasureTheory.Measure.restrict_empty MeasureTheory.integral_zero_measure Set.empty_prod MeasureTheory.measureReal_empty setIntegral_density_of_measurableSet MeasureTheory.integral_add_compl integrable_density Set.prod_diff_prod Set.compl_eq_univ_diff sdiff_self Set.prod_empty Set.empty_union MeasureTheory.measureReal_def MeasureTheory.measure_diff MeasurableSet.nullMeasurableSet MeasurableSet.prod MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure ENNReal.toReal_sub_of_le MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass eq_tsub_iff_add_eq_of_le AddGroup.existsAddOfLE IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid AddGroup.toOrderedSub covariant_swap_add_of_covariant_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le ENNReal.toReal_mono Set.prod_mono subset_refl Set.instReflSubset add_comm integral_density MeasureTheory.integral_iUnion instCountableNat MeasureTheory.Integrable.integrableOn ENNReal.tsum_toReal_eq Set.iUnion_prod_const MeasureTheory.measure_iUnion Pairwise.mono Set.Disjoint.set_prod_left
setIntegral_densityProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet MeasureTheory.Filtration.seq Nat.instPreorder ProbabilityTheory.countableFiltration	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure instFunLike densityProcess MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd	—	isFiniteKernel_of_isFiniteKernel_fst ProbabilityTheory.isFiniteKernel_of_le MeasurableSpace.measurableSet_generateFrom_countablePartition_iff Set.sUnion_eq_iUnion MeasurableSpace.disjoint_countablePartition MeasureTheory.integral_iUnion Finite.to_countable Finite.of_fintype MeasurableSpace.measurableSet_countablePartition MeasureTheory.Integrable.integrableOn integrable_densityProcess Set.iUnion_prod_const MeasureTheory.measureReal_def MeasureTheory.measure_iUnion MeasurableSet.prod ENNReal.tsum_toReal_eq MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure setIntegral_densityProcess_of_mem
setIntegral_densityProcess_of_le 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet MeasureTheory.Filtration.seq Nat.instPreorder ProbabilityTheory.countableFiltration	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure instFunLike densityProcess MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd	—	setIntegral_densityProcess MeasureTheory.Filtration.mono
setIntegral_densityProcess_of_mem 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet Set Set.instMembership MeasurableSpace.countablePartition	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure instFunLike densityProcess MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set.instSProd	—	isFiniteKernel_of_isFiniteKernel_fst ProbabilityTheory.isFiniteKernel_of_le MeasurableSpace.measurableSet_countablePartition MeasureTheory.integral_toReal Measurable.aemeasurable Measurable.comp measurable_densityProcess_aux measurable_prodMk_left MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass ENNReal.instCanonicallyOrderedAdd LE.le.trans Eq.le MeasureTheory.measure_mono_null fst_apply' MeasurableSpace.measurableSet_countablePartitionSet ENNReal.zero_div Ne.lt_top ENNReal.div_ne_top MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.setLIntegral_congr_fun MeasurableSpace.countablePartitionSet_of_mem MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter MulZeroClass.mul_zero div_eq_mul_inv mul_assoc ENNReal.inv_mul_cancel mul_one
setIntegral_density_of_measurableSet 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet MeasureTheory.Filtration.seq Nat.instPreorder ProbabilityTheory.countableFiltration	MeasureTheory.integral Real Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure instFunLike density MeasureTheory.Measure.real Prod.instMeasurableSpace SProd.sprod Set Set.instSProd	—	tendsto_setIntegral_densityProcess Filter.Tendsto.limsup_eq instOrderTopologyReal Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.limsup_const Filter.limsup_congr setIntegral_densityProcess_of_le setIntegral_densityProcess
setLIntegral_density 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure instFunLike ENNReal.ofReal density Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike SProd.sprod Set.instSProd	—	isFiniteKernel_of_isFiniteKernel_fst ProbabilityTheory.isFiniteKernel_of_le MeasureTheory.ofReal_integral_eq_lintegral_ofReal MeasureTheory.Integrable.restrict integrable_density MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass density_nonneg setIntegral_density MeasureTheory.measureReal_def ENNReal.ofReal_toReal MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
stronglyAdapted_densityProcess 📖	mathematical	MeasurableSet	MeasureTheory.StronglyAdapted Nat.instPreorder Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace ProbabilityTheory.countableFiltration densityProcess	—	stronglyMeasurable_countableFiltration_densityProcess
stronglyMeasurable_countableFiltration_densityProcess 📖	mathematical	MeasurableSet	MeasureTheory.StronglyMeasurable Real UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Filtration.seq Nat.instPreorder ProbabilityTheory.countableFiltration densityProcess	—	Measurable.stronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_countableFiltration_densityProcess
tendsto_densityProcess_atTop_empty_of_antitone 📖	mathematical	Antitone Set Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iInter Set.instEmptyCollection MeasurableSet	Filter.Tendsto Real densityProcess Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	ENNReal.toReal_div div_zero Set.prod_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass T5Space.toT1Space T6Space.toT5Space instT6SpaceOfMetrizableSpace EMetricSpace.metrizableSpace Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.Tendsto.comp ENNReal.tendsto_toReal ENNReal.div_eq_top Mathlib.Tactic.Push.not_and_eq instIsEmptyFalse ENNReal.Tendsto.div_const MeasureTheory.tendsto_measure_iInter_atTop instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace MeasurableSet.nullMeasurableSet MeasurableSet.prod MeasurableSpace.measurableSet_countablePartitionSet Set.prod_mono_right MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure
tendsto_densityProcess_atTop_of_antitone 📖	mathematical	Antitone Set Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iInter Set.instEmptyCollection MeasurableSet	Filter.Tendsto Real densityProcess Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	densityProcess_empty tendsto_densityProcess_atTop_empty_of_antitone
tendsto_densityProcess_fst_atTop_ae_of_monotone 📖	mathematical	Monotone Set Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iUnion Set.univ	Filter.Eventually Filter.Tendsto Real densityProcess fst Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass densityProcess_fst_univ_ae Filter.univ_mem' tendsto_densityProcess_fst_atTop_univ_of_monotone
tendsto_densityProcess_fst_atTop_univ_of_monotone 📖	mathematical	Monotone Set Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iUnion Set.univ	Filter.Tendsto Real densityProcess fst Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace	—	Filter.Tendsto.comp ENNReal.tendsto_toReal ENNReal.div_eq_top Mathlib.Tactic.Push.not_and_eq fst_apply' MeasurableSpace.measurableSet_countablePartitionSet MeasureTheory.measure_mono_null MeasureTheory.Measure.instOuterMeasureClass eq_top_mono MeasureTheory.measure_mono ENNReal.zero_div T5Space.toT1Space ENNReal.instT5Space Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Set.ext ENNReal.Tendsto.div_const Set.prod_iUnion MeasureTheory.tendsto_measure_iUnion_atTop instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace Monotone.set_prod monotone_const
tendsto_densityProcess_limitProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	Filter.Eventually Filter.Tendsto Real densityProcess Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Filtration.limitProcess Real.instZero ProbabilityTheory.countableFiltration DFunLike.coe MeasureTheory.Measure instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Submartingale.ae_tendsto_limitProcess ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.Martingale.submartingale Real.instCompleteSpace martingale_densityProcess LE.le.trans_eq eLpNorm_densityProcess_le ENNReal.coe_toNNReal MeasureTheory.measure_ne_top
tendsto_density_atTop_ae_of_antitone 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst Antitone Set Nat.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iInter Set.instEmptyCollection MeasurableSet	Filter.Eventually Filter.Tendsto Real density Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe instFunLike	—	MeasureTheory.tendsto_of_integral_tendsto_of_antitone integrable_density MeasureTheory.integrable_const ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.integral_zero tendsto_integral_density_of_antitone MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass density_mono_set density_nonneg
tendsto_density_fst_atTop_ae_of_monotone 📖	mathematical	Monotone Set Nat.instPreorder PartialOrder.toPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iUnion Set.univ MeasurableSet	Filter.Eventually Filter.Tendsto Real density fst Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instOne MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	MeasureTheory.tendsto_of_integral_tendsto_of_monotone integrable_density le_rfl IsFiniteKernel.fst MeasureTheory.integrable_const ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.integral_const Real.instCompleteSpace smul_eq_mul mul_one fst_apply' MeasurableSet.univ tendsto_integral_density_of_monotone MeasureTheory.ae_of_all MeasureTheory.Measure.instOuterMeasureClass density_mono_set density_le_one
tendsto_eLpNorm_one_densityProcess_limitProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	Filter.Tendsto ENNReal MeasureTheory.eLpNorm Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Pi.instSub Real.instSub densityProcess MeasureTheory.Filtration.limitProcess Nat.instPreorder Real.instZero Real.pseudoMetricSpace ProbabilityTheory.countableFiltration DFunLike.coe MeasureTheory.Measure instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal Filter.atTop nhds ENNReal.instTopologicalSpace instZeroENNReal	—	MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcess ProbabilityTheory.IsFiniteKernel.isFiniteMeasure MeasureTheory.Martingale.submartingale Real.instCompleteSpace martingale_densityProcess MeasureTheory.uniformIntegrable_of le_rfl ENNReal.one_ne_top Measurable.aestronglyMeasurable PseudoEMetricSpace.pseudoMetrizableSpace instSecondCountableTopologyReal BorelSpace.opensMeasurable Real.borelSpace measurable_densityProcess_right Nat.instAtLeastTwoHAddOfNat Set.ext LE.le.trans_lt densityProcess_nonneg Real.nnnorm_of_nonneg Nat.cast_one densityProcess_le_one one_lt_two LinearOrderedCommMonoidWithZero.toZeroLeOneClass NeZero.charZero_one IsStrictOrderedRing.toCharZero NNReal.instIsStrictOrderedRing IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd NNReal.addLeftMono Set.indicator_empty MeasureTheory.eLpNorm_zero' ENNReal.instCanonicallyOrderedAdd
tendsto_eLpNorm_one_restrict_densityProcess_limitProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	Filter.Tendsto ENNReal MeasureTheory.eLpNorm Real ContinuousENorm.toENorm UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddGroup.toPseudoMetricSpace SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing Real.normedCommRing SeminormedAddGroup.toContinuousENorm Pi.instSub Real.instSub densityProcess MeasureTheory.Filtration.limitProcess Nat.instPreorder Real.instZero Real.pseudoMetricSpace ProbabilityTheory.countableFiltration DFunLike.coe MeasureTheory.Measure instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal MeasureTheory.Measure.restrict Filter.atTop nhds ENNReal.instTopologicalSpace instZeroENNReal	—	tendsto_of_tendsto_of_tendsto_of_le_of_le ENNReal.instOrderTopology tendsto_const_nhds tendsto_eLpNorm_one_densityProcess_limitProcess zero_le ENNReal.instCanonicallyOrderedAdd MeasureTheory.eLpNorm_restrict_le
tendsto_integral_density_of_antitone 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst Antitone Set Nat.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iInter Set.instEmptyCollection MeasurableSet	Filter.Tendsto Real MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe MeasureTheory.Measure instFunLike density Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace Real.instZero	—	isFiniteKernel_of_isFiniteKernel_fst ProbabilityTheory.isFiniteKernel_of_le integral_density ENNReal.toReal_zero ENNReal.continuousAt_toReal ENNReal.zero_ne_top Filter.Tendsto.comp ContinuousAt.tendsto MeasureTheory.tendsto_measure_iInter_atTop instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace MeasurableSet.nullMeasurableSet MeasurableSet.prod Antitone.set_prod antitone_const MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure Set.prod_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass
tendsto_integral_density_of_monotone 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst Monotone Set Nat.instPreorder OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra Set.iUnion Set.univ MeasurableSet	Filter.Tendsto Real MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal DFunLike.coe MeasureTheory.Measure instFunLike density Filter.atTop nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace MeasureTheory.Measure.real Prod.instMeasurableSpace	—	isFiniteKernel_of_isFiniteKernel_fst ProbabilityTheory.isFiniteKernel_of_le integral_density ContinuousOn.continuousAt ENNReal.continuousOn_toReal mem_nhds_iff ne_top_of_lt isOpen_Iio instClosedIciTopology OrderTopology.to_orderClosedTopology ENNReal.instOrderTopology ENNReal.lt_add_right MeasureTheory.measure_ne_top ProbabilityTheory.IsFiniteKernel.isFiniteMeasure one_ne_zero NeZero.charZero_one ENNReal.instCharZero Filter.Tendsto.comp ContinuousAt.tendsto Set.prod_iUnion Set.univ_prod_univ MeasureTheory.tendsto_measure_iUnion_atTop instIsCountablyGenerated_atTop OrderTopology.of_linearLocallyFinite instDiscreteTopologyNat TopologicalSpace.SecondCountableTopology.to_separableSpace TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountableNat PseudoEMetricSpace.pseudoMetrizableSpace Monotone.set_prod monotone_const
tendsto_m_density 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	Filter.Eventually Filter.Tendsto Real densityProcess Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace density MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe instFunLike	—	Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass density_ae_eq_limitProcess tendsto_densityProcess_limitProcess Filter.univ_mem'
tendsto_setIntegral_densityProcess 📖	mathematical	ProbabilityTheory.Kernel Preorder.toLE PartialOrder.toPreorder instPartialOrder fst MeasurableSet	Filter.Tendsto Real MeasureTheory.integral Real.normedAddCommGroup InnerProductSpace.toNormedSpace Real.instRCLike NormedAddCommGroup.toSeminormedAddCommGroup RCLike.toInnerProductSpaceReal MeasureTheory.Measure.restrict DFunLike.coe MeasureTheory.Measure instFunLike densityProcess Filter.atTop Nat.instPreorder nhds UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Real.pseudoMetricSpace density	—	MeasureTheory.tendsto_setIntegral_of_L1' integrable_density Filter.Eventually.of_forall integrable_densityProcess Filter.tendsto_congr MeasureTheory.eLpNorm_congr_ae Filter.EventuallyEq.sub MeasureTheory.Measure.instOuterMeasureClass Filter.EventuallyEq.rfl Filter.EventuallyEq.symm density_ae_eq_limitProcess tendsto_eLpNorm_one_densityProcess_limitProcess

---

← Back to Index