Theorem MeasureTheory.Measure.ae_comp_iff

Modification history

2025-06-23 11:31
Mathlib/Probability/Kernel/Composition/MeasureComp.lean
feat(Probability): sum of sub-Gaussian random variables is sub-Gaussian (#26164) …
Added MeasureTheory.Measure.ae_comp_iffView on Github →