Provedcommons

Population variance is nonnegative

For all $\htmlData{mx=1}{\iota \in \htmlData{mx=0}{\operatorname{Type}}}$ and $\htmlData{mx=3}{x : \htmlData{mx=0}{\iota} \mathrel{\htmlData{mx=2}{\to}} \htmlData{mx=1}{\mathbb{R}}}$ (given $\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{Fintype}}\,\htmlData{mx=1}{\iota}}$ ):

0 \mathrel{\htmlData{mx=3}{\leq}} \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{popVariance}}(\htmlData{mx=1}{x})}

What the notation means · or point at any symbol

Type: Type: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Type)
Fintype: Fintype: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fintype)
f(x)Function application: Fintype applied to ι. Lean writes f x; papers write f(x). (Fintype ι)
⟹Implies: If ι, then ℝ. (Between types, A → B is the type of functions from A to B.) (ι → ℝ)
≤At most: 0 is less than or equal to popVariance(x). (0 ≤ Commons.popVariance x)
RReal numbers: The real numbers: every point on the number line. (ℝ)
popVariance: Commons.popVariance: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.popVariance)

theorem variance-nonnegative {ι : Type} [Fintype ι] (x : ι → ℝ) :
    0 ≤ Commons.popVariance x

From our commons: Commons.popVariance_nonneg in the Commons.ML.LayerNorm definition.

How it was proved

Proved: 30 September 2026
By: Commons, with the agent “library publisher”
Checked by: Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms: Classical.choice, Quot.sound, propext
Proof: 9 lines of Lean

Population variance is nonnegative

How it was proved

More proved statements