# Variance in finite probability models

This English edition is an AI candidate and does not yet have an OCME Atlas (GPT-6) Twin closure receipt.

This entry defines variance as E[(X−E[X])²], distinct from sample variance with an n−1 denominator. Zero-weight outliers do not affect it.

mko-variance · definition · v0.10.0



## Mathematical statement

Put μ=E[X]. In a valid finite probability model, define V(X)=Var(X)=Σ_s w_s(X(s)−μ)²≥0. Translation leaves variance unchanged and Var(kX)=k²Var(X). Variance is zero exactly when X has one common value at every positive-weight outcome.





## Representative formula (exact TeX)

V(X)





## Assumptions


- The finite nonempty sample space, normalized nonnegative weights, and total real-valued function are explicit.
- Use probability-distribution variance rather than a sample estimator, distinguishing positive-weight support from the whole sample space.





## Symbol scope


- V — variance of a finite probability distribution
- X — real-valued random variable





## Intuition, definition, and misconceptions

Every weighted squared term is nonnegative. Zero-weight outcomes may have different values without affecting the moments. Zero variance means constant almost everywhere; in this finite model, that is constant on the positive-weight support.

For X+c, the mean also increases by c, leaving deviations unchanged. For kX, deviations are multiplied by k and squaring gives k². Keep the cases k=0, negative k, and one-point support explicit.

The exercises compute exact rational moments without floating approximations of E[X²]−E[X]². They do not use an n−1 sample denominator or unconditionally split Var(X+Y) into two variances. Standard deviation and general covariance have separate obligations.

Common errors include requiring equal values even at zero-probability outcomes for zero variance, or confusing sample variance with distribution variance or standard deviation.





## Adopted derivation guide

[Variance in finite probability models: translation, scaling and the zero-variance characterization](https://ocme.evemisslab.com/en/derivations/derivation-mko-variance-01/)The original MKO is retained. The guide has its own append-only revision and verification boundaries, not a new Lean proof.





## Prerequisites


- [Expectation in finite models](https://ocme.evemisslab.com/en/mko/mko-expectation/) — Variance first requires the expectation.
- [Natural-number powers and principal square roots](https://ocme.evemisslab.com/en/mko/mko-power-root/) — Squared deviations and k² use power semantics.





## Verification boundary

Finite central moments can be recomputed exactly; general variance, almost-everywhere equivalence, and integrability have no attached formal Evidence.

not_formalized

This does not mean the content is false; it means no replayable computational or formal evidence is registered yet.





## Next obligation

Bind finite centered moments, constancy on positive support, and the bridge to ProbabilityTheory.variance.





## Same-source structured data

This page and the interactive view use the same object and existing language edition; this adds no proof or human review.

[Canonical MKO JSON](https://ocme.evemisslab.com/data/mko/variance.json) · [Plain Markdown](https://ocme.evemisslab.com/en/mko/mko-variance/index.md)