Theorem MeasureTheory.Measure.prodMkLeft_comp_compProd

Modification history

2025-03-11 17:38
Mathlib/Probability/Kernel/Composition/MeasureComp.lean
feat(Probability): (conditionally) sub-Gaussian random variables (#22623) …
Added MeasureTheory.Measure.prodMkLeft_comp_compProdView on Github →