MapComap

📁 Source: Mathlib/Probability/Kernel/Composition/MapComap.lean

Statistics

Metric	Count
Definitions comap, fst, map, mapOfMeasurable, prodMkLeft, prodMkRight, sectL, sectR, snd, swapLeft, swapRight	11
Theorems comap, fst, map, prodMkLeft, prodMkRight, snd, swapLeft, swapRight, comap, fst, map, prodMkLeft, prodMkRight, snd, swapLeft, swapRight, comap, fst, map, prodMkLeft, prodMkRight, snd, swapLeft, swapRight, comap, fst, map, prodMkLeft, prodMkRight, snd, swapRight, coe_comap, comap_apply, comap_apply', comap_comp_right, comap_id, comap_id', comap_map_comm, comap_sectL, comap_sectR, comap_zero, deterministic_map, fst_apply, fst_apply', fst_eq, fst_map_id_prod, fst_map_prod, fst_prodMkLeft, fst_prodMkRight, fst_real_apply, fst_swapRight, fst_zero, id_comap, id_map, instIsFiniteKernelSectLOfProd, instIsFiniteKernelSectROfProd, instIsMarkovKernelProdOfSectL, instIsMarkovKernelProdOfSectR, instIsMarkovKernelSectLOfProd, instIsMarkovKernelSectROfProd, instIsSFiniteKernelSectLOfProd, instIsSFiniteKernelSectROfProd, instIsZeroOrMarkovKernelSectLOfProd, instIsZeroOrMarkovKernelSectROfProd, instNeZeroMeasureCoeSectLOfProdMk, instNeZeroMeasureCoeSectROfProdMk, isFiniteKernel_of_isFiniteKernel_fst, isFiniteKernel_of_isFiniteKernel_snd, isSFiniteKernel_prodMkLeft_iff, isSFiniteKernel_prodMkLeft_unit, isSFiniteKernel_prodMkRight_iff, isSFiniteKernel_prodMkRight_unit, lintegral_comap, lintegral_fst, lintegral_map, lintegral_prodMkLeft, lintegral_prodMkRight, lintegral_snd, lintegral_swapLeft, lintegral_swapRight, mapOfMeasurable_eq_map, map_apply, map_apply', map_apply_eq_iff_map_symm_apply_eq, map_comp_right, map_const, map_id, map_id', map_of_not_measurable, map_prodMkLeft, map_prodMkRight, map_zero, prodMkLeft_add, prodMkLeft_apply, prodMkLeft_apply', prodMkLeft_zero, prodMkRight_add, prodMkRight_apply, prodMkRight_apply', prodMkRight_zero, sectL_apply, sectL_prodMkLeft, sectL_prodMkRight, sectL_swapRight, sectL_zero, sectR_apply, sectR_prodMkLeft, sectR_prodMkRight, sectR_swapRight, sectR_zero, snd_apply, snd_apply', snd_eq, snd_map_prod, snd_map_prod_id, snd_prodMkLeft, snd_prodMkRight, snd_swapRight, snd_zero, sum_comap_seq, sum_map_seq, sum_prodMkLeft, sum_prodMkRight, swapLeft_apply, swapLeft_apply', swapLeft_prodMkLeft, swapLeft_prodMkRight, swapLeft_zero, swapRight_apply, swapRight_apply', swapRight_eq, swapRight_zero	132
Total	143

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
comap 📖	CompOp	25 math math: sum_comap_seq, MeasureTheory.Measure.condKernel_def, IsMarkovKernel.comap, comap_prod, comap_id', ProbabilityTheory.condExpKernel_def, comap_sectL, comap_id, lintegral_comap, comap_comp_right, IsFiniteKernel.comap, comp_map, compProd_assoc, id_comap, ProbabilityTheory.condExpKernel_eq, IsSFiniteKernel.comap, comap_apply, comap_zero, comp_deterministic_eq_comap, comap_prod_swap, comap_sectR, IsZeroOrMarkovKernel.comap, comap_map_comm, comap_apply', coe_comap
fst 📖	CompOp	45 math math: density_fst_univ, ProbabilityTheory.setIntegral_condKernel_univ_left, fst_prod, ProbabilityTheory.setLIntegral_condKernel_univ_right, lintegral_fst, IsSFiniteKernel.fst, ProbabilityTheory.setIntegral_condKernel_univ_right, IsCondKernel.isProbabilityMeasure_ae, fst_comp, isCondKernelCDF_condKernelCDF, fst_prodMkRight, fst_real_apply, IsMarkovKernel.fst, fst_apply, ProbabilityTheory.setLIntegral_condKernel, ProbabilityTheory.lintegral_condKernel, fst_prodMkLeft, condKernel_apply_eq_condKernel, densityProcess_fst_univ_ae, ProbabilityTheory.setLIntegral_condKernel_univ_left, MeasureTheory.AEStronglyMeasurable.integral_kernel_condKernel, compProd_fst_condKernelReal, tendsto_densityProcess_fst_atTop_univ_of_monotone, isRatCondKernelCDF_density_Iic, disintegrate, fst_apply', ProbabilityTheory.setIntegral_condKernel, fst_eq, IsFiniteKernel.fst, fst_swapRight, isRatCondKernelCDFAux_density_Iic, tendsto_densityProcess_fst_atTop_ae_of_monotone, ProbabilityTheory.setLIntegral_condKernel_eq_measure_prod, fst_map_id_prod, IsCondKernel.disintegrate, densityProcess_fst_univ, fst_compProd, ProbabilityTheory.integral_condKernel, fst_map_prod, ProbabilityTheory.lintegral_condKernel_mem, snd_swapRight, tendsto_density_fst_atTop_ae_of_monotone, IsZeroOrMarkovKernel.fst, fst_zero, fst_compProd_apply
map 📖	CompOp	64 math math: deterministic_map, partialTraj_succ_of_le, map_apply, map_id', deterministic_comp_eq_map, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim, map_partialTraj_succ_self, MeasureTheory.Measure.map_comp, map_comp_right, map_apply', IsFiniteKernel.map, map_prod_eq, ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map, IsSFiniteKernel.map, ProbabilityTheory.condDistrib_apply_ae_eq_condExpKernel_map, lintegral_map, MeasureTheory.Measure.compProd_map, partialTraj_le_def, ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, id_map, prodAssoc_symm_prod, prodAssoc_prod, snd_map_prod, ProbabilityTheory.condDistrib_comp, partialTraj_succ_map_frestrictLe₂, MeasureTheory.partialTraj_const, partialTraj_succ_self, swap_comp_eq_map, snd_map_prod_id, traj_map_frestrictLe_of_le, HasSubgaussianMGF.id_map_iff, swapRight_eq, prodComm_prod, snd_eq, mapOfMeasurable_eq_map, fst_eq, map_comp, map_const, comp_map, IsZeroOrMarkovKernel.map, traj_map_frestrictLe, map_prodMkRight, compProd_assoc, fst_map_id_prod, MeasureTheory.partialTraj_const_restrict₂, map_traj_succ_self, indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map, IsMarkovKernel.map, map_prodMkLeft, partialTraj_map_frestrictLe₂, map_prod_map, ProbabilityTheory.bayesRisk_le_bayesRisk_map, sum_map_seq, fst_map_prod, comap_prod_swap, map_prod_swap, lmarginalPartialTraj_eq_lintegral_map, comap_map_comm, map_apply_eq_iff_map_symm_apply_eq, partialTraj_eq_prod, map_zero, map_id, map_of_not_measurable, traj_eq_prod
mapOfMeasurable 📖	CompOp	1 math math: mapOfMeasurable_eq_map
prodMkLeft 📖	CompOp	27 math math: IsSFiniteKernel.prodMkLeft, HasSubgaussianMGF.add_comp, prodMkLeft_apply, comp_eq_snd_compProd, swapLeft_prodMkRight, prodMkLeft_add, snd_compProd_prodMkLeft, fst_prodMkLeft, isSFiniteKernel_prodMkLeft_unit, compProd_prodMkLeft_eq_comp, snd_prodMkLeft, prodMkLeft_apply', swapLeft_prodMkLeft, sectL_prodMkLeft, prod_prodMkLeft_comp_prod_deterministic, sectR_prodMkLeft, lintegral_prodMkLeft, map_prodMkLeft, IsZeroOrMarkovKernel.prodMkLeft, isSFiniteKernel_prodMkLeft_iff, MeasureTheory.Measure.prodMkLeft_comp_compProd, comap_prod_swap, HasSubgaussianMGF.prodMkLeft_compProd, prodMkLeft_zero, IsMarkovKernel.prodMkLeft, IsFiniteKernel.prodMkLeft, sum_prodMkLeft
prodMkRight 📖	CompOp	23 math math: sectR_prodMkRight, isSFiniteKernel_prodMkRight_iff, fst_prodMkRight, prodMkRight_add, swapLeft_prodMkRight, isSFiniteKernel_prodMkRight_unit, prod_prodMkRight_comp_deterministic_prod, lintegral_prodMkRight, prodMkRight_zero, snd_prodMkRight, IsFiniteKernel.prodMkRight, prodMkRight_apply, sectL_prodMkRight, IsSFiniteKernel.prodMkRight, swapLeft_prodMkLeft, IsMarkovKernel.prodMkRight, prodMkRight_apply', map_prodMkRight, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkRight, ProbabilityTheory.condIndepFun_iff_condDistrib_prod_ae_eq_prodMkLeft, sum_prodMkRight, IsZeroOrMarkovKernel.prodMkRight, comap_prod_swap
sectL 📖	CompOp	12 math math: sectR_swapRight, instIsZeroOrMarkovKernelSectLOfProd, sectL_prodMkRight, instIsSFiniteKernelSectLOfProd, sectL_swapRight, instNeZeroMeasureCoeSectLOfProdMk, comap_sectL, sectL_zero, sectL_prodMkLeft, sectL_apply, instIsFiniteKernelSectLOfProd, instIsMarkovKernelSectLOfProd
sectR 📖	CompOp	13 math math: sectR_apply, instIsFiniteKernelSectROfProd, sectR_prodMkRight, instNeZeroMeasureCoeSectROfProdMk, instIsMarkovKernelSectROfProd, sectR_swapRight, instIsSFiniteKernelSectROfProd, sectL_swapRight, sectR_zero, sectR_prodMkLeft, compProd_apply_eq_compProd_sectR, comap_sectR, instIsZeroOrMarkovKernelSectROfProd
snd 📖	CompOp	19 math math: snd_comp, snd_zero, comp_eq_snd_compProd, snd_compProd_prodMkLeft, snd_prodMkRight, snd_map_prod, snd_prod, IsFiniteKernel.snd, snd_map_prod_id, snd_prodMkLeft, lintegral_snd, IsZeroOrMarkovKernel.snd, IsMarkovKernel.snd, snd_eq, snd_apply', snd_apply, fst_swapRight, IsSFiniteKernel.snd, snd_swapRight
swapLeft 📖	CompOp	11 math math: swapLeft_zero, swapLeft_prodMkRight, IsMarkovKernel.swapLeft, sectR_swapRight, IsFiniteKernel.swapLeft, sectL_swapRight, IsSFiniteKernel.swapLeft, swapLeft_prodMkLeft, swapLeft_apply', lintegral_swapLeft, swapLeft_apply
swapRight 📖	CompOp	11 math math: lintegral_swapRight, swapRight_apply', swapRight_apply, IsMarkovKernel.swapRight, IsZeroOrMarkovKernel.swapRight, swapRight_eq, fst_swapRight, swapRight_zero, snd_swapRight, IsFiniteKernel.swapRight, IsSFiniteKernel.swapRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comap 📖	mathematical	Measurable	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike comap	—	—
comap_apply 📖	mathematical	Measurable	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike comap	—	—
comap_apply' 📖	mathematical	Measurable	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike comap	—	—
comap_comp_right 📖	mathematical	Measurable	comap Measurable.comp	—	ext Measurable.comp MeasureTheory.Measure.ext
comap_id 📖	mathematical	—	comap measurable_id	—	ext measurable_id MeasureTheory.Measure.ext
comap_id' 📖	mathematical	—	comap measurable_id	—	comap_id
comap_map_comm 📖	mathematical	Measurable	comap map	—	ext MeasureTheory.Measure.ext comap_apply map_apply
comap_sectL 📖	mathematical	Measurable	comap sectL Prod.instMeasurableSpace Measurable.prodMk measurable_const	—	ext Measurable.prodMk measurable_const MeasureTheory.Measure.ext comap_apply sectL_apply
comap_sectR 📖	mathematical	Measurable	comap sectR Prod.instMeasurableSpace Measurable.prodMk measurable_const	—	ext Measurable.prodMk measurable_const MeasureTheory.Measure.ext comap_apply sectR_apply
comap_zero 📖	mathematical	Measurable	comap ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext
deterministic_map 📖	mathematical	Measurable	map deterministic Measurable.comp	—	Measurable.comp id_map map_comp_right
fst_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike fst MeasureTheory.Measure.map Prod.instMeasurableSpace	—	—
fst_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike fst Prod.instMeasurableSpace setOf Set.instMembership	—	fst_apply MeasureTheory.Measure.map_apply measurable_fst
fst_eq 📖	mathematical	—	fst map Prod.instMeasurableSpace	—	mapOfMeasurable_eq_map measurable_fst
fst_map_id_prod 📖	mathematical	Measurable	fst map Prod.instMeasurableSpace	—	fst_map_prod map_id'
fst_map_prod 📖	mathematical	Measurable	fst map Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext fst_apply' map_apply' Measurable.prod measurable_fst Mathlib.Tactic.Contrapose.contrapose₄ Measurable.fst map_of_not_measurable fst_zero
fst_prodMkLeft 📖	mathematical	—	fst Prod.instMeasurableSpace prodMkLeft	—	—
fst_prodMkRight 📖	mathematical	—	fst Prod.instMeasurableSpace prodMkRight	—	—
fst_real_apply 📖	mathematical	MeasurableSet	MeasureTheory.Measure.real DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike fst Prod.instMeasurableSpace setOf Set Set.instMembership	—	fst_apply'
fst_swapRight 📖	mathematical	—	fst swapRight snd	—	ext MeasureTheory.Measure.ext fst_apply' swapRight_apply' measurable_fst snd_apply'
fst_zero 📖	mathematical	—	fst ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	measurable_fst mapOfMeasurable_eq_map map_zero
id_comap 📖	mathematical	Measurable	comap id deterministic	—	ext MeasureTheory.Measure.ext comap_apply deterministic_apply id_apply
id_map 📖	mathematical	Measurable	map id deterministic	—	ext MeasureTheory.Measure.ext map_apply deterministic_apply id_apply MeasureTheory.Measure.map_dirac
instIsFiniteKernelSectLOfProd 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel sectL	—	sectL.eq_1 IsFiniteKernel.comap
instIsFiniteKernelSectROfProd 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel sectR	—	sectR.eq_1 IsFiniteKernel.comap
instIsMarkovKernelProdOfSectL 📖	mathematical	ProbabilityTheory.IsMarkovKernel sectL	Prod.instMeasurableSpace	—	sectL_apply MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure'
instIsMarkovKernelProdOfSectR 📖	mathematical	ProbabilityTheory.IsMarkovKernel sectR	Prod.instMeasurableSpace	—	sectR_apply MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure'
instIsMarkovKernelSectLOfProd 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel sectL	—	sectL.eq_1 IsMarkovKernel.comap
instIsMarkovKernelSectROfProd 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel sectR	—	sectR.eq_1 IsMarkovKernel.comap
instIsSFiniteKernelSectLOfProd 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel sectL	—	sectL.eq_1 IsSFiniteKernel.comap
instIsSFiniteKernelSectROfProd 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel sectR	—	sectR.eq_1 IsSFiniteKernel.comap
instIsZeroOrMarkovKernelSectLOfProd 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel sectL	—	sectL.eq_1 IsZeroOrMarkovKernel.comap
instIsZeroOrMarkovKernelSectROfProd 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel sectR	—	sectR.eq_1 IsZeroOrMarkovKernel.comap
instNeZeroMeasureCoeSectLOfProdMk 📖	mathematical	—	MeasureTheory.Measure MeasureTheory.Measure.instZero DFunLike.coe ProbabilityTheory.Kernel instFunLike sectL	—	sectL_apply
instNeZeroMeasureCoeSectROfProdMk 📖	mathematical	—	MeasureTheory.Measure MeasureTheory.Measure.instZero DFunLike.coe ProbabilityTheory.Kernel instFunLike sectR	—	sectR_apply
isFiniteKernel_of_isFiniteKernel_fst 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace	—	bound_lt_top le_trans fst_apply' MeasurableSet.univ measure_le_bound
isFiniteKernel_of_isFiniteKernel_snd 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace	—	bound_lt_top le_trans snd_apply' MeasurableSet.univ measure_le_bound
isSFiniteKernel_prodMkLeft_iff 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace prodMkLeft	—	sectR_prodMkLeft instIsSFiniteKernelSectROfProd IsSFiniteKernel.prodMkLeft
isSFiniteKernel_prodMkLeft_unit 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace PUnit.instMeasurableSpace prodMkLeft	—	Measurable.prodMk measurable_const measurable_id' IsSFiniteKernel.comap IsSFiniteKernel.prodMkLeft
isSFiniteKernel_prodMkRight_iff 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace prodMkRight	—	sectL_prodMkRight instIsSFiniteKernelSectLOfProd IsSFiniteKernel.prodMkRight
isSFiniteKernel_prodMkRight_unit 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace PUnit.instMeasurableSpace prodMkRight	—	Measurable.prodMk measurable_id' measurable_const IsSFiniteKernel.comap IsSFiniteKernel.prodMkRight
lintegral_comap 📖	mathematical	Measurable	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike comap	—	—
lintegral_fst 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike fst Prod.instMeasurableSpace	—	fst_eq lintegral_map measurable_fst
lintegral_map 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike map	—	map_apply MeasureTheory.lintegral_map
lintegral_prodMkLeft 📖	mathematical	—	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike prodMkLeft	—	—
lintegral_prodMkRight 📖	mathematical	—	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike prodMkRight	—	—
lintegral_snd 📖	mathematical	Measurable ENNReal ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike snd Prod.instMeasurableSpace	—	snd_eq lintegral_map measurable_snd
lintegral_swapLeft 📖	mathematical	—	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike swapLeft	—	swapLeft_apply
lintegral_swapRight 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike swapRight	—	swapRight_eq lintegral_map measurable_swap
mapOfMeasurable_eq_map 📖	mathematical	Measurable	mapOfMeasurable map	—	—
map_apply 📖	mathematical	Measurable	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike map MeasureTheory.Measure.map	—	—
map_apply' 📖	mathematical	Measurable MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike map Set.preimage	—	map_apply MeasureTheory.Measure.map_apply
map_apply_eq_iff_map_symm_apply_eq 📖	mathematical	—	map DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm	—	map_apply MeasurableEquiv.measurable MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq
map_comp_right 📖	mathematical	Measurable	map	—	ext map_apply MeasureTheory.Measure.map_map Measurable.comp
map_const 📖	mathematical	Measurable	map const MeasureTheory.Measure.map	—	ext MeasureTheory.Measure.ext map_apply' const_apply MeasureTheory.Measure.map_apply
map_id 📖	mathematical	—	map	—	ext MeasureTheory.Measure.ext map_apply MeasureTheory.Measure.map_id
map_id' 📖	mathematical	—	map	—	map_id
map_of_not_measurable 📖	mathematical	Measurable	map ProbabilityTheory.Kernel instZero	—	—
map_prodMkLeft 📖	mathematical	—	map Prod.instMeasurableSpace prodMkLeft	—	map_of_not_measurable prodMkLeft_zero
map_prodMkRight 📖	mathematical	—	map Prod.instMeasurableSpace prodMkRight	—	map_of_not_measurable prodMkRight_zero
map_zero 📖	mathematical	—	map ProbabilityTheory.Kernel instZero	—	ext MeasureTheory.Measure.ext map_apply MeasureTheory.Measure.map_zero map_of_not_measurable
prodMkLeft_add 📖	mathematical	—	prodMkLeft ProbabilityTheory.Kernel instAdd Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext
prodMkLeft_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike prodMkLeft	—	—
prodMkLeft_apply' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel Prod.instMeasurableSpace instFunLike prodMkLeft	—	—
prodMkLeft_zero 📖	mathematical	—	prodMkLeft ProbabilityTheory.Kernel instZero Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext
prodMkRight_add 📖	mathematical	—	prodMkRight ProbabilityTheory.Kernel instAdd Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext
prodMkRight_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike prodMkRight	—	—
prodMkRight_apply' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel Prod.instMeasurableSpace instFunLike prodMkRight	—	—
prodMkRight_zero 📖	mathematical	—	prodMkRight ProbabilityTheory.Kernel instZero Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext
sectL_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike sectL Prod.instMeasurableSpace	—	—
sectL_prodMkLeft 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike sectL prodMkLeft	—	—
sectL_prodMkRight 📖	mathematical	—	sectL prodMkRight	—	—
sectL_swapRight 📖	mathematical	—	sectL swapLeft sectR	—	—
sectL_zero 📖	mathematical	—	sectL ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	comap_zero
sectR_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike sectR Prod.instMeasurableSpace	—	—
sectR_prodMkLeft 📖	mathematical	—	sectR prodMkLeft	—	—
sectR_prodMkRight 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike sectR prodMkRight	—	—
sectR_swapRight 📖	mathematical	—	sectR swapLeft sectL	—	—
sectR_zero 📖	mathematical	—	sectR ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	comap_zero
snd_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike snd MeasureTheory.Measure.map Prod.instMeasurableSpace	—	—
snd_apply' 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike snd Prod.instMeasurableSpace Set.preimage	—	snd_apply MeasureTheory.Measure.map_apply measurable_snd
snd_eq 📖	mathematical	—	snd map Prod.instMeasurableSpace	—	mapOfMeasurable_eq_map measurable_snd
snd_map_prod 📖	mathematical	Measurable	snd map Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext snd_apply' map_apply' Measurable.prod measurable_snd Mathlib.Tactic.Contrapose.contrapose₄ Measurable.snd map_of_not_measurable snd_zero
snd_map_prod_id 📖	mathematical	Measurable	snd map Prod.instMeasurableSpace	—	snd_map_prod map_id'
snd_prodMkLeft 📖	mathematical	—	snd Prod.instMeasurableSpace prodMkLeft	—	—
snd_prodMkRight 📖	mathematical	—	snd Prod.instMeasurableSpace prodMkRight	—	—
snd_swapRight 📖	mathematical	—	snd swapRight fst	—	ext MeasureTheory.Measure.ext snd_apply' swapRight_apply' measurable_snd fst_apply'
snd_zero 📖	mathematical	—	snd ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	measurable_snd mapOfMeasurable_eq_map map_zero
sum_comap_seq 📖	mathematical	Measurable	sum instCountableNat comap seq	—	ext instCountableNat MeasureTheory.Measure.ext sum_apply comap_apply' MeasureTheory.Measure.sum_apply measure_sum_seq
sum_map_seq 📖	mathematical	—	sum instCountableNat map seq	—	instCountableNat ext MeasureTheory.Measure.ext sum_apply map_apply' MeasureTheory.Measure.sum_apply measure_sum_seq sum.congr_simp map_of_not_measurable sum_zero
sum_prodMkLeft 📖	mathematical	—	sum Prod.instMeasurableSpace prodMkLeft	—	ext MeasureTheory.Measure.ext
sum_prodMkRight 📖	mathematical	—	sum Prod.instMeasurableSpace prodMkRight	—	ext MeasureTheory.Measure.ext
swapLeft_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike swapLeft	—	—
swapLeft_apply' 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel Prod.instMeasurableSpace instFunLike swapLeft	—	—
swapLeft_prodMkLeft 📖	mathematical	—	swapLeft prodMkLeft prodMkRight	—	—
swapLeft_prodMkRight 📖	mathematical	—	swapLeft prodMkRight prodMkLeft	—	—
swapLeft_zero 📖	mathematical	—	swapLeft ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	comap_zero measurable_swap
swapRight_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike swapRight MeasureTheory.Measure.map	—	—
swapRight_apply' 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike swapRight setOf Set.instMembership	—	swapRight_apply MeasureTheory.Measure.map_apply measurable_swap
swapRight_eq 📖	mathematical	—	swapRight map Prod.instMeasurableSpace	—	mapOfMeasurable_eq_map measurable_swap
swapRight_zero 📖	mathematical	—	swapRight ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	measurable_swap mapOfMeasurable_eq_map map_zero

ProbabilityTheory.Kernel.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Measurable	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.comap	—	ProbabilityTheory.Kernel.bound_lt_top ProbabilityTheory.Kernel.comap_apply' ProbabilityTheory.Kernel.measure_le_bound
fst 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.fst	—	ProbabilityTheory.Kernel.fst_eq map
map 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.map	—	ProbabilityTheory.Kernel.bound_lt_top ProbabilityTheory.Kernel.map_apply' MeasurableSet.univ ProbabilityTheory.Kernel.measure_le_bound ProbabilityTheory.Kernel.map_of_not_measurable ENNReal.instCanonicallyOrderedAdd
prodMkLeft 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkLeft	—	measurable_snd ProbabilityTheory.Kernel.prodMkLeft.eq_1 comap
prodMkRight 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkRight	—	measurable_fst ProbabilityTheory.Kernel.prodMkRight.eq_1 comap
snd 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel ProbabilityTheory.Kernel.snd	—	ProbabilityTheory.Kernel.snd_eq map
swapLeft 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.swapLeft	—	measurable_swap ProbabilityTheory.Kernel.swapLeft.eq_1 comap
swapRight 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.swapRight	—	ProbabilityTheory.Kernel.swapRight_eq map

ProbabilityTheory.Kernel.IsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Measurable	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.comap	—	ProbabilityTheory.Kernel.comap_apply' MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure'
fst 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.fst	—	ProbabilityTheory.Kernel.fst_eq map measurable_fst
map 📖	mathematical	Measurable	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.map	—	ProbabilityTheory.Kernel.map_apply' MeasurableSet.univ Set.preimage_univ MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure'
prodMkLeft 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkLeft	—	measurable_snd ProbabilityTheory.Kernel.prodMkLeft.eq_1 comap
prodMkRight 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkRight	—	measurable_fst ProbabilityTheory.Kernel.prodMkRight.eq_1 comap
snd 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel ProbabilityTheory.Kernel.snd	—	ProbabilityTheory.Kernel.snd_eq map measurable_snd
swapLeft 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.swapLeft	—	measurable_swap ProbabilityTheory.Kernel.swapLeft.eq_1 comap
swapRight 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.swapRight	—	ProbabilityTheory.Kernel.swapRight_eq map measurable_swap

ProbabilityTheory.Kernel.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Measurable	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.comap	—	instCountableNat ProbabilityTheory.Kernel.IsFiniteKernel.comap ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.sum_comap_seq
fst 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.fst	—	ProbabilityTheory.Kernel.fst_eq map
map 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.map	—	instCountableNat ProbabilityTheory.Kernel.IsFiniteKernel.map ProbabilityTheory.Kernel.isFiniteKernel_seq ProbabilityTheory.Kernel.sum_map_seq
prodMkLeft 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkLeft	—	measurable_snd ProbabilityTheory.Kernel.prodMkLeft.eq_1 comap
prodMkRight 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkRight	—	measurable_fst ProbabilityTheory.Kernel.prodMkRight.eq_1 comap
snd 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel ProbabilityTheory.Kernel.snd	—	ProbabilityTheory.Kernel.snd_eq map
swapLeft 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.swapLeft	—	measurable_swap ProbabilityTheory.Kernel.swapLeft.eq_1 comap
swapRight 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.swapRight	—	ProbabilityTheory.Kernel.swapRight_eq map

ProbabilityTheory.Kernel.IsZeroOrMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comap 📖	mathematical	Measurable	ProbabilityTheory.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.comap	—	ProbabilityTheory.eq_zero_or_isMarkovKernel ProbabilityTheory.Kernel.comap_zero ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel ProbabilityTheory.Kernel.IsMarkovKernel.comap ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel
fst 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.fst	—	ProbabilityTheory.Kernel.fst_eq map
map 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.map	—	ProbabilityTheory.eq_zero_or_isMarkovKernel ProbabilityTheory.Kernel.map_zero ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel ProbabilityTheory.Kernel.IsMarkovKernel.map ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.map_of_not_measurable
prodMkLeft 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkLeft	—	measurable_snd ProbabilityTheory.Kernel.prodMkLeft.eq_1 comap
prodMkRight 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.prodMkRight	—	measurable_fst ProbabilityTheory.Kernel.prodMkRight.eq_1 comap
snd 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.snd	—	ProbabilityTheory.Kernel.snd_eq map
swapRight 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.swapRight	—	ProbabilityTheory.Kernel.swapRight_eq map

---

← Back to Index