Commit 2025-11-15 16:31 f3938091

View on Github →

feat: compute the PMF of a product measure (#31392) It is the product of the PMFs.

Estimated changes

Modified Mathlib/MeasureTheory/Constructions/Pi.lean

added theorem MeasureTheory.Measure.pi_singleton

Modified Mathlib/Probability/Independence/InfinitePi.lean

Modified Mathlib/Probability/ProductMeasure.lean

added theorem MeasureTheory.Measure.infinitePi_dirac

added theorem MeasureTheory.Measure.infinitePi_singleton