Basic

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

Statistics

Metric	Count
Definitions boolKernel, comapRight, const, copy, deterministic, discard, id, ofFunOfCountable, piecewise, restrict, swap	11
Theorems comapRight, piecewise, restrict, comapRight, piecewise, comapRight, piecewise, restrict, boolKernel_apply, boolKernel_false, boolKernel_true, comapRight_apply, comapRight_apply', comapRight_id, instIsFiniteKernel, instIsMarkovKernel, instIsSFiniteKernel, instIsZeroOrMarkovKernel, const_add, const_apply, const_zero, copy_apply, deterministic_apply, deterministic_apply', deterministic_congr, discard_apply, discard_eq_const, eq_boolKernel, exists_ae_eq_isMarkovKernel, id_apply, instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure, instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure, instIsMarkovKernelId, instIsMarkovKernelProdCopy, instIsMarkovKernelProdSwap, instIsMarkovKernelUnitDiscard, instIsSFiniteKernelBoolBoolKernelOfSFinite, instNonemptySubtypeIsMarkovKernel, isMarkovKernel_deterministic, isSFiniteKernel_const, lintegral_const, lintegral_deterministic, lintegral_deterministic', lintegral_id, lintegral_id', lintegral_piecewise, lintegral_restrict, piecewise_apply, piecewise_apply', restrict_apply, restrict_apply', restrict_const, restrict_univ, setLIntegral_const, setLIntegral_deterministic, setLIntegral_deterministic', setLIntegral_piecewise, setLIntegral_restrict, sum_const, swap_apply, swap_apply'	61
Total	72

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
boolKernel 📖	CompOp	13 math math: instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure, ProbabilityTheory.boolKernel_comp_measure, ProbabilityTheory.posterior_boolKernel_apply_true, boolKernel_apply, eq_boolKernel, boolKernel_false, ProbabilityTheory.posterior_boolKernel_apply_false, boolKernel_true, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_right, instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure, ProbabilityTheory.absolutelyContinuous_boolKernel_comp_left, comp_boolKernel, instIsSFiniteKernelBoolBoolKernelOfSFinite
comapRight 📖	CompOp	8 math math: compProd_fst_borelMarkovFromReal_eq_comapRight_compProd, IsMarkovKernel.comapRight, comapRight_compProd_id_prod, comapRight_id, comapRight_apply', comapRight_apply, IsSFiniteKernel.comapRight, IsFiniteKernel.comapRight
const 📖	CompOp	50 math math: ProbabilityTheory.posterior_eq_withDensity, const.instIsFiniteKernel, ProbabilityTheory.HasSubgaussianMGF_iff_kernel, MeasureTheory.Measure.condKernel_def, restrict_const, const_comp', MeasureTheory.Measure.const_comp, const.instIsSFiniteKernel, ProbabilityTheory.rnDeriv_posterior_symm, ProbabilityTheory.bayesRisk_eq_iInf_measure_of_subsingleton, sum_const, setIntegral_const, prod_const_comp, ProbabilityTheory.isRatCondKernelCDF_preCDF, ProbabilityTheory.bayesRisk_const_of_nonempty, MeasureTheory.Measure.comp_eq_comp_const_apply, integral_const, MeasureTheory.partialTraj_const, comp_const, MeasureTheory.Measure.dirac_unit_compProd_const, lintegral_const, const_prod_comp, const_zero, map_const, ProbabilityTheory.avgRisk_const_left, ProbabilityTheory.isRatCondKernelCDFAux_preCDF, ProbabilityTheory.bayesRisk_const_of_neZero, ProbabilityTheory.avgRisk_const_left', MeasureTheory.Measure.snd_dirac_unit_compProd_const, ProbabilityTheory.isCondKernelCDF_condCDF, ProbabilityTheory.bayesRisk_const, const.instIsMarkovKernel, const_add, ProbabilityTheory.rnDeriv_posterior, MeasureTheory.partialTraj_const_restrict₂, ProbabilityTheory.avgRisk_const_right, ProbabilityTheory.avgRisk_const_right', prod_const, const_apply, setLIntegral_const, ProbabilityTheory.rnDeriv_posterior_ae_prod, ProbabilityTheory.condKernel_const, discard_eq_const, const_comp, ProbabilityTheory.bayesRisk_const', MeasureTheory.Measure.condKernel_apply, isSFiniteKernel_const, Invariant.comp_const, const.instIsZeroOrMarkovKernel, MeasureTheory.Measure.compProd_const
copy 📖	CompOp	10 math math: instIsMarkovKernelProdCopy, copy_apply, MeasureTheory.Measure.compProd_id_eq_copy_comp, swap_copy, parallelComp_comp_copy, deterministic_comp_copy, ProbabilityTheory.parallelProd_posterior_comp_copy_comp, compProd_def, MeasureTheory.Measure.copy_comp_map, MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp
deterministic 📖	CompOp	37 math math: deterministic_map, setIntegral_deterministic', integral_deterministic', deterministic_comp_eq_map, deterministic_prod_apply', compProd_deterministic_apply, deterministic_apply, prod_prodMkRight_comp_deterministic_prod, deterministic_comp_deterministic, setIntegral_deterministic, id_map, setLIntegral_deterministic, partialTraj_le, isMarkovKernel_deterministic, MeasureTheory.Measure.compProd_deterministic, traj_map_frestrictLe_of_le, deterministic_comp_copy, setLIntegral_deterministic', MeasureTheory.Measure.deterministic_comp_eq_map, deterministic_prod_deterministic, lintegral_deterministic_prod, deterministic_parallelComp_deterministic, prod_prodMkLeft_comp_prod_deterministic, ProbabilityTheory.condDistrib_comp_self, deterministic_apply', compProd_def, id_comap, lintegral_prod_deterministic, ProbabilityTheory.condDistrib_const, lintegral_deterministic, comp_deterministic_eq_comap, lintegral_deterministic', id_prod_eq, partialTraj_zero, integral_deterministic, ProbabilityTheory.deterministic_comp_posterior, deterministic_congr
discard 📖	CompOp	7 math math: MeasureTheory.Measure.discard_comp, discard_apply, comp_discard, comp_discard', ProbabilityTheory.bayesRisk_discard, discard_eq_const, instIsMarkovKernelUnitDiscard
id 📖	CompOp	41 math math: partialTraj_succ_of_le, swap_swap, parallelComp_comm, lintegral_id_prod, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, MeasureTheory.Measure.compProd_id, partialTraj_le_def, id_prod_apply', id_map, ProbabilityTheory.posterior_prod_id_comp, MeasureTheory.Measure.compProd_id_eq_copy_comp, compProd_prodMkLeft_eq_comp, MeasureTheory.Measure.parallelComp_comp_compProd, parallelComp_id_right_comp_parallelComp, MeasureTheory.partialTraj_const, partialTraj_succ_self, MeasureTheory.Measure.compProd_eq_comp_prod, ProbabilityTheory.parallelProd_posterior_comp_copy_comp, ProbabilityTheory.condDistrib_self, partialTraj_self, id_apply, MeasureTheory.Measure.id_comp, lintegral_id, MeasureTheory.Measure.prod_comp_left, compProd_def, ProbabilityTheory.posterior_id, id_comap, id_comp, instIsMarkovKernelId, MeasureTheory.Measure.prod_comp_right, comp_id, id_prod_eq, instIsIrreducibleIdOfSubsingleton, MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp, parallelComp_id_left_comp_parallelComp, ProbabilityTheory.deterministic_comp_posterior, partialTraj_eq_prod, lintegral_prod_id, traj_eq_prod, lintegral_id', ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib
ofFunOfCountable 📖	CompOp	—
piecewise 📖	CompOp	9 math math: piecewise_apply', piecewise_apply, IsMarkovKernel.piecewise, lintegral_piecewise, IsFiniteKernel.piecewise, setIntegral_piecewise, setLIntegral_piecewise, integral_piecewise, IsSFiniteKernel.piecewise
restrict 📖	CompOp	17 math math: restrict_apply', setIntegral_restrict, integral_restrict, restrict_const, compProd_restrict_left, restrict_apply, setLIntegral_restrict, IsProper.restrict_eq_indicator_smul, IsProper.restrict_eq_indicator_smul', isProper_iff_restrict_eq_indicator_smul, IsSFiniteKernel.restrict, comp_restrict, compProd_restrict, IsFiniteKernel.restrict, restrict_univ, lintegral_restrict, compProd_restrict_right
swap 📖	CompOp	12 math math: instIsMarkovKernelProdSwap, MeasureTheory.Measure.swap_comp, swap_swap, swap_apply, swap_prod, swap_copy, swap_comp_eq_map, ProbabilityTheory.swap_compProd_posterior, compProd_def, ProbabilityTheory.compProd_posterior_eq_swap_comp, swap_parallelComp, swap_apply'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
boolKernel_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Bool.instMeasurableSpace MeasureTheory.Measure instFunLike boolKernel	—	—
boolKernel_false 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Bool.instMeasurableSpace MeasureTheory.Measure instFunLike boolKernel	—	—
boolKernel_true 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Bool.instMeasurableSpace MeasureTheory.Measure instFunLike boolKernel	—	—
comapRight_apply 📖	mathematical	MeasurableEmbedding	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike comapRight MeasureTheory.Measure.comap	—	—
comapRight_apply' 📖	mathematical	MeasurableEmbedding MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike comapRight Set.image	—	comapRight_apply MeasureTheory.Measure.comap_apply MeasurableEmbedding.injective MeasurableEmbedding.measurableSet_image
comapRight_id 📖	mathematical	—	comapRight MeasurableEmbedding.id	—	ext MeasurableEmbedding.id MeasureTheory.Measure.ext comapRight_apply' Set.image_congr Set.image_id'
const_add 📖	mathematical	—	const MeasureTheory.Measure MeasureTheory.Measure.instAdd ProbabilityTheory.Kernel instAdd	—	ext MeasureTheory.Measure.ext
const_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike const	—	—
const_zero 📖	mathematical	—	const MeasureTheory.Measure MeasureTheory.Measure.instZero ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext
copy_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike copy MeasureTheory.Measure.dirac	—	—
deterministic_apply 📖	mathematical	Measurable	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic MeasureTheory.Measure.dirac	—	—
deterministic_apply' 📖	mathematical	Measurable MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike deterministic Set.indicator instZeroENNReal AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	deterministic.eq_1 MeasureTheory.Measure.dirac_apply'
deterministic_congr 📖	mathematical	Measurable	deterministic	—	—
discard_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel PUnit.instMeasurableSpace MeasureTheory.Measure instFunLike discard MeasureTheory.Measure.dirac	—	deterministic_apply measurable_const
discard_eq_const 📖	mathematical	—	discard const PUnit.instMeasurableSpace MeasureTheory.Measure.dirac	—	—
eq_boolKernel 📖	mathematical	—	boolKernel DFunLike.coe ProbabilityTheory.Kernel Bool.instMeasurableSpace MeasureTheory.Measure instFunLike	—	ext MeasureTheory.Measure.ext
exists_ae_eq_isMarkovKernel 📖	mathematical	Filter.Eventually MeasureTheory.IsProbabilityMeasure DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	Filter.EventuallyEq ProbabilityTheory.IsMarkovKernel	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_toMeasurable Mathlib.Tactic.Contrapose.contrapose₂ MeasureTheory.subset_toMeasurable MeasureTheory.measure_empty add_zero ENNReal.instCanonicallyOrderedAdd MeasureTheory.measure_univ_le_add_compl Filter.mp_mem MeasureTheory.measure_eq_zero_iff_ae_notMem Filter.univ_mem'
id_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike id MeasureTheory.Measure.dirac	—	measurable_id id.eq_1 deterministic_apply
instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Bool.instMeasurableSpace boolKernel	—	max_lt MeasureTheory.measure_lt_top
instIsMarkovKernelBoolBoolKernelOfIsProbabilityMeasure 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Bool.instMeasurableSpace boolKernel	—	—
instIsMarkovKernelId 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel id	—	measurable_id id.eq_1 isMarkovKernel_deterministic
instIsMarkovKernelProdCopy 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace copy	—	copy.eq_1 isMarkovKernel_deterministic
instIsMarkovKernelProdSwap 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace swap	—	measurable_swap swap.eq_1 isMarkovKernel_deterministic
instIsMarkovKernelUnitDiscard 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel PUnit.instMeasurableSpace discard	—	measurable_const discard.eq_1 isMarkovKernel_deterministic
instIsSFiniteKernelBoolBoolKernelOfSFinite 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Bool.instMeasurableSpace boolKernel	—	instCountableNat instIsFiniteKernelBoolBoolKernelOfIsFiniteMeasure MeasureTheory.isFiniteMeasure_sfiniteSeq ext MeasureTheory.Measure.ext sum_apply MeasureTheory.sum_sfiniteSeq
instNonemptySubtypeIsMarkovKernel 📖	mathematical	—	ProbabilityTheory.Kernel ProbabilityTheory.IsMarkovKernel	—	nonempty_subtype const.instIsMarkovKernel MeasureTheory.Measure.dirac.isProbabilityMeasure
isMarkovKernel_deterministic 📖	mathematical	Measurable	ProbabilityTheory.IsMarkovKernel deterministic	—	deterministic_apply MeasureTheory.Measure.dirac.isProbabilityMeasure
isSFiniteKernel_const 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel const MeasureTheory.SFinite	—	ProbabilityTheory.IsSFiniteKernel.sFinite const.instIsSFiniteKernel
lintegral_const 📖	mathematical	—	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike const	—	const_apply
lintegral_deterministic 📖	mathematical	Measurable	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic	—	deterministic_apply MeasureTheory.lintegral_dirac
lintegral_deterministic' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic	—	deterministic_apply MeasureTheory.lintegral_dirac'
lintegral_id 📖	mathematical	—	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike id	—	id_apply MeasureTheory.lintegral_dirac
lintegral_id' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike id	—	id_apply MeasureTheory.lintegral_dirac'
lintegral_piecewise 📖	mathematical	MeasurableSet	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike piecewise ENNReal Set Set.instMembership	—	—
lintegral_restrict 📖	mathematical	MeasurableSet	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike restrict MeasureTheory.Measure.restrict	—	restrict_apply
piecewise_apply 📖	mathematical	MeasurableSet	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike piecewise Set Set.instMembership	—	—
piecewise_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike piecewise Set.instMembership	—	piecewise_apply
restrict_apply 📖	mathematical	MeasurableSet	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike restrict MeasureTheory.Measure.restrict	—	—
restrict_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike restrict Set.instInter	—	restrict_apply MeasureTheory.Measure.restrict_apply
restrict_const 📖	mathematical	MeasurableSet	restrict const MeasureTheory.Measure.restrict	—	ext MeasureTheory.Measure.ext
restrict_univ 📖	mathematical	—	restrict Set.univ MeasurableSet.univ	—	ext MeasurableSet.univ restrict_apply MeasureTheory.Measure.restrict_univ
setLIntegral_const 📖	mathematical	—	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike const	—	const_apply
setLIntegral_deterministic 📖	mathematical	Measurable	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic ENNReal Set Set.instMembership instZeroENNReal	—	deterministic_apply MeasureTheory.setLIntegral_dirac
setLIntegral_deterministic' 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike deterministic Set Set.instMembership instZeroENNReal	—	deterministic_apply MeasureTheory.setLIntegral_dirac'
setLIntegral_piecewise 📖	mathematical	MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike piecewise ENNReal Set Set.instMembership	—	—
setLIntegral_restrict 📖	mathematical	MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike restrict Set Set.instInter	—	restrict_apply MeasureTheory.Measure.restrict_restrict'
sum_const 📖	mathematical	—	sum const MeasureTheory.Measure.sum	—	—
swap_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike swap MeasureTheory.Measure.dirac	—	measurable_swap swap.eq_1 deterministic_apply
swap_apply' 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike swap Set.indicator instZeroENNReal Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	—	swap_apply MeasureTheory.Measure.dirac_apply'

ProbabilityTheory.Kernel.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comapRight 📖	mathematical	MeasurableEmbedding	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.comapRight	—	ProbabilityTheory.Kernel.bound_lt_top ProbabilityTheory.Kernel.comapRight_apply' MeasurableSet.univ ProbabilityTheory.Kernel.measure_le_bound
piecewise 📖	mathematical	MeasurableSet	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.piecewise	—	max_lt ProbabilityTheory.Kernel.bound_lt_top ProbabilityTheory.Kernel.piecewise_apply' LE.le.trans ite_le_sup sup_le_sup ProbabilityTheory.Kernel.measure_le_bound
restrict 📖	mathematical	MeasurableSet	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.restrict	—	ProbabilityTheory.Kernel.bound_lt_top ProbabilityTheory.Kernel.restrict_apply' MeasurableSet.univ ProbabilityTheory.Kernel.measure_le_bound

ProbabilityTheory.Kernel.IsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comapRight 📖	mathematical	MeasurableEmbedding DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel ProbabilityTheory.Kernel.instFunLike Set.range AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.comapRight	—	ProbabilityTheory.Kernel.comapRight_apply' MeasurableSet.univ Set.image_univ
piecewise 📖	mathematical	MeasurableSet	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.piecewise	—	ProbabilityTheory.Kernel.piecewise_apply' MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure'

ProbabilityTheory.Kernel.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comapRight 📖	mathematical	MeasurableEmbedding	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.comapRight	—	instCountableNat ProbabilityTheory.Kernel.IsFiniteKernel.comapRight ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.ext ProbabilityTheory.Kernel.sum_apply ProbabilityTheory.Kernel.comapRight_apply MeasureTheory.Measure.ext MeasureTheory.Measure.comap_apply MeasurableEmbedding.injective MeasurableEmbedding.measurableSet_image MeasureTheory.Measure.sum_apply ProbabilityTheory.Kernel.measure_sum_seq
piecewise 📖	mathematical	MeasurableSet	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.piecewise	—	instCountableNat ProbabilityTheory.Kernel.IsFiniteKernel.piecewise ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.ext ProbabilityTheory.Kernel.measure_sum_seq
restrict 📖	mathematical	MeasurableSet	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.restrict	—	instCountableNat ProbabilityTheory.Kernel.IsFiniteKernel.restrict ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.ext MeasureTheory.Measure.restrict_sum ProbabilityTheory.Kernel.kernel_sum_seq

ProbabilityTheory.Kernel.const

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsFiniteKernel 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.const	—	MeasureTheory.measure_lt_top le_rfl
instIsMarkovKernel 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.const	—	—
instIsSFiniteKernel 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.const	—	instCountableNat instIsFiniteKernel MeasureTheory.isFiniteMeasure_sfiniteSeq ProbabilityTheory.Kernel.sum_const MeasureTheory.sum_sfiniteSeq
instIsZeroOrMarkovKernel 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.const	—	MeasureTheory.eq_zero_or_isProbabilityMeasure ProbabilityTheory.Kernel.const_zero ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernel

---

← Back to Index