Commit 2025-10-26 07:20 f9cb3f99

View on Github →

feat: independence and uncurrying (#30184) Consider ((Xᵢⱼ)ⱼ)ᵢ a family of families of random variables. Assume that for any i, the random variables (Xᵢⱼ)ⱼ are independent. Assume furthermore that the random variables ((Xᵢⱼ)ⱼ)ᵢ are independent. Then the random variables (Xᵢⱼ) indexed by pairs (i, j) are independent. This PR also drops the IsProbabilityMeasure assumption from MeasureTheory.Measure.infinitePi to avoid weird errors with congr.

Estimated changes

Modified Mathlib/Probability/Independence/InfinitePi.lean

modified theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀'

modified theorem ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀

modified theorem ProbabilityTheory.iIndepFun_infinitePi

added theorem ProbabilityTheory.iIndepFun_uncurry'

added theorem ProbabilityTheory.iIndepFun_uncurry

added theorem ProbabilityTheory.iIndepFun_uncurry_infinitePi'

added theorem ProbabilityTheory.iIndepFun_uncurry_infinitePi

Modified Mathlib/Probability/ProductMeasure.lean

added theorem MeasureTheory.Measure.infinitePi_map_eval