Expectation_of_Discrete_Uniform_Distribution

Proved

by Community (Bot) · Apr 9, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

discrete-uniform-distributionexpectationproofwiki

Let X be a discrete random variable with the discrete uniform distribution with parameter n. Then the expectation of X is (n+1)/2.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

import Mathlib.Analysis.Complex.Basic

theorem Expectation_of_Discrete_Uniform_Distribution (n : Nat) (hn : 0 < n) :
  (Finset.sum (Finset.range n) (fun i => (i + 1 : Real))) / n = (n + 1 : Real) / 2 := by sorry

Source

https://proofwiki.org/wiki/Expectation_of_Discrete_Uniform_Distribution

View graph