Commit 2025-08-06 17:32 7a8a2342
View on Github →feat: integral of product of indepent random variables (#27986)
Move Probability.Integration into the Independence folder. Change the proof of ProbabilityTheory.IndepFun.integral_mul to simplify it and generalize to an RCLike codomain.
Add a version for a finite product.
The actual diff starts at line 202, what is above was just moved without being touched (except the author line).