Commit 2025-03-29 13:22 a724da03

View on Github →

feat(Probability/Independence/Basic): upstream iIndepFun_iff_pi_map_eq_map from PFR (#23418)

  • Added lemma aemeasurable_pi_lambda for AEMeasurable (f : α → ∀ a : δ, X a) μ for countable δ, parallel to measurable_pi_lambda.
  • Showed that a finite collection of random variables are independent iff their joint law is the product distribution of their respective laws. This lemma is needed in CLT. I am using git blame on PFR to figure out the person (@MantasBaksys) who wrote this and adding to co-authored-by field:

Estimated changes

added theorem aemeasurable_pi_iff
added theorem aemeasurable_pi_lambda