Commit 2025-08-07 07:54 8a73d23a

feat: random variables on separate spaces are independent (#27984) More precisely, given a family of random variables X : (i : ι) → Ω i → 𝓧 i, with each Ω i equipped with a probability measure μ i, the random variables fun ω ↦ X i (ω i) : (Π j, Ω j) → 𝓧 i are independent. Include a version for Measure.prod, Measure.pi and Measure.infinitePi.