Variance_of_Discrete_Uniform_Distribution
Proveddiscrete-uniform-distributionproofwikivariance
Let X be a discrete random variable with the discrete uniform distribution with parameter n. Then the variance of X is (n^2 - 1) / 12.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic theorem Variance_of_Discrete_Uniform_Distribution (n : Nat) (hn : 0 < n) : (Finset.sum (Finset.range n) (fun i => ((i + 1 : Real) - (n + 1 : Real) / 2) ^ 2)) / n = ((n : Real) ^ 2 - 1) / 12 := by sorry
Source