ParallelComp

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

Statistics

Metric	Count
Definitions parallelComp, «term_∥ₖ_»	2
Theorems deterministic_parallelComp_deterministic, instIsFiniteKernelProdParallelComp, instIsMarkovKernelProdParallelComp, instIsSFiniteKernelProdParallelComp, instIsZeroOrMarkovKernelProdParallelComp, lintegral_parallelComp, lintegral_parallelComp_symm, parallelComp_apply, parallelComp_apply', parallelComp_apply_prod, parallelComp_apply_univ, parallelComp_def, parallelComp_of_not_isSFiniteKernel_left, parallelComp_of_not_isSFiniteKernel_right, parallelComp_sum_left, parallelComp_sum_right, parallelComp_zero_left, parallelComp_zero_right	18
Total	20

ProbabilityTheory

Definitions

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

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
parallelComp 📖	CompOp	32 math math: parallelComp_comp_parallelComp, parallelComp_comp_prod, parallelComp_of_not_isSFiniteKernel_left, parallelComp_comm, parallelComp_apply_prod, parallelComp_def, parallelComp_sum_left, instIsSFiniteKernelProdParallelComp, MeasureTheory.Measure.parallelComp_comp_compProd, parallelComp_id_right_comp_parallelComp, parallelComp_comp_copy, parallelComp_apply', deterministic_comp_copy, parallelComp_sum_right, ProbabilityTheory.parallelProd_posterior_comp_copy_comp, deterministic_parallelComp_deterministic, parallelComp_of_not_isSFiniteKernel_right, lintegral_parallelComp_symm, parallelComp_zero_right, MeasureTheory.Measure.prod_comp_left, compProd_def, MeasureTheory.Measure.prod_comp_right, parallelComp_apply, instIsZeroOrMarkovKernelProdParallelComp, parallelComp_apply_univ, swap_parallelComp, lintegral_parallelComp, MeasureTheory.Measure.compProd_eq_parallelComp_comp_copy_comp, instIsFiniteKernelProdParallelComp, instIsMarkovKernelProdParallelComp, parallelComp_id_left_comp_parallelComp, parallelComp_zero_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deterministic_parallelComp_deterministic 📖	mathematical	Measurable	parallelComp deterministic Prod.instMeasurableSpace Measurable.prodMap	—	ext Measurable.prodMap parallelComp_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel isMarkovKernel_deterministic MeasureTheory.Measure.dirac_prod_dirac
instIsFiniteKernelProdParallelComp 📖	mathematical	—	ProbabilityTheory.IsFiniteKernel Prod.instMeasurableSpace parallelComp	—	ENNReal.mul_lt_top bound_lt_top parallelComp_apply_univ IsFiniteKernel.isSFiniteKernel mul_le_mul' IsOrderedMonoid.toMulLeftMono ENNReal.instIsOrderedMonoid covariant_swap_mul_of_covariant_mul measure_le_bound
instIsMarkovKernelProdParallelComp 📖	mathematical	—	ProbabilityTheory.IsMarkovKernel Prod.instMeasurableSpace parallelComp	—	parallelComp_apply_univ IsFiniteKernel.isSFiniteKernel ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel MeasureTheory.IsProbabilityMeasure.measure_univ ProbabilityTheory.IsMarkovKernel.is_probability_measure' mul_one
instIsSFiniteKernelProdParallelComp 📖	mathematical	—	ProbabilityTheory.IsSFiniteKernel Prod.instMeasurableSpace parallelComp	—	instCountableNat kernel_sum_seq parallelComp_sum_left IsFiniteKernel.isSFiniteKernel isFiniteKernel_seq sum.congr_simp parallelComp_sum_right isSFiniteKernel_sum instIsFiniteKernelProdParallelComp parallelComp_of_not_isSFiniteKernel_right ProbabilityTheory.isFiniteKernel_zero parallelComp_of_not_isSFiniteKernel_left
instIsZeroOrMarkovKernelProdParallelComp 📖	mathematical	—	ProbabilityTheory.IsZeroOrMarkovKernel Prod.instMeasurableSpace parallelComp	—	ProbabilityTheory.eq_zero_or_isMarkovKernel parallelComp_zero_right ProbabilityTheory.instIsZeroOrMarkovKernelOfNatKernel parallelComp_zero_left ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel instIsMarkovKernelProdParallelComp
lintegral_parallelComp 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike parallelComp	—	parallelComp_apply MeasureTheory.lintegral_prod ProbabilityTheory.IsSFiniteKernel.sFinite Measurable.aemeasurable
lintegral_parallelComp_symm 📖	mathematical	Measurable ENNReal Prod.instMeasurableSpace ENNReal.measurableSpace	MeasureTheory.lintegral DFunLike.coe ProbabilityTheory.Kernel MeasureTheory.Measure instFunLike parallelComp	—	parallelComp_apply MeasureTheory.lintegral_prod_symm ProbabilityTheory.IsSFiniteKernel.sFinite Measurable.aemeasurable
parallelComp_apply 📖	mathematical	—	DFunLike.coe ProbabilityTheory.Kernel Prod.instMeasurableSpace MeasureTheory.Measure instFunLike parallelComp MeasureTheory.Measure.prod	—	parallelComp_def
parallelComp_apply' 📖	mathematical	MeasurableSet Prod.instMeasurableSpace	DFunLike.coe MeasureTheory.Measure Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike parallelComp MeasureTheory.lintegral Set.preimage	—	parallelComp_apply MeasureTheory.Measure.prod_apply ProbabilityTheory.IsSFiniteKernel.sFinite
parallelComp_apply_prod 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike parallelComp SProd.sprod Set.instSProd Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	parallelComp_apply MeasureTheory.Measure.prod_prod ProbabilityTheory.IsSFiniteKernel.sFinite
parallelComp_apply_univ 📖	mathematical	—	DFunLike.coe MeasureTheory.Measure Prod.instMeasurableSpace Set ENNReal MeasureTheory.Measure.instFunLike ProbabilityTheory.Kernel instFunLike parallelComp Set.univ Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring ENNReal.instCommSemiring	—	parallelComp_apply MeasureTheory.Measure.prod_apply ProbabilityTheory.IsSFiniteKernel.sFinite MeasurableSet.univ mul_comm MeasureTheory.lintegral_const
parallelComp_def 📖	mathematical	—	parallelComp ProbabilityTheory.Kernel Prod.instMeasurableSpace ProbabilityTheory.IsSFiniteKernel MeasureTheory.Measure.prod DFunLike.coe MeasureTheory.Measure instFunLike instZero	—	—
parallelComp_of_not_isSFiniteKernel_left 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	parallelComp ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	parallelComp_def
parallelComp_of_not_isSFiniteKernel_right 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	parallelComp ProbabilityTheory.Kernel Prod.instMeasurableSpace instZero	—	parallelComp_def
parallelComp_sum_left 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	parallelComp sum Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext parallelComp_apply isSFiniteKernel_sum MeasureTheory.Measure.prod_sum_left ProbabilityTheory.IsSFiniteKernel.sFinite parallelComp_of_not_isSFiniteKernel_right sum.congr_simp sum_zero
parallelComp_sum_right 📖	mathematical	ProbabilityTheory.IsSFiniteKernel	parallelComp sum Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext parallelComp_apply isSFiniteKernel_sum MeasureTheory.Measure.prod_sum_right ProbabilityTheory.IsSFiniteKernel.sFinite parallelComp_of_not_isSFiniteKernel_left sum.congr_simp sum_zero
parallelComp_zero_left 📖	mathematical	—	parallelComp ProbabilityTheory.Kernel instZero Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext parallelComp_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.isFiniteKernel_zero MeasureTheory.Measure.zero_prod parallelComp_of_not_isSFiniteKernel_right
parallelComp_zero_right 📖	mathematical	—	parallelComp ProbabilityTheory.Kernel instZero Prod.instMeasurableSpace	—	ext MeasureTheory.Measure.ext parallelComp_apply IsFiniteKernel.isSFiniteKernel ProbabilityTheory.isFiniteKernel_zero MeasureTheory.Measure.prod_zero parallelComp_of_not_isSFiniteKernel_left

---

← Back to Index