[Merged by Bors] - feat: integral of a continuous bilinear map applied to independent random variables#38754

EtienneC30 wants to merge 21 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

EtienneC30:indep_smulEtienneC30/mathlib4:indep_smulCopy head branch name to clipboard