Theorems · Definition · probability

Finset.expect

{ι : Type u_1} → {M : Type u_4} → [inst : AddCommMonoid M] → [Module ℚ≥0 M] → Finset ι → (ι → M) → M

Average of a function over a finset. If the finset is empty, this is equal to zero.

Defined in

Mathlib.Algebra.BigOperators.Expect

Cited by

116 results in Mathlib

Foundations

Depth 90 from the axioms, rests on 1,341 definitions · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidModule