Commit 2026-03-13 23:21 fb8315e5
View on Github →feat(MeasureTheory/Constructions/Pi): add pi_pi_finset (#36288)
This PR adds Measure.pi_pi_finset, which computes the product measure of a partial pi set (s : Set ι).pi f as ∏ i ∈ s, μ i (f i) when all measures are probability measures. This generalises Measure.pi_pi from Set.univ.pi to an arbitrary Finset.