Prod

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

Statistics

Metric	Count
Definitions `prod`, `«term_×ₖ_»`	2
Theorems `prod`, `prod`, `prod`, `prod`, `comap_prod`, `comap_prod_swap`, `const_prod_comp`, `deterministic_prod_apply'`, `deterministic_prod_deterministic`, `fst_prod`, `id_prod_apply'`, `id_prod_eq`, `lintegral_deterministic_prod`, `lintegral_id_prod`, `lintegral_prod`, `lintegral_prod_deterministic`, `lintegral_prod_id`, `lintegral_prod_symm`, `map_prod_eq`, `map_prod_map`, `map_prod_swap`, `parallelComp_comp_copy`, `prodAssoc_prod`, `prodAssoc_symm_prod`, `prodComm_prod`, `prod_apply`, `prod_apply'`, `prod_apply_prod`, `prod_const`, `prod_const_comp`, `prod_of_not_isSFiniteKernel_left`, `prod_of_not_isSFiniteKernel_right`, `prod_zero`, `snd_prod`, `swap_prod`, `zero_prod`	36
Total	38

ProbabilityTheory

Definitions

Name	Category	Theorems
`«term_×ₖ_»` 📖	CompOp	—

ProbabilityTheory.Kernel

Definitions

Name	Category	Theorems
`prod` 📖	CompOp	53 math math: `prod_apply'`, `parallelComp_comp_prod`, `partialTraj_succ_of_le`, `fst_prod`, `lintegral_id_prod`, `ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_comp_trim`, `deterministic_prod_apply'`, `swap_prod`, `map_prod_eq`, `prod_apply`, `prod_const_comp`, `ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_map_map`, `prod_prodMkRight_comp_deterministic_prod`, `prod_of_not_isSFiniteKernel_right`, `IsMarkovKernel.prod`, `partialTraj_le_def`, `ProbabilityTheory.condIndepFun_iff_compProd_map_prod_eq_compProd_prod_map_map`, `id_prod_apply'`, `prodAssoc_symm_prod`, `ProbabilityTheory.posterior_prod_id_comp`, `prodAssoc_prod`, `compProd_prodMkLeft_eq_comp`, `prod_of_not_isSFiniteKernel_left`, `snd_prod`, `MeasureTheory.partialTraj_const`, `IsSFiniteKernel.prod`, `comap_prod`, `partialTraj_succ_self`, `parallelComp_comp_copy`, `lintegral_prod`, `MeasureTheory.Measure.compProd_eq_comp_prod`, `lintegral_prod_symm`, `prodComm_prod`, `const_prod_comp`, `deterministic_prod_deterministic`, `lintegral_deterministic_prod`, `IsZeroOrMarkovKernel.prod`, `prod_prodMkLeft_comp_prod_deterministic`, `prod_zero`, `IsFiniteKernel.prod`, `lintegral_prod_deterministic`, `indepFun_iff_compProd_map_prod_eq_compProd_prod_map_map`, `map_prod_map`, `prod_const`, `comap_prod_swap`, `id_prod_eq`, `map_prod_swap`, `partialTraj_eq_prod`, `prod_apply_prod`, `zero_prod`, `lintegral_prod_id`, `traj_eq_prod`, `ProbabilityTheory.condIndepFun_iff_map_prod_eq_prod_condDistrib_prod_condDistrib`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_prod` 📖	mathematical	`Measurable`	`comap` `Prod.instMeasurableSpace` `prod`	—	`ext` `comap_apply` `prod_apply` `IsSFiniteKernel.comap`
`comap_prod_swap` 📖	mathematical	—	`comap` `Prod.instMeasurableSpace` `prod` `prodMkRight` `prodMkLeft` `measurable_swap` `map`	—	`measurable_swap` `ext_fun_iff` `lintegral_comap` `lintegral_map` `lintegral_prod` `IsSFiniteKernel.prodMkRight` `IsSFiniteKernel.prodMkLeft` `Measurable.fun_comp` `MeasureTheory.lintegral_lintegral_swap` `ProbabilityTheory.IsSFiniteKernel.sFinite` `Measurable.comp_aemeasurable'` `AEMeasurable.prodMk` `AEMeasurable.snd` `aemeasurable_id` `AEMeasurable.fst`
`const_prod_comp` 📖	mathematical	—	`comp` `Prod.instMeasurableSpace` `prod` `const`	—	`ext` `MeasureTheory.Measure.ext` `comp_apply'` `prod_apply` `const.instIsSFiniteKernel` `IsSFiniteKernel.comp` `MeasureTheory.Measure.prod_apply_symm` `ProbabilityTheory.IsSFiniteKernel.sFinite` `lintegral_comp` `measurable_measure_prodMk_right`
`deterministic_prod_apply'` 📖	mathematical	`Measurable` `MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `prod` `deterministic` `Set.preimage`	—	`prod_apply'` `IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `isMarkovKernel_deterministic` `lintegral_deterministic'` `measurable_measure_prodMk_left` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`deterministic_prod_deterministic` 📖	mathematical	`Measurable`	`prod` `deterministic` `Prod.instMeasurableSpace` `Measurable.prodMk`	—	`ext` `Measurable.prodMk` `MeasureTheory.Measure.ext` `prod_apply` `IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `isMarkovKernel_deterministic` `MeasureTheory.Measure.dirac_prod_dirac`
`fst_prod` 📖	mathematical	—	`fst` `prod`	—	`prod.eq_1` `fst_comp` `ext` `comp_apply` `copy_apply` `MeasureTheory.Measure.dirac_bind` `measurable` `fst_apply` `parallelComp_apply` `IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `IsScalarTower.right` `MeasureTheory.Measure.map_fst_prod` `ProbabilityTheory.IsSFiniteKernel.sFinite` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `one_smul`
`id_prod_apply'` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `prod` `id` `Set.preimage`	—	`measurable_id` `id.eq_1` `deterministic_prod_apply'`
`id_prod_eq` 📖	mathematical	—	`id` `MeasurableSpace` `Prod.instMeasurableSpace` `prod` `deterministic` `measurable_fst` `measurable_snd`	—	`measurable_fst` `measurable_snd` `Measurable.prodMk` `deterministic_prod_deterministic`
`lintegral_deterministic_prod` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike` `prod` `deterministic`	—	`lintegral_prod` `IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `isMarkovKernel_deterministic` `lintegral_deterministic'` `Measurable.lintegral_prod_right'` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`lintegral_id_prod` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike` `prod` `id`	—	`measurable_id` `id.eq_1` `lintegral_deterministic_prod`
`lintegral_prod` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike` `prod`	—	`lintegral_comp` `copy_apply` `MeasureTheory.lintegral_dirac'` `Measurable.lintegral_kernel` `parallelComp_apply` `MeasureTheory.lintegral_prod` `Measurable.aemeasurable` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`lintegral_prod_deterministic` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike` `prod` `deterministic`	—	`lintegral_prod_symm` `IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `isMarkovKernel_deterministic` `lintegral_deterministic'` `Measurable.lintegral_prod_left'` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`lintegral_prod_id` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike` `prod` `id`	—	`measurable_id` `id.eq_1` `lintegral_prod_deterministic`
`lintegral_prod_symm` 📖	mathematical	`Measurable` `ENNReal` `Prod.instMeasurableSpace` `ENNReal.measurableSpace`	`MeasureTheory.lintegral` `DFunLike.coe` `ProbabilityTheory.Kernel` `MeasureTheory.Measure` `instFunLike` `prod`	—	`prod_apply` `MeasureTheory.lintegral_prod_symm` `ProbabilityTheory.IsSFiniteKernel.sFinite` `Measurable.aemeasurable`
`map_prod_eq` 📖	mathematical	`Measurable`	`prod` `map` `Prod.instMeasurableSpace`	—	`map_prod_map` `measurable_id` `map_id`
`map_prod_map` 📖	mathematical	`Measurable`	`prod` `map` `Prod.instMeasurableSpace`	—	`ext` `map_apply` `Measurable.prodMap` `prod_apply` `MeasureTheory.Measure.map_prod_map` `ProbabilityTheory.IsSFiniteKernel.sFinite` `IsSFiniteKernel.map`
`map_prod_swap` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `prod`	—	`ext_fun_iff` `lintegral_map` `measurable_swap` `lintegral_prod` `Measurable.fun_comp` `MeasureTheory.lintegral_lintegral_swap` `ProbabilityTheory.IsSFiniteKernel.sFinite` `Measurable.comp_aemeasurable'` `AEMeasurable.prodMk` `AEMeasurable.snd` `aemeasurable_id` `AEMeasurable.fst`
`parallelComp_comp_copy` 📖	mathematical	—	`comp` `Prod.instMeasurableSpace` `parallelComp` `copy` `prod`	—	—
`prodAssoc_prod` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `prod` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.prodAssoc`	—	`ext` `map_apply` `MeasurableEquiv.measurable` `prod_apply` `IsSFiniteKernel.prod` `MeasureTheory.Measure.prodAssoc_prod` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`prodAssoc_symm_prod` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `prod` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.symm` `MeasurableEquiv.prodAssoc`	—	`prodAssoc_prod` `map_comp_right` `MeasurableEquiv.measurable` `MeasurableEquiv.symm_comp_self` `map_id`
`prodComm_prod` 📖	mathematical	—	`map` `Prod.instMeasurableSpace` `prod` `DFunLike.coe` `MeasurableEquiv` `EquivLike.toFunLike` `MeasurableEquiv.instEquivLike` `MeasurableEquiv.prodComm`	—	`map_prod_swap`
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `ProbabilityTheory.Kernel` `Prod.instMeasurableSpace` `MeasureTheory.Measure` `instFunLike` `prod` `MeasureTheory.Measure.prod`	—	`MeasureTheory.Measure.ext` `prod_apply'` `MeasureTheory.Measure.prod_apply` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`prod_apply'` 📖	mathematical	`MeasurableSet` `Prod.instMeasurableSpace`	`DFunLike.coe` `MeasureTheory.Measure` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `prod` `MeasureTheory.lintegral` `Set.preimage`	—	`copy_apply` `MeasureTheory.Measure.dirac_bind` `measurable` `parallelComp_apply` `MeasureTheory.Measure.prod_apply` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`prod_apply_prod` 📖	mathematical	—	`DFunLike.coe` `MeasureTheory.Measure` `Prod.instMeasurableSpace` `Set` `ENNReal` `MeasureTheory.Measure.instFunLike` `ProbabilityTheory.Kernel` `instFunLike` `prod` `SProd.sprod` `Set.instSProd` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ENNReal.instCommSemiring`	—	`prod_apply` `MeasureTheory.Measure.prod_prod` `ProbabilityTheory.IsSFiniteKernel.sFinite`
`prod_const` 📖	mathematical	—	`prod` `const` `Prod.instMeasurableSpace` `MeasureTheory.Measure.prod`	—	`ext` `MeasureTheory.Measure.ext` `const_apply` `prod_apply` `const.instIsSFiniteKernel`
`prod_const_comp` 📖	mathematical	—	`comp` `Prod.instMeasurableSpace` `prod` `const`	—	`ext` `MeasureTheory.Measure.ext` `comp_apply'` `prod_apply'` `const.instIsSFiniteKernel` `IsSFiniteKernel.comp` `lintegral_comp` `measurable_measure_prodMk_left`
`prod_of_not_isSFiniteKernel_left` 📖	mathematical	`ProbabilityTheory.IsSFiniteKernel`	`prod` `ProbabilityTheory.Kernel` `Prod.instMeasurableSpace` `instZero`	—	`parallelComp_of_not_isSFiniteKernel_left` `zero_comp`
`prod_of_not_isSFiniteKernel_right` 📖	mathematical	`ProbabilityTheory.IsSFiniteKernel`	`prod` `ProbabilityTheory.Kernel` `Prod.instMeasurableSpace` `instZero`	—	`parallelComp_of_not_isSFiniteKernel_right` `zero_comp`
`prod_zero` 📖	mathematical	—	`prod` `ProbabilityTheory.Kernel` `instZero` `Prod.instMeasurableSpace`	—	`parallelComp_zero_right` `zero_comp`
`snd_prod` 📖	mathematical	—	`snd` `prod`	—	`ext` `MeasureTheory.Measure.ext` `IsScalarTower.right` `prod_apply` `IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `MeasureTheory.Measure.map_snd_prod` `ProbabilityTheory.IsSFiniteKernel.sFinite` `MeasureTheory.IsProbabilityMeasure.measure_univ` `ProbabilityTheory.IsMarkovKernel.is_probability_measure'` `one_smul`
`swap_prod` 📖	mathematical	—	`comp` `Prod.instMeasurableSpace` `swap` `prod`	—	`swap_comp_eq_map` `map_prod_swap`
`zero_prod` 📖	mathematical	—	`prod` `ProbabilityTheory.Kernel` `instZero` `Prod.instMeasurableSpace`	—	`parallelComp_zero_left` `zero_comp`

ProbabilityTheory.Kernel.IsFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	—	`ProbabilityTheory.IsFiniteKernel` `Prod.instMeasurableSpace` `ProbabilityTheory.Kernel.prod`	—	`ProbabilityTheory.Kernel.prod.eq_1` `comp` `ProbabilityTheory.Kernel.instIsFiniteKernelProdParallelComp` `ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy`

ProbabilityTheory.Kernel.IsMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	—	`ProbabilityTheory.IsMarkovKernel` `Prod.instMeasurableSpace` `ProbabilityTheory.Kernel.prod`	—	`ProbabilityTheory.Kernel.prod.eq_1` `comp` `ProbabilityTheory.Kernel.instIsMarkovKernelProdParallelComp` `ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy`

ProbabilityTheory.Kernel.IsSFiniteKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	—	`ProbabilityTheory.IsSFiniteKernel` `Prod.instMeasurableSpace` `ProbabilityTheory.Kernel.prod`	—	`ProbabilityTheory.Kernel.prod.eq_1` `comp` `ProbabilityTheory.Kernel.instIsSFiniteKernelProdParallelComp` `ProbabilityTheory.Kernel.IsFiniteKernel.isSFiniteKernel` `ProbabilityTheory.Kernel.isFiniteKernel_of_isFiniteKernel_snd` `ProbabilityTheory.IsZeroOrMarkovKernel.isFiniteKernel` `ProbabilityTheory.Kernel.IsZeroOrMarkovKernel.snd` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy`

ProbabilityTheory.Kernel.IsZeroOrMarkovKernel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod` 📖	mathematical	—	`ProbabilityTheory.IsZeroOrMarkovKernel` `Prod.instMeasurableSpace` `ProbabilityTheory.Kernel.prod`	—	`ProbabilityTheory.eq_zero_or_isMarkovKernel` `comp` `ProbabilityTheory.IsMarkovKernel.IsZeroOrMarkovKernel` `ProbabilityTheory.Kernel.instIsMarkovKernelProdCopy` `ProbabilityTheory.Kernel.instIsZeroOrMarkovKernelProdParallelComp` `ProbabilityTheory.Kernel.IsMarkovKernel.prod`

---

← Back to Index