Commit 2024-09-17 18:34 fe83e801

feat: Expectation of a function over a finset (#15883) Define the expectation of a function f : ι → M over a finset s : Finset ι as ∑ i ∈ s, f i divided by s.card. Naïvely, this requires M to be a semifield but, since s.card⁻¹ is rational, we can get away with assuming M to be a NNRat-module. This generality is important to talk about expectation of functions. From LeanAPAP