Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems compProd_eq_parallelComp_comp_copy_comp, compProd_map, parallelComp_comp_compProd, prod_comp_left, prod_comp_right, prod_prodMkLeft_comp_prod_deterministic, prod_prodMkRight_comp_deterministic_prod	7
Total	7

MeasureTheory.Measure

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd_eq_parallelComp_comp_copy_comp 📖	mathematical	—	compProd bind Prod.instMeasurableSpace DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.copy ProbabilityTheory.Kernel.parallelComp ProbabilityTheory.Kernel.id	—	compProd_eq_comp_prod ProbabilityTheory.Kernel.parallelComp_comp_copy comp_assoc compProd_of_not_isSFiniteKernel ProbabilityTheory.Kernel.parallelComp_of_not_isSFiniteKernel_right bind_zero_right
compProd_map 📖	mathematical	Measurable	compProd ProbabilityTheory.Kernel.map map Prod.instMeasurableSpace	—	comp_assoc ProbabilityTheory.Kernel.parallelComp_comp_prod ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.instIsMarkovKernelId ProbabilityTheory.Kernel.isMarkovKernel_deterministic compProd_eq_comp_prod ProbabilityTheory.Kernel.IsSFiniteKernel.map ProbabilityTheory.Kernel.id_comp ProbabilityTheory.Kernel.deterministic_comp_eq_map measurable_id ProbabilityTheory.Kernel.id.eq_1 Measurable.prodMap ProbabilityTheory.Kernel.deterministic_parallelComp_deterministic deterministic_comp_eq_map
parallelComp_comp_compProd 📖	mathematical	—	bind Prod.instMeasurableSpace compProd DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike ProbabilityTheory.Kernel.parallelComp ProbabilityTheory.Kernel.id ProbabilityTheory.Kernel.comp	—	compProd_eq_comp_prod ProbabilityTheory.Kernel.IsSFiniteKernel.comp comp_assoc ProbabilityTheory.Kernel.parallelComp_comp_prod ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.instIsMarkovKernelId ProbabilityTheory.Kernel.id_comp compProd_of_not_sfinite bind_zero_left
prod_comp_left 📖	mathematical	—	prod bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike Prod.instMeasurableSpace ProbabilityTheory.Kernel.parallelComp ProbabilityTheory.Kernel.id	—	prod_swap instSFiniteBindCoeKernelOfIsSFiniteKernel measurable_swap ProbabilityTheory.Kernel.swap.eq_1 deterministic_comp_eq_map comp_assoc ProbabilityTheory.Kernel.swap_parallelComp prod_comp_right
prod_comp_right 📖	mathematical	—	prod bind DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure ProbabilityTheory.Kernel.instFunLike Prod.instMeasurableSpace ProbabilityTheory.Kernel.parallelComp ProbabilityTheory.Kernel.id	—	ext prod_apply instSFiniteBindCoeKernelOfIsSFiniteKernel bind_apply ProbabilityTheory.Kernel.aemeasurable measurable_prodMk_left MeasureTheory.lintegral_prod Measurable.aemeasurable ProbabilityTheory.Kernel.measurable_coe ProbabilityTheory.Kernel.parallelComp_apply ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel ProbabilityTheory.Kernel.instIsMarkovKernelId ProbabilityTheory.Kernel.id_apply ProbabilityTheory.IsSFiniteKernel.sFinite MeasureTheory.lintegral_dirac' measurable_measure_prodMk_left

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_prodMkLeft_comp_prod_deterministic 📖	mathematical	Measurable	comp Prod.instMeasurableSpace prod prodMkLeft deterministic	—	ext MeasureTheory.Measure.ext prod_apply' IsSFiniteKernel.comp IsSFiniteKernel.prod IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel isMarkovKernel_deterministic comp_apply' lintegral_prod_deterministic measurable_coe lintegral_comp measurable_measure_prodMk_left ProbabilityTheory.IsSFiniteKernel.sFinite Measurable.lintegral_kernel IsSFiniteKernel.prodMkLeft prodMkLeft_apply comp_deterministic_eq_comap comap_apply
prod_prodMkRight_comp_deterministic_prod 📖	mathematical	Measurable	comp Prod.instMeasurableSpace prod prodMkRight deterministic	—	ext MeasureTheory.Measure.ext prod_apply' IsSFiniteKernel.comp IsSFiniteKernel.prod IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel isMarkovKernel_deterministic comp_apply' lintegral_deterministic_prod measurable_coe lintegral_comp measurable_measure_prodMk_left ProbabilityTheory.IsSFiniteKernel.sFinite Measurable.lintegral_kernel IsSFiniteKernel.prodMkRight prodMkRight_apply comp_deterministic_eq_comap comap_apply

---

← Back to Index