CompProd

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

Statistics

Metric	Count
Definitions compProd, «term_⊗ₖ_»	2
Theorems compProd, compProd, compProd, compProd, ae_ae_of_ae_compProd, ae_compProd_iff, ae_compProd_of_ae_ae, ae_kernel_lt_top, ae_null_of_compProd_null, comapRight_compProd_id_prod, compProd_add_left, compProd_add_right, compProd_apply, compProd_apply_prod, compProd_apply_univ, compProd_apply_univ_le, compProd_assoc, compProd_congr, compProd_def, compProd_deterministic_apply, compProd_eq_sum_compProd, compProd_eq_sum_compProd_left, compProd_eq_sum_compProd_right, compProd_eq_tsum_compProd, compProd_eq_zero_iff, compProd_null, compProd_of_not_isSFiniteKernel_left, compProd_of_not_isSFiniteKernel_right, compProd_preimage_fst, compProd_restrict, compProd_restrict_left, compProd_restrict_right, compProd_sum_left, compProd_sum_right, compProd_zero_left, compProd_zero_right, fst_compProd, fst_compProd_apply, le_compProd_apply, lintegral_compProd, lintegral_compProd', lintegral_compProd₀, setLIntegral_compProd, setLIntegral_compProd_univ_left, setLIntegral_compProd_univ_right	45
Total	47

ProbabilityTheory

Definitions

Name	Category	Theorems
«term_⊗ₖ_» 📖	CompOp	—

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
compProd 📖	CompOp	58 math math: ae_compProd_of_ae_ae, IsMarkovKernel.compProd, MeasureTheory.Measure.comp_compProd_comm, compProd_congr, HasSubgaussianMGF.add_compProd, compProd_null, ae_compProd_iff, compProd_restrict_left, HasSubgaussianMGF.integrable_exp_add_compProd, HasSubgaussianMGF.add_comp, compProd_zero_right, compProd_of_not_isSFiniteKernel_right, compProd_deterministic_apply, compProd_eq_tsum_compProd, comapRight_compProd_id_prod, comp_eq_snd_compProd, le_compProd_apply, snd_compProd_prodMkLeft, compProd_eq_sum_compProd, ProbabilityTheory.bayesRisk_compProd_le_bayesRisk, MeasureTheory.Measure.compProd_assoc', compProd_of_not_isSFiniteKernel_left, setLIntegral_compProd_univ_left, compProd_prodMkLeft_eq_comp, compProd_eq_zero_iff, lintegral_compProd', compProd_fst_condKernelReal, continuous_integral_integral, compProd_apply_univ_le, compProd_sum_left, disintegrate, ProbabilityTheory.compProd_toKernel, setLIntegral_compProd, compProd_preimage_fst, compProd_eq_sum_compProd_left, MeasureTheory.Measure.compProd_assoc, compProd_add_right, compProd_apply_univ, IsZeroOrMarkovKernel.compProd, setLIntegral_compProd_univ_right, compProd_zero_left, compProd_restrict, compProd_assoc, compProd_def, IsCondKernel.disintegrate, compProd_add_left, ProbabilityTheory.hasFiniteIntegral_compProd_iff, compProd_apply_eq_compProd_sectR, compProd_apply, fst_compProd, IsFiniteKernel.compProd, compProd_eq_sum_compProd_right, compProd_sum_right, lintegral_compProd, compProd_apply_prod, IsSFiniteKernel.compProd, compProd_restrict_right, fst_compProd_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ae_ae_of_ae_compProd 📖	—	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure Prod.instMeasurableSpace MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike compProd	—	—	MeasureTheory.Measure.instOuterMeasureClass ae_null_of_compProd_null
ae_compProd_iff 📖	mathematical	MeasurableSet Prod.instMeasurableSpace setOf	Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike compProd	—	MeasureTheory.Measure.instOuterMeasureClass ae_ae_of_ae_compProd ae_compProd_of_ae_ae
ae_compProd_of_ae_ae 📖	mathematical	MeasurableSet Prod.instMeasurableSpace setOf Filter.Eventually MeasureTheory.ae MeasureTheory.Measure MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass DFunLike.coe ProbabilityTheory.Kernel instFunLike	compProd	—	MeasureTheory.Measure.instOuterMeasureClass compProd_null MeasurableSet.compl MeasureTheory.ae.congr_simp compProd_of_not_isSFiniteKernel_right MeasureTheory.ae_zero compProd_of_not_isSFiniteKernel_left
ae_kernel_lt_top 📖	mathematical	—	Filter.Eventually ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel Prod.instMeasurableSpace instFunLike Set.preimage Top.top instTopENNReal MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass Set.preimage_mono MeasureTheory.subset_toMeasurable MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_toMeasurable MeasureTheory.ae_lt_top measurable_kernel_prodMk_left' compProd_apply Filter.mp_mem Filter.univ_mem' LE.le.trans_lt
ae_null_of_compProd_null 📖	mathematical	DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd instZeroENNReal	Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass Set.preimage Pi.instZero	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.exists_measurable_superset_of_null Filter.eventuallyLE_antisymm_iff Filter.EventuallyLE.trans_eq Filter.Eventually.of_forall MeasureTheory.measure_mono Set.preimage_mono compProd_null zero_le ENNReal.instCanonicallyOrderedAdd
comapRight_compProd_id_prod 📖	mathematical	MeasurableEmbedding	comapRight Prod.instMeasurableSpace compProd MeasurableEmbedding.prodMap MeasurableEmbedding.id	—	ext MeasurableEmbedding.prodMap MeasurableEmbedding.id MeasureTheory.Measure.ext comapRight_apply' compProd_apply MeasurableEmbedding.measurableSet_image IsSFiniteKernel.comapRight MeasureTheory.lintegral_congr measurable_prodMk_left Set.ext
compProd_add_left 📖	mathematical	—	compProd ProbabilityTheory.Kernel instAdd Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext compProd_apply IsSFiniteKernel.add MeasureTheory.lintegral_add_measure compProd_of_not_isSFiniteKernel_right add_zero
compProd_add_right 📖	mathematical	—	compProd ProbabilityTheory.Kernel Prod.instMeasurableSpace instAdd	—	ext MeasureTheory.Measure.ext compProd_apply IsSFiniteKernel.add MeasureTheory.lintegral_add_left measurable_kernel_prodMk_left' compProd_of_not_isSFiniteKernel_left add_zero
compProd_apply 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd MeasureTheory.lintegral Set.preimage	—	compProd_def comp_apply copy_apply MeasureTheory.Measure.dirac_bind measurable parallelComp_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId id_apply MeasureTheory.Measure.bind_apply Measurable.aemeasurable MeasureTheory.lintegral_prod ProbabilityTheory.IsSFiniteKernel.sFinite measurable_coe MeasureTheory.lintegral_dirac' MeasurableEquiv.measurable Measurable.lintegral_prod_left Measurable.fun_comp Measurable.prodMk Measurable.snd measurable_id' Measurable.fst isFiniteKernel_of_isFiniteKernel_snd IsZeroOrMarkovKernel.snd instIsMarkovKernelProdCopy MeasureTheory.Measure.dirac_prod_dirac deterministic_apply MeasureTheory.instSFiniteOfSigmaFinite MeasureTheory.Measure.dirac.instSigmaFinite swap_apply' Measurable.indicator measurable_const measurable_prodMk_right Set.indicator_apply MeasureTheory.lintegral_indicator_one measurable_prodMk_left
compProd_apply_prod 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd SProd.sprod Set.instSProd MeasureTheory.lintegral MeasureTheory.Measure.restrict	—	compProd_apply MeasurableSet.prod MeasureTheory.lintegral_indicator Set.mk_preimage_prod_right Set.indicator_of_mem Set.mk_preimage_prod_right_eq_empty MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass Set.indicator_of_notMem
compProd_apply_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd Set.univ	—	compProd_apply MeasurableSet.univ IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.lintegral_const one_mul
compProd_apply_univ_le 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd Set.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring bound	—	compProd_apply MeasurableSet.univ IsFiniteKernel.isSFiniteKernel MeasureTheory.lintegral_mono measure_le_bound MeasureTheory.lintegral_const mul_comm compProd_of_not_isSFiniteKernel_left ENNReal.instCanonicallyOrderedAdd
compProd_assoc 📖	mathematical	—	map Prod.instMeasurableSpace compProd comap DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.prodAssoc MeasurableEquiv.measurable MeasurableEquiv.symm	—	MeasurableEquiv.measurable ext MeasureTheory.Measure.ext compProd_apply IsSFiniteKernel.compProd map_apply' MeasurableSet.preimage lintegral_compProd measurable_kernel_prodMk_left' Measurable.fun_comp Measurable.prodMk measurable_const measurable_id' IsSFiniteKernel.comap Measurable.comp MeasurableEquiv.self_comp_symm comap.congr_simp comap_id compProd_of_not_isSFiniteKernel_right compProd_zero_right map_zero compProd_of_not_isSFiniteKernel_left compProd_zero_left
compProd_congr 📖	mathematical	Filter.Eventually MeasureTheory.Measure DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace instFunLike MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	compProd	—	MeasureTheory.Measure.instOuterMeasureClass ext MeasureTheory.Measure.ext compProd_apply MeasureTheory.lintegral_congr_ae Filter.mp_mem Filter.univ_mem' compProd_of_not_isSFiniteKernel_left
compProd_def 📖	mathematical	—	compProd comp Prod.instMeasurableSpace swap parallelComp id deterministic DFunLike.coe MeasurableEquiv EquivLike.toFunLike MeasurableEquiv.instEquivLike MeasurableEquiv.symm MeasurableEquiv.prodAssoc copy	—	—
compProd_deterministic_apply 📖	mathematical	Measurable Prod.instMeasurableSpace MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd deterministic setOf Set.instMembership	—	compProd_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel isMarkovKernel_deterministic MeasureTheory.Measure.dirac_apply Set.indicator_apply Measurable.prodMk measurable_id Measurable.comp measurable_prodMk_left MeasureTheory.lintegral_add_compl MeasureTheory.setLIntegral_congr_fun MeasurableSet.compl MeasureTheory.lintegral_zero MeasureTheory.setLIntegral_one add_zero
compProd_eq_sum_compProd 📖	mathematical	—	compProd sum Prod.instMeasurableSpace instCountableNat seq	—	instCountableNat sum.congr_simp
compProd_eq_sum_compProd_left 📖	mathematical	—	compProd sum Prod.instMeasurableSpace instCountableNat seq	—	instCountableNat compProd_def sum.congr_simp comp_sum_left comp_sum_right parallelComp_sum_right IsFiniteKernel.isSFiniteKernel isFiniteKernel_seq kernel_sum_seq
compProd_eq_sum_compProd_right 📖	mathematical	—	compProd sum Prod.instMeasurableSpace instCountableNat seq	—	instCountableNat compProd_def sum.congr_simp comp_sum_left comp_sum_right parallelComp_sum_left IsFiniteKernel.isSFiniteKernel isFiniteKernel_seq kernel_sum_seq
compProd_eq_tsum_compProd 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd tsum ENNReal.instAddCommMonoid ENNReal.instTopologicalSpace seq SummationFilter.unconditional	—	instCountableNat compProd_eq_sum_compProd sum_apply'
compProd_eq_zero_iff 📖	mathematical	—	compProd ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero Filter.Eventually MeasureTheory.Measure DFunLike.coe instFunLike MeasureTheory.Measure.instZero MeasureTheory.ae MeasureTheory.Measure.instFunLike MeasureTheory.Measure.instOuterMeasureClass	—	MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.lintegral_eq_zero_iff Measurable.comp measurable_coe MeasurableSet.univ measurable_prodMk_left MeasureTheory.setLIntegral_univ compProd_apply_prod Set.univ_prod_univ compProd_zero_right compProd_congr IsFiniteKernel.isSFiniteKernel ProbabilityTheory.isFiniteKernel_zero
compProd_null 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd instZeroENNReal Filter.EventuallyEq MeasureTheory.ae MeasureTheory.Measure.instOuterMeasureClass Set.preimage Pi.instZero	—	MeasureTheory.Measure.instOuterMeasureClass compProd_apply MeasureTheory.lintegral_eq_zero_iff measurable_kernel_prodMk_left'
compProd_of_not_isSFiniteKernel_left 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	compProd ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	compProd_def parallelComp_of_not_isSFiniteKernel_right comp_zero zero_comp
compProd_of_not_isSFiniteKernel_right 📖	mathematical	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace	compProd ProbabilityTheory.Kernel instZero	—	compProd_def parallelComp_of_not_isSFiniteKernel_left comp_zero zero_comp
compProd_preimage_fst 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike compProd Set.preimage	—	compProd_apply measurable_fst IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' Set.indicator_of_mem MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass Set.indicator_of_notMem MeasureTheory.lintegral_indicator_const one_mul
compProd_restrict 📖	mathematical	MeasurableSet	compProd restrict Prod.instMeasurableSpace SProd.sprod Set Set.instSProd MeasurableSet.prod	—	ext MeasurableSet.prod MeasureTheory.Measure.ext compProd_apply IsSFiniteKernel.restrict restrict_apply' MeasurableSet.inter MeasureTheory.Measure.restrict_apply' Set.indicator_apply MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.lintegral_indicator
compProd_restrict_left 📖	mathematical	MeasurableSet	compProd restrict Prod.instMeasurableSpace SProd.sprod Set Set.instSProd Set.univ MeasurableSet.prod MeasurableSet.univ	—	MeasurableSet.prod MeasurableSet.univ compProd_restrict restrict_univ
compProd_restrict_right 📖	mathematical	MeasurableSet	compProd restrict Prod.instMeasurableSpace SProd.sprod Set Set.instSProd Set.univ MeasurableSet.prod MeasurableSet.univ	—	MeasurableSet.prod MeasurableSet.univ compProd_restrict restrict_univ
compProd_sum_left 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	compProd sum Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext compProd_apply isSFiniteKernel_sum MeasureTheory.lintegral_sum_measure MeasureTheory.Measure.sum_apply compProd_of_not_isSFiniteKernel_right sum.congr_simp sum_zero
compProd_sum_right 📖	mathematical	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace	compProd sum	—	ext MeasureTheory.Measure.ext compProd_apply isSFiniteKernel_sum MeasureTheory.Measure.sum_apply MeasureTheory.lintegral_tsum Measurable.aemeasurable measurable_kernel_prodMk_left' measurable_prodMk_left compProd_of_not_isSFiniteKernel_left sum.congr_simp sum_zero
compProd_zero_left 📖	mathematical	—	compProd ProbabilityTheory.Kernel instZero Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext compProd_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.isFiniteKernel_zero MeasureTheory.lintegral_zero_measure compProd_of_not_isSFiniteKernel_right
compProd_zero_right 📖	mathematical	—	compProd ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	ext MeasureTheory.Measure.ext compProd_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.isFiniteKernel_zero MeasureTheory.lintegral_const MulZeroClass.zero_mul compProd_of_not_isSFiniteKernel_left
fst_compProd 📖	mathematical	—	fst compProd	—	ext MeasureTheory.Measure.ext fst_compProd_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.lintegral_indicator MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter one_mul
fst_compProd_apply 📖	mathematical	MeasurableSet	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike fst compProd MeasureTheory.lintegral Set.indicator instZeroENNReal Prod.instMeasurableSpace Set.univ	—	fst_apply' compProd_apply measurable_fst Set.indicator_of_mem MeasureTheory.measure_empty MeasureTheory.Measure.instOuterMeasureClass Set.indicator_of_notMem
le_compProd_apply 📖	mathematical	—	ENNReal Preorder.toLE PartialOrder.toPreorder ENNReal.instPartialOrder MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike Set MeasureTheory.Measure.instFunLike Prod.instMeasurableSpace setOf Set.instMembership compProd	—	MeasureTheory.lintegral_mono MeasureTheory.measure_mono MeasureTheory.Measure.instOuterMeasureClass MeasureTheory.subset_toMeasurable compProd_apply MeasureTheory.measurableSet_toMeasurable MeasureTheory.measure_toMeasurable
lintegral_compProd 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike compProd	—	lintegral_compProd'
lintegral_compProd' 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike compProd	—	MeasureTheory.SimpleFunc.iSup_eapprox_apply MeasureTheory.SimpleFunc.monotone_eapprox MeasureTheory.lintegral_iSup MeasureTheory.SimpleFunc.measurable Measurable.comp measurable_prodMk_left Measurable.lintegral_kernel_prod_right'' MeasureTheory.lintegral_mono MeasureTheory.SimpleFunc.induction Set.piecewise_eq_indicator MeasureTheory.lintegral_indicator_const compProd_apply MeasureTheory.lintegral_const_mul measurable_kernel_prodMk_left Measurable.prodMk Measurable.snd measurable_fst measurable_snd MeasureTheory.lintegral_indicator_const_comp MeasureTheory.lintegral_add_left
lintegral_compProd₀ 📖	mathematical	AEMeasurable ENNReal ENNReal.measurableSpace Prod.instMeasurableSpace DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike compProd	MeasureTheory.lintegral	—	MeasureTheory.lintegral_congr_ae Filter.mp_mem MeasureTheory.Measure.instOuterMeasureClass ae_ae_of_ae_compProd Filter.univ_mem' lintegral_compProd
setLIntegral_compProd 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike compProd SProd.sprod Set Set.instSProd	—	MeasurableSet.prod compProd_restrict lintegral_compProd IsSFiniteKernel.restrict
setLIntegral_compProd_univ_left 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike compProd SProd.sprod Set Set.instSProd Set.univ	—	setLIntegral_compProd MeasurableSet.univ MeasureTheory.Measure.restrict_univ
setLIntegral_compProd_univ_right 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace MeasurableSet	MeasureTheory.lintegral MeasureTheory.Measure.restrict DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike compProd SProd.sprod Set Set.instSProd Set.univ	—	setLIntegral_compProd MeasurableSet.univ MeasureTheory.Measure.restrict_univ

ProbabilityTheory.Kernel.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.compProd	—	ProbabilityTheory.Kernel.compProd_def comp ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap ProbabilityTheory.Kernel.instIsFiniteKernelProdParallelComp ProbabilityTheory.Kernel.instIsMarkovKernelId ProbabilityTheory.Kernel.isMarkovKernel_deterministic ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy

ProbabilityTheory.Kernel.IsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.compProd	—	ProbabilityTheory.Kernel.compProd_apply ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' MeasureTheory.lintegral_const mul_one

ProbabilityTheory.Kernel.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.compProd	—	ProbabilityTheory.Kernel.compProd_def comp ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap ProbabilityTheory.Kernel.instIsSFiniteKernelProdParallelComp ProbabilityTheory.Kernel.isMarkovKernel_deterministic ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy

ProbabilityTheory.Kernel.IsZeroOrMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel Prod.instMeasurableSpace ProbabilityTheory.Kernel.compProd	—	ProbabilityTheory.Kernel.compProd_def comp ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdParallelComp ProbabilityTheory.Kernel.instIsMarkovKernelId ProbabilityTheory.Kernel.isMarkovKernel_deterministic ProbabilityTheory.Kernel.instIsMarkovKernelProdSwap

---

← Back to Index