Defs

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

Statistics

Metric	Count
Definitions IsFiniteKernel, IsMarkovKernel, IsSFiniteKernel, IsZeroOrMarkovKernel, coeAddHom, instAdd, instAddCommMonoid, instFunLike, instOrderBot, instPartialOrder, instSMulNat, instZero, seq, sum, toFun, «termKernel[_,_]__», «termKernel[_]__»	17
Theorems add, bound_eq_zero_of_isEmpty, bound_eq_zero_of_isEmpty', bound_lt_top, bound_ne_top, bound_zero, exists_univ_le, isFiniteMeasure, IsZeroOrMarkovKernel, bound_eq_one, isProbabilityMeasure, is_probability_measure', sFinite, tsum_finite, bound_le_one, eq_zero_or_isMarkovKernel', isFiniteKernel, isZeroOrProbabilityMeasure, isSFiniteKernel, add, finset_sum, add_apply, aemeasurable, apply_congr_of_mem_measurableAtom, bound_eq_one, bound_eq_zero_of_isEmpty, bound_eq_zero_of_isEmpty', bound_le_one, bound_lt_top, bound_ne_top, bound_zero, coeAddHom_apply, coe_add, coe_finset_sum, coe_mk, coe_nsmul, coe_zero, eq_zero_of_isEmpty_left, eq_zero_of_isEmpty_right, ext, ext_fun, ext_fun_iff, ext_iff, ext_iff', finset_sum_apply, finset_sum_apply', instAddLeftMono, instIsMarkovKernelOfIsEmpty, instIsZeroOrMarkovKernelOfIsEmpty, instSubsingletonOfIsEmpty, isFiniteKernel_seq, isSFiniteKernel_sum, isSFiniteKernel_sum_of_denumerable, kernel_sum_seq, measurable, measurable', measurable_coe, measure_le_bound, measure_sum_seq, not_isMarkovKernel_zero, nsmul_apply, sum_add, sum_apply, sum_apply', sum_comm, sum_fintype, sum_zero, zero_apply, eq_zero_or_isMarkovKernel, instIsZeroOrMarkovKernelOfNatKernel, isFiniteKernel_of_le, isFiniteKernel_zero	72
Total	89

ProbabilityTheory

Definitions

Name	Category	Theorems
IsFiniteKernel 📖	CompData	31 math math: IsZeroOrMarkovKernel.isFiniteKernel, Kernel.instIsFiniteKernelSectROfProd, Kernel.const.instIsFiniteKernel, Kernel.instIsFiniteKernelWithDensityRnDeriv, Kernel.IsFiniteKernel.map, IsSFiniteKernel.tsum_finite, IsFiniteKernel.add, Kernel.IsFiniteKernel.prodMkRight, Kernel.IsFiniteKernel.swapLeft, Kernel.IsFiniteKernel.snd, Kernel.isFiniteKernel_seq, Kernel.isFiniteKernel_of_isFiniteKernel_snd, Kernel.IsFiniteKernel.comap, Kernel.IsFiniteKernel.fst, Kernel.IsFiniteKernel.piecewise, Kernel.IsFiniteKernel.prod, isFiniteKernel_of_le, Kernel.IsFiniteKernel.restrict, Kernel.instIsFiniteKernelSectLOfProd, Kernel.IsFiniteKernel.comp, Kernel.IsFiniteKernel.compProd, Kernel.instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure, Kernel.IsFiniteKernel.comapRight, Kernel.instIsFiniteKernelSingularPart, Kernel.isFiniteKernel_of_isFiniteKernel_fst, Kernel.isFiniteKernel_withDensity_of_bounded, Kernel.IsFiniteKernel.prodMkLeft, Kernel.instIsFiniteKernelBorelMarkovFromReal, Kernel.instIsFiniteKernelProdParallelComp, isFiniteKernel_zero, Kernel.IsFiniteKernel.swapRight
IsMarkovKernel 📖	CompData	41 math math: Kernel.instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure, Kernel.instIsMarkovKernelProdSwap, Kernel.instIsMarkovKernelCondKernelBorel, Kernel.instIsMarkovKernelProdCopy, Kernel.instIsMarkovKernelBorelMarkovFromReal, Kernel.IsMarkovKernel.compProd, Kernel.instNonemptySubtypeIsMarkovKernel, Kernel.instIsMarkovKernelOfIsEmpty, Kernel.instIsMarkovKernelCondKernelUnitReal, Kernel.not_isMarkovKernel_zero, Kernel.instIsMarkovKernelSectROfProd, Kernel.IsMarkovKernel.fst, Kernel.IsMarkovKernel.comapRight, Kernel.IsMarkovKernel.swapRight, Kernel.IsMarkovKernel.prod, Kernel.IsMarkovKernel.comap, Kernel.IsMarkovKernel.swapLeft, instIsMarkovKernelPosterior, Kernel.IsMarkovKernel.comp, Kernel.isMarkovKernel_deterministic, eq_zero_or_isMarkovKernel, Kernel.instIsMarkovKernelCondKernelUnitBorel, Kernel.IsMarkovKernel.snd, instIsMarkovKernelCondExpKernel, Kernel.IsMarkovKernel.piecewise, Kernel.IsMarkovKernel.prodMkRight, Kernel.exists_ae_eq_isMarkovKernel, Kernel.instIsMarkovKernelCondKernel, instIsMarkovKernel_toKernel, Kernel.const.instIsMarkovKernel, MeasureTheory.Measure.IsCondKernel.isMarkovKernel, Kernel.instIsMarkovKernelId, Kernel.instIsMarkovKernelCondKernelReal, Kernel.IsMarkovKernel.map, IsZeroOrMarkovKernel.eq_zero_or_isMarkovKernel', instIsMarkovKernelCondDistrib, Kernel.instIsMarkovKernelSectLOfProd, MeasureTheory.Measure.instIsMarkovKernelCondKernel, Kernel.instIsMarkovKernelUnitDiscard, Kernel.IsMarkovKernel.prodMkLeft, Kernel.instIsMarkovKernelProdParallelComp
IsSFiniteKernel 📖	CompData	33 math math: Kernel.IsSFiniteKernel.add, Kernel.IsSFiniteKernel.prodMkLeft, Kernel.IsSFiniteKernel.fst, Kernel.const.instIsSFiniteKernel, Kernel.isSFiniteKernel_prodMkRight_iff, Kernel.isSFiniteKernel_withDensity_of_isFiniteKernel, Kernel.IsSFiniteKernel.comp, Kernel.instIsSFiniteKernelWithDensityOfNNReal, Kernel.isSFiniteKernel_prodMkRight_unit, Kernel.parallelComp_def, Kernel.IsSFiniteKernel.map, Kernel.instIsSFiniteKernelProdParallelComp, Kernel.isSFiniteKernel_prodMkLeft_unit, Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialTraj, Kernel.IsSFiniteKernel.prod, Kernel.instIsSFiniteKernelBorelMarkovFromReal, Kernel.instIsSFiniteKernelSectLOfProd, Kernel.instIsSFiniteKernelSectROfProd, Kernel.IsSFiniteKernel.swapLeft, Kernel.IsSFiniteKernel.prodMkRight, Kernel.IsSFiniteKernel.restrict, MeasureTheory.Measure.IsCondKernel.isSFiniteKernel, Kernel.IsSFiniteKernel.comap, Kernel.isSFiniteKernel_prodMkLeft_iff, Kernel.IsSFiniteKernel.withDensity, Kernel.IsSFiniteKernel.comapRight, Kernel.IsFiniteKernel.isSFiniteKernel, Kernel.IsSFiniteKernel.snd, Kernel.isSFiniteKernel_const, Kernel.IsSFiniteKernel.compProd, Kernel.instIsSFiniteKernelBoolBoolKernelOfSFinite, Kernel.IsSFiniteKernel.swapRight, Kernel.IsSFiniteKernel.piecewise
IsZeroOrMarkovKernel 📖	CompData	17 math math: Kernel.instIsZeroOrMarkovKernelOfIsEmpty, Kernel.instIsZeroOrMarkovKernelSectLOfProd, Kernel.IsZeroOrMarkovKernel.snd, Kernel.IsZeroOrMarkovKernel.swapRight, Kernel.IsZeroOrMarkovKernel.prod, Kernel.IsZeroOrMarkovKernel.map, Kernel.IsZeroOrMarkovKernel.comp, Kernel.IsZeroOrMarkovKernel.compProd, Kernel.IsZeroOrMarkovKernel.prodMkLeft, Kernel.instIsZeroOrMarkovKernelProdParallelComp, instIsZeroOrMarkovKernelOfNatKernel, Kernel.IsZeroOrMarkovKernel.prodMkRight, Kernel.IsZeroOrMarkovKernel.comap, IsMarkovKernel.IsZeroOrMarkovKernel, Kernel.instIsZeroOrMarkovKernelSectROfProd, Kernel.IsZeroOrMarkovKernel.fst, Kernel.const.instIsZeroOrMarkovKernel
«termKernel[_,_]__» 📖	CompOp	—
«termKernel[_]__» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_or_isMarkovKernel 📖	mathematical	—	Kernel Kernel.instZero IsMarkovKernel	—	IsZeroOrMarkovKernel.eq_zero_or_isMarkovKernel'
instIsZeroOrMarkovKernelOfNatKernel 📖	mathematical	—	IsZeroOrMarkovKernel Kernel Kernel.instZero	—	—
isFiniteKernel_of_le 📖	mathematical	Kernel Preorder.toLE PartialOrder.toPreorder Kernel.instPartialOrder	IsFiniteKernel	—	Kernel.bound_lt_top LE.le.trans Kernel.measure_le_bound
isFiniteKernel_zero 📖	mathematical	—	IsFiniteKernel Kernel Kernel.instZero	—	ENNReal.coe_lt_top

ProbabilityTheory.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instAdd	—	ENNReal.add_lt_top ProbabilityTheory.Kernel.bound_lt_top add_le_add IsOrderedAddMonoid.toAddLeftMono ENNReal.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add ProbabilityTheory.Kernel.measure_le_bound
bound_eq_zero_of_isEmpty 📖	mathematical	—	ProbabilityTheory.Kernel.bound ENNReal instZeroENNReal	—	ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty
bound_eq_zero_of_isEmpty' 📖	mathematical	—	ProbabilityTheory.Kernel.bound ENNReal instZeroENNReal	—	ProbabilityTheory.Kernel.bound_eq_zero_of_isEmpty'
bound_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder ProbabilityTheory.Kernel.bound Top.top instTopENNReal	—	ProbabilityTheory.Kernel.bound_lt_top
bound_ne_top 📖	—	—	—	—	ProbabilityTheory.Kernel.bound_ne_top
bound_zero 📖	mathematical	—	ProbabilityTheory.Kernel.bound ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instZero ENNReal instZeroENNReal	—	ProbabilityTheory.Kernel.bound_zero
exists_univ_le 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder Top.top instTopENNReal Preorder.toLE DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.univ	—	—
isFiniteMeasure 📖	mathematical	—	MeasureTheory.IsFiniteMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	LE.le.trans_lt ProbabilityTheory.Kernel.measure_le_bound ProbabilityTheory.Kernel.bound_lt_top

ProbabilityTheory.IsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
IsZeroOrMarkovKernel 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel	—	—
bound_eq_one 📖	mathematical	—	ProbabilityTheory.Kernel.bound ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	ProbabilityTheory.Kernel.bound_eq_one
isProbabilityMeasure 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	—
is_probability_measure' 📖	mathematical	—	MeasureTheory.IsProbabilityMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	isProbabilityMeasure

ProbabilityTheory.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
sFinite 📖	mathematical	—	MeasureTheory.SFinite DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	ProbabilityTheory.IsFiniteKernel.isFiniteMeasure ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.measure_sum_seq
tsum_finite 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.sum instCountableNat	—	—

ProbabilityTheory.IsZeroOrMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bound_le_one 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder ProbabilityTheory.Kernel.bound AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	ProbabilityTheory.Kernel.bound_le_one
eq_zero_or_isMarkovKernel' 📖	mathematical	—	ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instZero ProbabilityTheory.IsMarkovKernel	—	—
isFiniteKernel 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel	—	ProbabilityTheory.eq_zero_or_isMarkovKernel ProbabilityTheory.isFiniteKernel_zero ENNReal.one_lt_top MeasureTheory.prob_le_one isZeroOrProbabilityMeasure
isZeroOrProbabilityMeasure 📖	mathematical	—	MeasureTheory.IsZeroOrProbabilityMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike	—	ProbabilityTheory.eq_zero_or_isMarkovKernel MeasureTheory.instIsZeroOrProbabilityMeasureOfNatMeasure MeasureTheory.instIsZeroOrProbabilityMeasureOfIsProbabilityMeasure ProbabilityTheory.IsMarkovKernel.is_probability_measure'

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
coeAddHom 📖	CompOp	1 math math: coeAddHom_apply
instAdd 📖	CompOp	30 math math: rnDeriv_add_singularPart, IsSFiniteKernel.add, coe_add, notMem_mutuallySingularSetSlice, measurable_singularPart_fun_right, MeasureTheory.Measure.add_comp, prodMkRight_add, rnDeriv_def', prodMkLeft_add, withDensity_add_left, ProbabilityTheory.IsFiniteKernel.add, add_apply, measurable_singularPart_fun, withDensity_rnDerivAux, sum_add, withDensity_one_sub_rnDerivAux, withDensity_add_right, compProd_add_right, const_add, compProd_add_left, mem_mutuallySingularSetSlice, singularPart_def, comp_add_right, MeasureTheory.Measure.compProd_add_right, rnDeriv_add, comp_add_left, withDensity_sub_add_cancel, rnDeriv_def, setLIntegral_rnDerivAux, instAddLeftMono
instAddCommMonoid 📖	CompOp	6 math math: sum_fintype, coeAddHom_apply, IsSFiniteKernel.finset_sum, finset_sum_apply', coe_finset_sum, finset_sum_apply
instFunLike 📖	CompOp	538 math math: restrict_apply', MeasureTheory.StronglyMeasurable.integral_kernel_prod_right'', ProbabilityTheory.stieltjesOfMeasurableRat_ae_eq, prod_apply', tendsto_m_density, ProbabilityTheory.absolutelyContinuous_posterior_iff, sectR_apply, coe_nsmul, iIndepSet_iff_meas_biInter, ProbabilityTheory.condDistrib_apply_of_ne_zero, ProbabilityTheory.condDistrib_ae_eq_condExp, lintegral_swapRight, ProbabilityTheory.IsCondKernelCDF.toKernel_Iic, MeasureTheory.AEStronglyMeasurable.integral_condDistrib_map, MeasureTheory.Measure.swap_comp, ProbabilityTheory.lintegral_toKernel_univ, borelMarkovFromReal_apply', iIndep.meas_biInter, ProbabilityTheory.IsRatCondKernelCDF.iInf_rat_gt_eq, density_fst_univ, setIntegral_deterministic', map_apply, condExp_traj', MeasureTheory.Measure.AbsolutelyContinuous.kernel_of_compProd, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_one_of_monotone, MeasureTheory.Measure.comp_apply_univ, swapRight_apply', ProbabilityTheory.condExp_ae_eq_integral_condDistrib_id, Measurable.lintegral_kernel_prod_left', MeasureTheory.Measure.comp_add, MeasureTheory.Integrable.norm_integral_condExpKernel, coe_add, trajContent_cylinder, ProbabilityTheory.boolKernel_comp_measure, MeasureTheory.Measure.ae_ae_of_ae_compProd, IndepSets.indep_aux, setIntegral_restrict, ProbabilityTheory.integrable_toReal_condExpKernel, sectR_prodMkRight, ProbabilityTheory.IsRatCondKernelCDFAux.bddBelow_range, integral_deterministic', MeasureTheory.Measure.comp_compProd_comm, ProbabilityTheory.compProd_posterior_eq_map_swap, apply_eq_measure_condKernel_of_compProd_eq, integral_restrict, ProbabilityTheory.bayesRisk_of_subsingleton', withDensity_rnDeriv_eq_zero_iff_measure_eq_zero, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat_rat, compProd_null, lintegral_id_prod, ProbabilityTheory.IsRatCondKernelCDF.setIntegral, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, nsmul_apply, ProbabilityTheory.setLIntegral_condKernel_univ_right, ProbabilityTheory.condExpKernel_comp_trim, ProbabilityTheory.IsCondKernelCDF.integral, traj_map_updateFinset, swapRight_apply, lintegral_fst, coeAddHom_apply, IsCondKernel.isProbabilityMeasure_ae, MeasureTheory.Measure.map_comp, measure_zero_or_one_of_measurableSet_limsup_atTop, MeasureTheory.Measure.const_comp, MeasureTheory.AEStronglyMeasurable.integral_condExpKernel, ae_compProd_iff, MeasureTheory.AEStronglyMeasurable.ae_integrable_condKernel_iff, swap_apply, measurable_densityProcess_countableFiltration_aux, deterministic_prod_apply', coe_zero, isIrreducible_iff, HasSubgaussianMGF.integrable_exp_add_compProd, MeasureTheory.Measure.setIntegral_condKernel, ProbabilityTheory.integral_stieltjesOfMeasurableRat, ProbabilityTheory.condExp_ae_eq_integral_condDistrib, map_apply', HasSubgaussianMGF.memLp_exp_mul, instNeZeroMeasureCoeSectROfProdMk, ProbabilityTheory.posterior_boolKernel_apply_true, parallelComp_apply_prod, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atBot_zero, restrict_apply, MeasureTheory.Measure.add_comp, iIndepSet.meas_biInter, MeasureTheory.Measure.comp_eq_sum_of_countable, MeasureTheory.Measure.setIntegral_condKernel_univ_left, MeasureTheory.StronglyMeasurable.integral_kernel_prod_right, mutuallySingular_singularPart, ProbabilityTheory.stronglyMeasurable_integral_condDistrib, ProbabilityTheory.measurable_condDistrib, MeasureTheory.Measure.discard_comp, tendsto_density_atTop_ae_of_antitone, MeasureTheory.Integrable.integral_norm_condDistrib_map, fst_real_apply, piecewise_apply', MeasureTheory.Measure.snd_compProd, MeasureTheory.Measure.AbsolutelyContinuous.comp_right, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_antitone, indepSet_iff_measure_inter_eq_mul, compProd_deterministic_apply, setIntegral_densityProcess_of_mem, Invariant.def, rnDeriv_singularPart, MeasureTheory.Measure.instIsProbabilityMeasureBindCoeKernelOfIsMarkovKernel, compProd_eq_tsum_compProd, prodMkLeft_apply, lintegral_withDensity, rnDeriv_eq_rnDeriv_measure, integrable_densityProcess, martingale_densityProcess, MeasureTheory.Measure.integral_condKernel, MeasureTheory.Measure.mutuallySingular_of_mutuallySingular_compProd, MeasureTheory.Integrable.norm_integral_condDistrib, HasSubgaussianMGF.measure_pos_eq_zero_of_hasSubGaussianMGF_zero, ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd, boolKernel_apply, ProbabilityTheory.stronglyMeasurable_condExpKernel, MeasureTheory.Measure.mutuallySingular_compProd_right_iff, ae_lt_top_of_comp_ne_top, indepFun_iff_measure_inter_preimage_eq_mul, prod_apply, ProbabilityTheory.avgRisk_le_iSup_risk, ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd, setIntegral_const, setIntegral_densityProcess_of_le, le_compProd_apply, fst_apply, MeasureTheory.Measure.setIntegral_compProd, deterministic_apply, iIndepSets.meas_biInter, ProbabilityTheory.setLIntegral_condKernel, ProbabilityTheory.condExpKernel_ae_eq_condExp', ProbabilityTheory.lintegral_condKernel, MeasureTheory.Integrable.condKernel_ae, ProbabilityTheory.condDistrib_comp_map, measure_zero_or_one_of_measurableSet_limsup, ProbabilityTheory.aestronglyMeasurable_integral_condDistrib, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map, ProbabilityTheory.IsCondKernelCDF.setIntegral, withDensity_absolutelyContinuous, MeasureTheory.Measure.setIntegral_condKernel_univ_right, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel_of_stronglyMeasurable, ae_kernel_lt_top, MeasureTheory.Measure.absolutelyContinuous_comp_of_countable, ProbabilityTheory.condExp_ae_eq_trim_integral_condExpKernel, MeasureTheory.Measure.condKernel_apply_of_ne_zero, copy_apply, rnDeriv_ne_top, HasSubgaussianMGF.integrable_exp_mul, parallelComp_def, ProbabilityTheory.IsRatCondKernelCDFAux.mono, setIntegral_deterministic, MeasureTheory.Measure.compProd_apply, eq_boolKernel, setLIntegral_restrict, partialTraj_compProd_traj, lintegral_prodMkRight, ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map, MeasureTheory.Integrable.integral_norm_condExpKernel, MeasureTheory.StronglyMeasurable.integral_kernel_prod_right', ProbabilityTheory.IsZeroOrMarkovKernel.isZeroOrProbabilityMeasure, MeasureTheory.Measure.add_comp', ProbabilityTheory.IsCondKernelCDF.setLIntegral, condKernelCountable_apply, ProbabilityTheory.IsRatCondKernelCDFAux.nonneg, finset_sum_apply', MeasureTheory.StronglyMeasurable.integral_condExpKernel, lintegral_map, pow_add_apply_eq_lintegral, ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure, aemeasurable, condKernel_apply_eq_condKernel, meas_countablePartitionSet_le_of_fst_le, IsProper.restrict_eq_indicator_smul, discard_apply, ProbabilityTheory.IsSFiniteKernel.sFinite, tendsto_integral_density_of_monotone, memL1_limitProcess_densityProcess, Measurable.lintegral_kernel_prod_right'', id_prod_apply', condDistrib_trajMeasure, singularPart_eq_zero_iff_apply_eq_zero, MeasureTheory.Integrable.norm_integral_condKernel, ProbabilityTheory.IsRatCondKernelCDF.tendsto_atTop_one, ae_comp_iff, ProbabilityTheory.posterior_prod_id_comp, MeasureTheory.Measure.compProd_id_eq_copy_comp, singularPart_eq_zero_iff_measure_eq_zero, setLIntegral_deterministic, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat, ae_eq_of_compProd_eq, measurable_kernel_prodMk_left', MeasureTheory.Measure.lintegral_condKernel, partialTraj_map_frestrictLe₂_apply, densityProcess_fst_univ_ae, ProbabilityTheory.setLIntegral_condKernel_univ_left, boolKernel_false, lintegral_traj, MeasureTheory.Integrable.integral_condExpKernel, setLIntegral_compProd_univ_left, measurable_lintegral_indicator_const, comp_apply, MeasureTheory.Measure.parallelComp_comp_compProd, IsProper.restrict_eq_indicator_smul', ProbabilityTheory.condDistrib_comp, setIntegral_density_of_measurableSet, Measurable.setLIntegral_kernel_prod_left, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel, MeasureTheory.Measure.comp_eq_comp_const_apply, comp_discard', integral_const, add_apply, tendsto_integral_density_of_antitone, HasSubgaussianMGF.isFiniteMeasure, compProd_eq_zero_iff, ext_iff, piecewise_apply, lintegral_compProd', ProbabilityTheory.condKernel_compProd, prodMkRight_apply, density_ae_eq_limitProcess, Measurable.setLIntegral_kernel, IsFiniteKernel.integrable, ProbabilityTheory.IsRatCondKernelCDFAux.mono', rnDerivAux_le_one, comp_const, Measurable.lintegral_kernel, Measurable.lintegral_kernel_prod_left, MeasureTheory.Integrable.integral_condDistrib_map, MeasureTheory.Measure.integrable_compProd_iff, continuous_integral_integral, MeasureTheory.Integrable.condDistrib_ae, measurableSet_mutuallySingular, ProbabilityTheory.setLIntegral_toKernel_univ, ProbabilityTheory.condExpKernel_singleton_ae_eq_cond, coe_mk, iIndepFun.measure_inter_preimage_eq_mul, lintegral_prod, MeasureTheory.StronglyMeasurable.integral_condExpKernel', ProbabilityTheory.condDistrib_snd_prod, setIntegral_densityProcess, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib, ProbabilityTheory.condExp_ae_eq_integral_condExpKernel', MeasureTheory.StronglyMeasurable.integral_condDistrib, isProper_iff_restrict_eq_indicator_smul, ext_iff', MeasureTheory.Measure.setLIntegral_condKernel, MeasureTheory.Measure.compProd_eq_comp_prod, integral_densityProcess, IndepFun.meas_inter, ProbabilityTheory.IsRatCondKernelCDFAux.le_one', isProjectiveLimit_trajFun, ProbabilityTheory.condDistrib_ae_eq_of_measure_eq_compProd_of_measurable, ProbabilityTheory.lintegral_toKernel_mem, coe_finset_sum, measurableSet_absolutelyContinuous, parallelComp_apply', ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_zero_of_antitone, IsIrreducible.irreducible, setLIntegral_density, MeasureTheory.Measure.ae_comp_iff, lintegral_snd, integrable_density, ProbabilityTheory.hasFiniteIntegral_prodMk_left, lintegral_const, instNeZeroMeasureCoeSectLOfProdMk, MeasureTheory.Measure.lintegral_condKernel_mem, setLIntegral_deterministic', MeasureTheory.AEStronglyMeasurable.ae_of_compProd, ProbabilityTheory.IsRatCondKernelCDF.tendsto_atBot_zero, MeasureTheory.Integrable.norm_integral_condDistrib_map, ProbabilityTheory.condExpKernel_ae_eq_condExp, lintegral_prod_symm, ProbabilityTheory.hasFiniteIntegral_comp_iff, ProbabilityTheory.aestronglyMeasurable_trim_condExpKernel, ProbabilityTheory.IsFiniteKernel.isFiniteMeasure, tendsto_eLpNorm_one_densityProcess_limitProcess, MeasureTheory.Measure.deterministic_comp_eq_map, ProbabilityTheory.measurableSet_integrable, integral_density, withDensity_rnDeriv_of_subset_mutuallySingularSetSlice, MeasureTheory.Measure.integral_compProd, compProd_apply_univ_le, lintegral_density, MeasureTheory.Integrable.integral_norm_condDistrib, ProbabilityTheory.IsRatCondKernelCDFAux.integrable, ProbabilityTheory.IsCondKernelCDF.integrable, ProbabilityTheory.condExpKernel_ae_eq_trim_condExp, withDensity_rnDeriv_of_subset_compl_mutuallySingularSetSlice, measurable_densityProcess_aux, ProbabilityTheory.IsRatCondKernelCDFAux.iInf_rat_gt_eq, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib₀, prodMkLeft_apply', lintegral_comap, ProbabilityTheory.IsRatCondKernelCDFAux.le_one, isProper_iff_inter_eq_indicator_mul, withDensity_rnDeriv_le, rnDeriv_lt_top, MeasureTheory.Measure.compProd_apply_prod, lintegral_piecewise, continuous_integral_integral_comp, ProbabilityTheory.parallelProd_posterior_comp_copy_comp, fst_apply', singularPart_eq_singularPart_measure, withDensity_apply, ProbabilityTheory.IsMarkovKernel.is_probability_measure', iIndep.meas_iInter, ext_fun_iff, ProbabilityTheory.posterior_boolKernel_apply_false, IsProper.setLIntegral_eq_indicator_mul_lintegral, singularPart_of_subset_compl_mutuallySingularSetSlice, tendsto_setIntegral_densityProcess, MeasureTheory.AEStronglyMeasurable.ae_integrable_condDistrib_map_iff, ProbabilityTheory.setLIntegral_toKernel_prod, lintegral_deterministic_prod, MeasureTheory.AEStronglyMeasurable.integral_condKernel, isProjectiveMeasureFamily_partialTraj, setLIntegral_compProd, IsProper.setLIntegral_eq_comp, snd_apply', snd_apply, sum_apply, ProbabilityTheory.measurable_condExpKernel, MeasureTheory.Integrable.integral_condDistrib, ProbabilityTheory.swap_compProd_posterior, ProbabilityTheory.avgRisk_const_left, ProbabilityTheory.condDistrib_self, IsMarkovKernel.integrable, compProd_preimage_fst, MeasureTheory.Measure.comp_assoc, ProbabilityTheory.condExp_ae_eq_integral_condDistrib', condExp_densityProcess, MeasureTheory.Measure.instIsFiniteMeasureBindCoeKernelOfIsFiniteKernel, tendsto_densityProcess_limitProcess, sectL_prodMkLeft, traj_apply, prodMkRight_apply', ProbabilityTheory.bayesRisk_le_iInf', withDensity_rnDeriv_eq_zero_iff_mutuallySingular, withDensity_rnDeriv_eq_zero_iff_apply_eq_zero, singularPart_eq_zero_iff_absolutelyContinuous, Measurable.lintegral_kernel_prod_right, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd_real, ProbabilityTheory.condDistrib_comp_self, ProbabilityTheory.measurableSet_kernel_integrable, MeasureTheory.StronglyMeasurable.integral_kernel_prod_left'', id_apply, ProbabilityTheory.integrable_kernel_prodMk_left, compProd_apply_univ, ProbabilityTheory.avgRisk_const_left', MeasureTheory.Measure.id_comp, MeasureTheory.Measure.setLIntegral_condKernel_univ_left, ProbabilityTheory.IsRatCondKernelCDFAux.integrable_iInf_rat_gt, deterministic_apply', boolKernel_true, tendsto_densityProcess_fst_atTop_ae_of_monotone, borelMarkovFromReal_apply, lintegral_parallelComp_symm, measure_le_bound, lintegral_id, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd', setLIntegral_compProd_univ_right, MeasureTheory.Measure.IsCondKernel.isProbabilityMeasure, MeasureTheory.Measure.prod_comp_left, measure_zero_or_one_of_measurableSet_limsup_atBot, traj_map_frestrictLe_apply, ProbabilityTheory.IsRatCondKernelCDFAux.isRatStieltjesPoint_ae, finset_sum_apply, MeasureTheory.Measure.comp_smul, ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod, eLpNorm_densityProcess_le, ProbabilityTheory.posterior_id, measure_eq_zero_or_one_or_top_of_indepSet_self, ProbabilityTheory.IsRatCondKernelCDFAux.nonneg', IsProper.setLIntegral_inter_eq_indicator_mul_setLIntegral, iIndep.ae_isProbabilityMeasure, lintegral_prod_deterministic, measure_sum_seq, singularPart_compl_mutuallySingularSetSlice, measurable, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral_iInf_rat_gt, MeasureTheory.Measure.setLIntegral_compProd, measurable_coe, withDensity_rnDeriv_mutuallySingularSetSlice, comapRight_apply', eLpNorm_density_le, lintegral_comp, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right, condKernel_def, setIntegral_piecewise, densityProcess_fst_univ, ProbabilityTheory.hasFiniteIntegral_compProd_iff, HasSubgaussianMGF.measure_ge_le, comap_apply, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, sectL_apply, ProbabilityTheory.posterior_posterior, zero_apply, ProbabilityTheory.condDistrib_const, lintegral_prodMkLeft, MeasureTheory.Measure.dirac_compProd_apply, MeasureTheory.AEStronglyMeasurable.integral_condDistrib, MeasureTheory.Measure.prod_comp_right, iIndepFun.meas_iInter, setIntegral_density, ProbabilityTheory.condDistrib_fst_prod, integral_integral_indicator, ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_atTop_one, ProbabilityTheory.posterior_comp_self, pow_succ_apply_eq_lintegral, iIndepFun.meas_biInter, IndepFun.measure_inter_preimage_eq_mul, ProbabilityTheory.posterior_eq_withDensity_of_countable, lintegral_deterministic, ProbabilityTheory.IsFiniteKernel.exists_univ_le, ProbabilityTheory.avgRisk_const_right', ProbabilityTheory.lintegral_stieltjesOfMeasurableRat, MeasureTheory.Measure.compProd_eq_zero_iff, measurable_singularPart, comapRight_apply, setLIntegral_piecewise, ProbabilityTheory.integrable_toReal_condDistrib, MeasureTheory.Measure.copy_comp_map, comp_apply', integral_piecewise, parallelComp_apply, compProd_apply_eq_compProd_sectR, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, ProbabilityTheory.IsRatCondKernelCDF.isRatStieltjesPoint_ae, HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero', iIndepSets_singleton_iff, MeasureTheory.Measure.setLIntegral_condKernel_univ_right, ProbabilityTheory.condDistrib_map, ProbabilityTheory.setLIntegral_condDistrib_of_measurableSet, compProd_eq_iff, compProd_apply, ProbabilityTheory.IsCondKernelCDF.lintegral, withDensity_apply', HasSubgaussianMGF.ae_aestronglyMeasurable, const_apply, rnDeriv_add, MeasureTheory.Measure.instSFiniteBindCoeKernelOfIsSFiniteKernel, ProbabilityTheory.setLIntegral_preimage_condDistrib, tendsto_eLpNorm_one_restrict_densityProcess_limitProcess, ProbabilityTheory.eq_condKernel_of_kernel_eq_compProd, sum_apply', MeasureTheory.Measure.ae_compProd_iff, IndepSet.measure_inter_eq_mul, MeasureTheory.Measure.absolutelyContinuous_compProd_right_iff, MeasureTheory.Measure.dirac_unit_compProd, iIndepFun.ae_isProbabilityMeasure, lintegral_deterministic', swapLeft_apply', ProbabilityTheory.IsRatCondKernelCDFAux.tendsto_integral_of_monotone, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left, ProbabilityTheory.lintegral_condKernel_mem, ProbabilityTheory.compProd_posterior_eq_swap_comp, setLIntegral_const, MeasureTheory.StronglyMeasurable.integral_kernel_prod_left', rnDeriv_self, measurable_kernel_prodMk_right, lmarginalPartialTraj_succ, MeasureTheory.Measure.prodMkLeft_comp_compProd, ProbabilityTheory.IsRatCondKernelCDF.mono, measure_mutuallySingularSetSlice, iIndepFun.cond_iInter, ProbabilityTheory.IsRatCondKernelCDFAux.setIntegral, Measurable.setLIntegral_kernel_prod_right, comp_apply_univ_le, ProbabilityTheory.setIntegral_stieltjesOfMeasurableRat_rat, ProbabilityTheory.IsRatCondKernelCDF.integrable, HasSubgaussianMGF.measure_univ_le_one, apply_congr_of_mem_measurableAtom, ProbabilityTheory.condKernel_const, lintegral_compProd, MeasureTheory.Integrable.condDistrib_ae_map, ProbabilityTheory.condExp_prod_ae_eq_integral_condDistrib', parallelComp_apply_univ, lintegral_parallelComp, MeasureTheory.Integrable.condExpKernel_ae, MeasureTheory.Integrable.integral_norm_condKernel, densityProcess_def, Measurable.lintegral_kernel_prod_right', MeasureTheory.Measure.instIsZeroOrProbabilityMeasureBindCoeKernelOfIsZeroOrMarkovKernel, HasSubgaussianMGF.aestronglyMeasurable, MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp, HasSubgaussianMGF.ae_integrable_exp_mul, MeasureTheory.StronglyMeasurable.integral_kernel, lmarginalPartialTraj_eq_lintegral_map, ProbabilityTheory.setLIntegral_stieltjesOfMeasurableRat, lintegral_swapLeft, MeasureTheory.StronglyMeasurable.integral_kernel_prod_left, integral_withDensity, const_comp, compProd_apply_prod, partialTraj_compProd_eq_map_traj, iIndepSets.meas_iInter, rnDeriv_withDensity, ProbabilityTheory.eq_condKernel_of_measure_eq_compProd, MeasureTheory.Measure.condKernel_apply, measurable_kernel_prodMk_left, setLIntegral_rnDerivAux, comp_boolKernel, MeasureTheory.Measure.lintegral_compProd, comap_apply', MeasureTheory.Integrable.integral_condKernel, ProbabilityTheory.aestronglyMeasurable_integral_condExpKernel, MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod, setLIntegral_rnDeriv_le, lintegral_restrict, swap_apply', tendsto_density_fst_atTop_ae_of_monotone, MeasureTheory.Measure.IsCondKernel.apply_of_ne_zero, indepSets_singleton_iff, coe_comap, integral_deterministic, iIndepSets.ae_isProbabilityMeasure, comp_null, swapLeft_apply, fst_compProd_apply, ProbabilityTheory.deterministic_comp_posterior, ProbabilityTheory.setLIntegral_toKernel_Iic, ProbabilityTheory.IsCondKernelCDF.toKernel_apply, IsProper.lintegral_mul, HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero_of_measurable, prod_apply_prod, IsProper.inter_eq_indicator_mul, ProbabilityTheory.condExpKernel_apply_eq_condDistrib, ProbabilityTheory.integrable_stieltjesOfMeasurableRat, lintegral_prod_id, singularPart_of_subset_mutuallySingularSetSlice, ProbabilityTheory.posterior_comp, HasSubgaussianMGF.ae_eq_zero_of_hasSubgaussianMGF_zero, lintegral_id', ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib, iIndepFun_iff_measure_inter_preimage_eq_mul, integral_indicator₂
instOrderBot 📖	CompOp	—
instPartialOrder 📖	CompOp	1 math math: instAddLeftMono
instSMulNat 📖	CompOp	2 math math: coe_nsmul, nsmul_apply
instZero 📖	CompOp	56 math math: swapLeft_zero, ProbabilityTheory.avgRisk_zero_right, indepSet_zero_left, parallelComp_of_not_isSFiniteKernel_left, coe_zero, snd_zero, compProd_zero_right, compProd_of_not_isSFiniteKernel_right, not_isMarkovKernel_zero, instIsCondKernel_zero, zero_comp, indepSets_zero_left, parallelComp_def, prod_of_not_isSFiniteKernel_right, compProd_of_not_isSFiniteKernel_left, comp_zero, prodMkRight_zero, ProbabilityTheory.bayesRisk_zero_left, prod_of_not_isSFiniteKernel_left, compProd_eq_zero_iff, eq_zero_of_isEmpty_right, ProbabilityTheory.eq_zero_or_isMarkovKernel, ProbabilityTheory.condExpKernel_def, sectR_zero, singularPart_self, sectL_zero, ProbabilityTheory.avgRisk_zero_left, const_zero, bound_zero, parallelComp_of_not_isSFiniteKernel_right, swapRight_zero, sum_zero, ProbabilityTheory.IsFiniteKernel.bound_zero, eq_zero_of_isEmpty_left, parallelComp_zero_right, compProd_zero_left, prod_zero, indepFun_zero_left, zero_apply, MeasureTheory.Measure.compProd_zero_right, ProbabilityTheory.IsZeroOrMarkovKernel.eq_zero_or_isMarkovKernel', withDensity_zero, ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel, comap_zero, indep_zero_left, withDensity_zero', HasSubgaussianMGF.zero_kernel, ProbabilityTheory.minimaxRisk_zero, prodMkLeft_zero, withDensity_of_not_measurable, fst_zero, ProbabilityTheory.isFiniteKernel_zero, parallelComp_zero_left, map_zero, zero_prod, map_of_not_measurable
seq 📖	CompOp	9 math math: sum_comap_seq, compProd_eq_tsum_compProd, compProd_eq_sum_compProd, isFiniteKernel_seq, kernel_sum_seq, compProd_eq_sum_compProd_left, measure_sum_seq, sum_map_seq, compProd_eq_sum_compProd_right
sum 📖	CompOp	27 math math: sum_fintype, sum_comap_seq, sum_const, ProbabilityTheory.IsSFiniteKernel.tsum_finite, compProd_eq_sum_compProd, parallelComp_sum_left, comp_sum_left, withDensity_tsum, sum_add, parallelComp_sum_right, compProd_sum_left, kernel_sum_seq, withDensity_kernel_sum, sum_apply, compProd_eq_sum_compProd_left, sum_comm, comp_sum_right, sum_zero, isSFiniteKernel_sum_of_denumerable, MeasureTheory.Measure.compProd_sum_right, sum_map_seq, compProd_eq_sum_compProd_right, sum_apply', sum_prodMkRight, compProd_sum_right, sum_prodMkLeft, isSFiniteKernel_sum
toFun 📖	CompOp	1 math math: measurable'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike instAdd MeasureTheory.Measure.instAdd	—	—
aemeasurable 📖	mathematical	—	AEMeasurable MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	Measurable.aemeasurable measurable
apply_congr_of_mem_measurableAtom 📖	mathematical	Set Set.instMembership measurableAtom	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	MeasureTheory.Measure.ext mem_of_mem_measurableAtom measurable_coe MeasurableSingletonClass.measurableSet_singleton instMeasurableSingletonClassOfMeasurableEq instMeasurableEqOfSecondCountableTopologyOfT2Space BorelSpace.opensMeasurable ENNReal.borelSpace ENNReal.instSecondCountableTopology ENNReal.instT2Space
bound_eq_one 📖	mathematical	—	bound ENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' ciSup_const
bound_eq_zero_of_isEmpty 📖	mathematical	—	bound ENNReal instZeroENNReal	—	ciSup_of_empty bot_eq_zero' ENNReal.instCanonicallyOrderedAdd
bound_eq_zero_of_isEmpty' 📖	mathematical	—	bound ENNReal instZeroENNReal	—	MeasureTheory.Measure.instSubsingleton ENNReal.iSup_zero
bound_le_one 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder bound AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	isEmpty_or_nonempty bound_eq_zero_of_isEmpty ENNReal.instCanonicallyOrderedAdd ProbabilityTheory.eq_zero_or_isMarkovKernel bound_zero bound_eq_one
bound_lt_top 📖	mathematical	—	ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder bound Top.top instTopENNReal	—	ProbabilityTheory.IsFiniteKernel.exists_univ_le lt_of_le_of_lt
bound_ne_top 📖	—	—	—	—	LT.lt.ne bound_lt_top
bound_zero 📖	mathematical	—	bound ProbabilityTheory.Kernel instZero ENNReal instZeroENNReal	—	ENNReal.iSup_zero
coeAddHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom ProbabilityTheory.Kernel AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid instAddCommMonoid Pi.addZeroClass MeasureTheory.Measure MeasureTheory.Measure.instAddCommMonoid AddMonoidHom.instFunLike coeAddHom instFunLike	—	—
coe_add 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike instAdd Pi.instAdd MeasureTheory.Measure.instAdd	—	—
coe_finset_sum 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike Finset.sum instAddCommMonoid Pi.addCommMonoid MeasureTheory.Measure.instAddCommMonoid	—	map_sum AddMonoidHom.instAddMonoidHomClass
coe_mk 📖	mathematical	Measurable MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace	DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	—
coe_nsmul 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike instSMulNat AddMonoid.toNatSMul Pi.addMonoid AddCommMonoid.toAddMonoid MeasureTheory.Measure.instAddCommMonoid	—	—
coe_zero 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike instZero Pi.instZero MeasureTheory.Measure.instZero	—	—
eq_zero_of_isEmpty_left 📖	mathematical	—	ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext
eq_zero_of_isEmpty_right 📖	mathematical	—	ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext MeasureTheory.Measure.eq_zero_of_isEmpty
ext 📖	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	—	DFunLike.ext
ext_fun 📖	—	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	—	ext MeasureTheory.Measure.ext one_mul MeasureTheory.lintegral_indicator_const Measurable.indicator measurable_const
ext_fun_iff 📖	mathematical	—	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	ext_fun
ext_iff 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike	—	ext
ext_iff' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike	—	—
finset_sum_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike Finset.sum instAddCommMonoid MeasureTheory.Measure.instAddCommMonoid	—	coe_finset_sum Finset.sum_apply
finset_sum_apply' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike Finset.sum instAddCommMonoid ENNReal.instAddCommMonoid	—	finset_sum_apply MeasureTheory.Measure.finset_sum_apply
instAddLeftMono 📖	mathematical	—	AddLeftMono ProbabilityTheory.Kernel instAdd Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	add_le_add_right IsOrderedAddMonoid.toAddLeftMono MeasureTheory.Measure.instIsOrderedAddMonoid
instIsMarkovKernelOfIsEmpty 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel	—	—
instIsZeroOrMarkovKernelOfIsEmpty 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel	—	ext MeasureTheory.Measure.ext Set.eq_empty_of_isEmpty instIsEmptySubtype MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass
instSubsingletonOfIsEmpty 📖	mathematical	—	ProbabilityTheory.Kernel	—	ext MeasureTheory.Measure.ext Set.eq_empty_of_isEmpty instIsEmptySubtype MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass
isFiniteKernel_seq 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel seq	—	instCountableNat ProbabilityTheory.IsSFiniteKernel.tsum_finite
isSFiniteKernel_sum 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	sum	—	Finite.to_countable Finite.of_fintype sum_fintype IsSFiniteKernel.finset_sum nonempty_denumerable isSFiniteKernel_sum_of_denumerable
isSFiniteKernel_sum_of_denumerable 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	sum Encodable.countable Denumerable.toEncodable	—	Encodable.countable instCountableNat isFiniteKernel_seq sum.congr_simp kernel_sum_seq ext MeasureTheory.Measure.ext sum_apply' Equiv.tsum_eq Summable.tsum_prod' ENNReal.instContinuousAdd T4Space.t3Space ENNReal.instT4Space ENNReal.summable
kernel_sum_seq 📖	mathematical	—	sum instCountableNat seq	—	instCountableNat ProbabilityTheory.IsSFiniteKernel.tsum_finite
measurable 📖	mathematical	—	Measurable MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace DFunLike.coe ProbabilityTheory.Kernel instFunLike	—	measurable'
measurable' 📖	mathematical	—	Measurable MeasureTheory.Measure MeasureTheory.Measure.instMeasurableSpace toFun	—	—
measurable_coe 📖	mathematical	MeasurableSet	Measurable ENNReal ENNReal.measurableSpace DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike	—	Measurable.comp MeasureTheory.Measure.measurable_coe measurable
measure_le_bound 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike bound	—	LE.le.trans MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.subset_univ le_iSup
measure_sum_seq 📖	mathematical	—	MeasureTheory.Measure.sum DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike seq	—	instCountableNat sum_apply kernel_sum_seq
not_isMarkovKernel_zero 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel instZero	—	MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure NeZero.charZero_one ENNReal.instCharZero
nsmul_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike instSMulNat AddMonoid.toNatSMul AddCommMonoid.toAddMonoid MeasureTheory.Measure.instAddCommMonoid	—	—
sum_add 📖	mathematical	—	sum ProbabilityTheory.Kernel instAdd	—	ext MeasureTheory.Measure.ext MeasureTheory.Measure.sum_apply Summable.tsum_add ENNReal.instT2Space ENNReal.instContinuousAdd SummationFilter.instNeBotUnconditional ENNReal.summable
sum_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike sum MeasureTheory.Measure.sum	—	—
sum_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike sum tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace SummationFilter.unconditional	—	sum_apply MeasureTheory.Measure.sum_apply
sum_comm 📖	mathematical	—	sum	—	ext MeasureTheory.Measure.ext MeasureTheory.Measure.sum_comm
sum_fintype 📖	mathematical	—	sum Finite.to_countable Finite.of_fintype Finset.sum ProbabilityTheory.Kernel instAddCommMonoid Finset.univ	—	ext Finite.to_countable Finite.of_fintype MeasureTheory.Measure.ext sum_apply' tsum_fintype SummationFilter.instLeAtTopUnconditional finset_sum_apply'
sum_zero 📖	mathematical	—	sum ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext sum_apply' tsum_zero
zero_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike instZero MeasureTheory.Measure.instZero	—	—

ProbabilityTheory.Kernel.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSFiniteKernel 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel	—	instCountableNat ProbabilityTheory.isFiniteKernel_zero ProbabilityTheory.Kernel.ext MeasureTheory.Measure.ext ProbabilityTheory.Kernel.sum_apply' tsum_ite_eq SummationFilter.instLeAtTopUnconditional

ProbabilityTheory.Kernel.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instAdd	—	instCountableNat ProbabilityTheory.IsFiniteKernel.add ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.sum_add ProbabilityTheory.Kernel.kernel_sum_seq
finset_sum 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	Finset.sum ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instAddCommMonoid	—	Finset.induction Finset.sum_empty ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.isFiniteKernel_zero Finset.sum_insert Finset.mem_insert_of_mem add Finset.mem_insert_self

---

← Back to Index