Theorems · Definition · probability
ProbabilityTheory.Kernel.comp
{α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} →
{mα : MeasurableSpace α} →
{mβ : MeasurableSpace β} →
{mγ : MeasurableSpace γ} →
ProbabilityTheory.Kernel β γ → ProbabilityTheory.Kernel α β → ProbabilityTheory.Kernel α γComposition of two kernels.
- Cited by
- 129 results in Mathlib
- Foundations
- Depth 213 from the axioms, rests on 5,172 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- MeasurableSpacestatement and proof · cited by 13,106
- ProbabilityTheory.Kernelstatement and proof · cited by 1,281
- MeasureTheory.Measure.bindproof · cited by 173
Cited by135
Results whose statement or proof uses this declaration.
- ProbabilityTheory.Kernel.prodproof · cited by 65
- ProbabilityTheory.Kernel.partialTrajproof · cited by 44
- ProbabilityTheory.Kernel.compProd_applyproof · cited by 31
- ProbabilityTheory.Kernel.comp_apply'statement · cited by 28
- ProbabilityTheory.avgRiskproof · cited by 25
- MeasureTheory.Measure.comp_assocstatement · cited by 17
- ProbabilityTheory.Kernel.compProd_of_not_isSFiniteKernel_leftproof · cited by 12
- ProbabilityTheory.Kernel.comp_applystatement · cited by 10
- ProbabilityTheory.Kernel.zero_compstatement · cited by 10
- MeasureTheory.Measure.compProd_eq_comp_prodproof · cited by 10
- ProbabilityTheory.Kernel.lintegral_compstatement · cited by 9
- ProbabilityTheory.Kernel.id_compstatement · cited by 9