Theorem ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFun

Modification history

2025-08-06 17:32
Mathlib/Probability/Independence/Integration.lean
feat: integral of product of indepent random variables (#27986) …
Modified ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFunView on Github →
2025-02-16 15:58
Mathlib/Probability/Integration.lean
chore(*): fix some Fintype/DecidableEq linter errors (#21943)
Modified ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFunView on Github →
2025-01-09 18:51
Mathlib/Probability/Integration.lean
feat: independence formula(finite product case) (#20437) …
Added ProbabilityTheory.lintegral_prod_eq_prod_lintegral_of_indepFunView on Github →