Commit 2026-06-14 07:12 e59d9d40

View on Github →

feat(Algebra/BigOperators/Expect): expectation of an indicator (#40388) and replace the generic variable M with K in the Semifield section From MeanFourier

Estimated changes

Modified Mathlib/Algebra/BigOperators/Expect.lean

modified theorem Finset.expect_boole_mul'

modified theorem Finset.expect_boole_mul

modified theorem Finset.expect_div

modified theorem Finset.expect_eq_sum_div_card

added theorem Finset.expect_indicator_one

modified theorem Fintype.expect_eq_sum_div_card