Theorems · Definition · probability
ProbabilityTheory.Kernel.prod
{α : Type u_1} →
{β : Type u_2} →
{mα : MeasurableSpace α} →
{mβ : MeasurableSpace β} →
{γ : Type u_4} →
{mγ : MeasurableSpace γ} →
ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α γ → ProbabilityTheory.Kernel α (β × γ)Product of two kernels. This is meaningful only when the kernels are s-finite.
- Cited by
- 65 results in Mathlib
- Foundations
- Depth 221 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- ProbabilityTheory.Kernelstatement and proof · cited by 1,281
- ProbabilityTheory.Kernel.compproof · cited by 129
- ProbabilityTheory.Kernel.parallelCompproof · cited by 49
- ProbabilityTheory.Kernel.copyproof · cited by 29
Cited by66
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.partialTrajproof · cited by 44
- ProbabilityTheory.Kernel.prod_applystatement · cited by 15
- MeasureTheory.Measure.compProd_eq_comp_prodstatement and proof · cited by 10
- ProbabilityTheory.Kernel.partialTraj_succ_selfstatement and proof · cited by 6
- ProbabilityTheory.Kernel.prod_apply'statement · cited by 6
- ProbabilityTheory.Kernel.map_prod_mapstatement and proof · cited by 4
- ProbabilityTheory.Kernel.prod_apply_prodstatement · cited by 4
- MeasureTheory.Measure.compProd_mapproof · cited by 4
- ProbabilityTheory.Kernel.lintegral_prodstatement · cited by 3
- ProbabilityTheory.Kernel.traj_map_updateFinsetproof · cited by 3
- ProbabilityTheory.Kernel.parallelComp_comp_copystatement · cited by 3
- ProbabilityTheory.Kernel.parallelComp_comp_prodstatement and proof · cited by 3