Theorems · Definition · probability
MeasureTheory.Measure.compProd
{α : Type u_1} →
{β : Type u_2} →
{mα : MeasurableSpace α} →
{mβ : MeasurableSpace β} → MeasureTheory.Measure α → ProbabilityTheory.Kernel α β → MeasureTheory.Measure (α × β)The composition-product of a measure and a kernel.
- Cited by
- 132 results in Mathlib
- Foundations
- Depth 225 from the axioms, rests on 5,400 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ProbabilityTheory.Kernelstatement and proof · cited by 1,281
- ProbabilityTheory.Kernel.compProdproof · cited by 99
- ProbabilityTheory.Kernel.constproof · cited by 93
- ProbabilityTheory.Kernel.prodMkLeftproof · cited by 38
Cited by136
Results whose statement or proof uses this declaration.
- ProbabilityTheory.posteriorproof · cited by 30
- MeasureTheory.Measure.compProd_applystatement · cited by 18
- MeasureTheory.Measure.disintegratestatement · cited by 12
- MeasureTheory.Measure.snd_compProdstatement and proof · cited by 11
- ProbabilityTheory.HasCondDistribproof · cited by 10
- MeasureTheory.Measure.compProd_eq_comp_prodstatement · cited by 10
- MeasureTheory.Measure.compProd_of_not_isSFiniteKernelstatement · cited by 10
- MeasureTheory.Measure.compProd_apply_prodstatement · cited by 8
- MeasureTheory.Measure.compProd_of_not_sfinitestatement · cited by 8
- ProbabilityTheory.compProd_map_condDistribstatement and proof · cited by 6
- MeasureTheory.Measure.lintegral_compProdstatement · cited by 6
- MeasureTheory.Measure.MutuallySingular.compProd_of_leftstatement and proof · cited by 5