KernelLemmas

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

Statistics

Metric	Count
Definitions	0
Theorems compProd_prodMkLeft_eq_comp, comp_eq_snd_compProd, deterministic_comp_copy, id_parallelComp_comp_parallelComp_id, parallelComp_comm, parallelComp_comp_parallelComp, parallelComp_comp_prod, parallelComp_id_left_comp_parallelComp, parallelComp_id_right_comp_parallelComp, snd_compProd_prodMkLeft, swap_parallelComp	11
Total	11

ProbabilityTheory.Kernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compProd_prodMkLeft_eq_comp 📖	mathematical	—	compProd prodMkLeft comp Prod.instMeasurableSpace prod id	—	ext MeasureTheory.Measure.ext comp_eq_snd_compProd IsSFiniteKernel.prod compProd_apply IsSFiniteKernel.prodMkLeft snd_apply' measurable_snd prod_apply' IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId id_apply MeasureTheory.lintegral_dirac' measurable_measure_prodMk_left ProbabilityTheory.IsSFiniteKernel.sFinite
comp_eq_snd_compProd 📖	mathematical	—	comp snd compProd prodMkLeft	—	ext MeasureTheory.Measure.ext comp_apply' snd_apply' compProd_apply measurable_snd IsSFiniteKernel.prodMkLeft
deterministic_comp_copy 📖	mathematical	Measurable	comp Prod.instMeasurableSpace parallelComp deterministic copy	—	Measurable.prodMk deterministic_prod_deterministic Measurable.comp deterministic_comp_deterministic
id_parallelComp_comp_parallelComp_id 📖	mathematical	—	comp Prod.instMeasurableSpace parallelComp id	—	parallelComp_id_left_comp_parallelComp IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId comp_id
parallelComp_comm 📖	mathematical	—	comp Prod.instMeasurableSpace parallelComp id	—	parallelComp_id_left_comp_parallelComp IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId parallelComp_id_right_comp_parallelComp comp_id parallelComp_of_not_isSFiniteKernel_left comp_zero zero_comp parallelComp_of_not_isSFiniteKernel_right
parallelComp_comp_parallelComp 📖	mathematical	—	comp Prod.instMeasurableSpace parallelComp	—	parallelComp_id_left_comp_parallelComp parallelComp_id_right_comp_parallelComp comp_assoc IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId comp_id
parallelComp_comp_prod 📖	mathematical	—	comp Prod.instMeasurableSpace parallelComp prod	—	parallelComp_comp_copy comp_assoc parallelComp_comp_parallelComp
parallelComp_id_left_comp_parallelComp 📖	mathematical	—	comp Prod.instMeasurableSpace parallelComp id	—	ext MeasureTheory.Measure.ext comp_apply' parallelComp_apply MeasureTheory.lintegral_prod ProbabilityTheory.IsSFiniteKernel.sFinite Measurable.aemeasurable measurable_coe IsSFiniteKernel.comp MeasureTheory.Measure.prod_apply measurable_prodMk_left parallelComp_apply' IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelId id_apply MeasureTheory.lintegral_dirac' measurable_measure_prodMk_left parallelComp_of_not_isSFiniteKernel_left comp_zero
parallelComp_id_right_comp_parallelComp 📖	mathematical	—	comp Prod.instMeasurableSpace parallelComp id	—	swap_parallelComp comp_assoc parallelComp_id_left_comp_parallelComp swap_swap id_comp
snd_compProd_prodMkLeft 📖	mathematical	—	snd compProd prodMkLeft comp	—	comp_eq_snd_compProd
swap_parallelComp 📖	mathematical	—	comp Prod.instMeasurableSpace swap parallelComp	—	ext MeasureTheory.Measure.ext parallelComp_apply MeasureTheory.Measure.bind_apply aemeasurable swap_apply MeasureTheory.lintegral_dirac' measurable_coe parallelComp_apply' MeasureTheory.lintegral_prod_symm ProbabilityTheory.IsSFiniteKernel.sFinite Measurable.aemeasurable Measurable.comp measurable_swap MeasureTheory.Measure.dirac_apply' MeasureTheory.lintegral_indicator measurable_prodMk_left MeasureTheory.lintegral_const MeasureTheory.Measure.restrict_apply Set.univ_inter one_mul parallelComp_of_not_isSFiniteKernel_right comp_zero parallelComp_of_not_isSFiniteKernel_left zero_comp

---

← Back to Index