lean_workbook_plus_62336
ProvedIf there are possibilities that occur with probabilities that are all-encompassing (so ) that have values if they occur, then the expected value is defined as .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62336 {n : ℕ} (p e : Fin n → ℝ) (hp : ∑ i, p i = 1) : ∃ k, ∑ i, p i * e i = k := by sorrySource