Variance in finite probability models: translation, scaling and the zero-variance characterization

Goal and scope

In a valid finite probability model, prove Var(X)≥0, Var(X+c)=Var(X), Var(kX)=k²Var(X), and Var(X)=0 ⇔ X takes one common value at every positive-weight outcome. Then with S={1,2,3,4}, w₁=1/2, w₂=1/4, w₃=1/4, w₄=0 and X=(1,3,−1,10), compute μ=1, Var(X)=2, Var(X+5)=2 and Var(−3X)=18, and use Z=(2,2,2,7) to show that a different value at a zero-weight outcome does not prevent zero variance.

Stays inside the MKO: finite nonempty sample space, nonnegative normalized weights, a total real-valued function, the probability-distribution variance rather than a sample estimator, and a clear distinction between the positive-weight support and the whole sample space (a1, a2). All arithmetic is exact and rational. Linearity of expectation is cited from mko-expectation. Var(X+Y), covariance, standard deviation and the formula E[X²]−μ² are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• finite_sum_rules
• square_nonneg
• order_basics
• distributive
• power_laws
• numeric_evaluation

• G1 — General model: S is finite and nonempty, w_s≥0 for all s with Σ_{s∈S} w_s=1; X:S→ℝ is total; μ=E[X]=Σ w_s X(s); c and k are reals.
• G2 — Instance: S={1,2,3,4}, w₁=1/2, w₂=1/4, w₃=1/4, w₄=0.
• G3 — X(1)=1, X(2)=3, X(3)=−1, X(4)=10; Z(1)=Z(2)=Z(3)=2, Z(4)=7.

• \mu=E[X] — the expectation of X
• \mathrm{Var}(X)=\sum_s w_s(X(s)-\mu)^2 — the variance of X
• \mathrm{supp}=\{s\in S\mid w_s>0\} — the positive-weight support
• c,k — translation amount and scaling factor (reals)
• t_s — the s-th term of the variance sum

Rules and sources

• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• square_nonneg · prerequisite — Squares are nonnegative: for every real u, u²≥0, and u²=0 ⇔ u=0.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_zero · prerequisite — Multiplying by zero: u·0=0. Reason: u·0=u·(0+0)=u·0+u·0; subtracting u·0 from both sides gives 0=u·0.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• add_assoc · prerequisite — Associativity of addition: (u+v)+w=u+(v+w).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• add_zero · prerequisite — Additive identity: u+0=u.
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• zero_product · prerequisite — Zero-product property: in ℤ, ℚ, ℝ, ℂ (or any integral domain), uv=0 ⇔ u=0 or v=0.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• contrapositive · prerequisite — Contrapositive: P⇒Q is equivalent to ¬Q⇒¬P. The converse Q⇒P is in general not equivalent to P⇒Q.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_variance_def · cited — 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. · mko-variance
• mko_expectation_lin · cited — For nonempty finite S, normalized nonnegative weights w_s, and a real random variable X, define E[X]=Σ_(s∈S)w_s X(s). On the same probability model, E[aX+b]=aE[X]+b and E[X+Y]=E[X]+E[Y] without assuming independence of X and Y; a constant c has expectation c. · mko-expectation
• support_def · prerequisite — Positive-weight support: supp={s∈S ∣ w_s>0}. Since w_s≥0, s∉supp means exactly w_s=0.
• L_shift · lemma — In the model of G1, for every real c: Var(X+c)=Var(X).
• L_scale · lemma — In the model of G1, for every real k: Var(kX)=k²Var(X).
• L_nonneg_sum_zero · lemma — If finitely many reals t_s are all ≥0 and Σ_s t_s=0, then every t_s=0.
• L_var_zero · lemma — In the model of G1: Var(X)=0 ⇔ X(s)=μ for every s∈supp.
• L_const_support · lemma — In the model of G1: Var(X)=0 ⇔ there is a real c with X(s)=c for every s∈supp.

Main derivation

w=(\tfrac12,\tfrac14,\tfrac14,0)

w_s\ge0,\ \sum_s w_s=1,\ \mathrm{supp}=\{1,2,3\}

\mu=E[X]

\tfrac12\cdot1+\tfrac14\cdot3+\tfrac14\cdot(-1)+0\cdot10=1

X(s)-\mu\ \ (s=1,2,3,4)

0,\ 2,\ -2,\ 9

\mathrm{Var}(X)=\sum_s w_s(X(s)-\mu)^2

\tfrac12\cdot0^2+\tfrac14\cdot2^2+\tfrac14\cdot(-2)^2+0\cdot9^2=2

w_s\ge0,\ (X(s)-\mu)^2\ge0

\mathrm{Var}(X)\ge0

\mathrm{Var}(X+c)

\mathrm{Var}(X)

\mathrm{Var}(kX)

k^2\,\mathrm{Var}(X)

\mathrm{Var}(X+5),\ X+5=(6,8,4,15)

\mathrm{Var}(X+5)=\mathrm{Var}(X)=2

\mathrm{Var}(-3X),\ -3X=(-3,-9,3,-30)

\mathrm{Var}(-3X)=(-3)^2\cdot2=18

t_s\ge0,\ \sum_s t_s=0

t_s=0\ \ \forall s

\mathrm{Var}(X)=0

X(s)=\mu\ \ \forall s\in\mathrm{supp}

\mathrm{Var}(X)=0

\exists c\ \forall s\in\mathrm{supp}:\ X(s)=c

Z=2\ \text{on}\ \mathrm{supp}=\{1,2,3\},\ Z(4)=7

\mathrm{Var}(Z)=0

X(1)=1\neq3=X(2),\ 1,2\in\mathrm{supp}

\mathrm{Var}(X)\neq0

\text{S04 to S14}

\mathrm{Var}\ge0,\ \mathrm{Var}(X+c)=\mathrm{Var}(X),\ \mathrm{Var}(kX)=k^2\mathrm{Var}(X),\ \mathrm{Var}=0\iff\text{const on supp}

Substeps and lemmas

E[X+c]

\mu+c

\sum_s w_s\bigl((X(s)+c)-(\mu+c)\bigr)^2

\sum_s w_s(X(s)-\mu)^2

E[kX]

k\mu

(kX(s)-k\mu)^2

k^2(X(s)-\mu)^2

\sum_s w_s\,k^2(X(s)-\mu)^2

k^2\sum_s w_s(X(s)-\mu)^2=k^2\,\mathrm{Var}(X)

t_r>0\ \text{for some}\ r

\sum_s t_s=t_r+\sum_{s\neq r}t_s\ge t_r>0

\sum_s t_s>0\ \text{and}\ \sum_s t_s=0

\neg\exists r:\ t_r>0,\ \text{so}\ t_s=0

\mathrm{Var}(X)=0,\ s\in\mathrm{supp}

X(s)=\mu

X(s)=\mu\ \ \forall s\in\mathrm{supp}

\mathrm{Var}(X)=\sum_s 0=0

\mathrm{Var}(X)=0

X(s)=\mu\ \ \forall s\in\mathrm{supp}\ \Rightarrow\ c=\mu

X(s)=c\ \ \forall s\in\mathrm{supp}

\mu=\sum_{s\in\mathrm{supp}}w_s c+\sum_{s\notin\mathrm{supp}}0\cdot X(s)=c,\ \text{so}\ \mathrm{Var}(X)=0

Reverse audits

• S15 · sufficient_goal_reduction · S04, S05, S06, S07, S08, S09, S12, S13, and_intro_elim — Goal G is the proofs and computations in the goal; the sufficient condition H is the conjunction of the step results, all proved forwards, and H⇒G uses only conjunction introduction.
• S14 · premise_audit · S12, contrapositive — Two different values inside the support suffice to rule out a common value; the conclusion only says nonzero, and the value comes from S04.
• S13 · premise_audit · S12, S01 — Only the ⇐ direction of S12 and the identification of the support are used; the direct computation is a cross-check.
• S12.2 · premise_audit · L_var_zero, finite_sum_rules, support_def, mul_zero — The key point is that μ is determined by the values on the support alone; values outside (such as Z(4)=7) are multiplied by 0 and vanish.
• S12.1 · premise_audit · L_var_zero, exists_intro — Existential introduction needs only the witness c=μ.
• S12 · inverse_equivalence · L_const_support — Both directions are proved in the sub-steps.
• S11.2 · premise_audit · case_analysis, support_def, mul_zero — The two cases exhaust S (support_def guarantees w_s=0 outside the support).
• S11.1 · premise_audit · S05, L_nonneg_sum_zero, zero_product, square_nonneg — For outcomes with w_s=0, t_s=0 gives no information about X(s), so the conclusion holds only on the support.
• S11 · inverse_equivalence · L_var_zero — The two directions are proved in the sub-steps, so this is an equivalence.
• S10.2 · premise_audit · contradiction, order_basics — Proof by contradiction discharges the temporary assumption of S10.1; trichotomy turns '≥0 and not >0' into '=0'.
• S10.1 · premise_audit · finite_sum_rules, order_basics — Only the nonnegativity of the other terms and order-preservation under addition are used; this is reasoning under a temporary assumption, discharged in S10.2.
• S10 · premise_audit · L_nonneg_sum_zero — It needs every term nonnegative; with negative terms allowed, for example 1+(−1)=0, the conclusion fails.
• S09 · premise_audit · S07, S04 — The conclusion comes from the lemma; the direct computation is only a cross-check.
• S08 · premise_audit · S06, S04 — The conclusion comes from the lemma; the direct computation is only a cross-check.
• S07.3 · inverse_equivalence · finite_sum_rules, def_unfold — Factoring out a constant and folding back the definition are equations and hold both ways.
• S07.2 · inverse_equivalence · distributive, power_laws — Both are identities valid for all reals, so the step holds both ways.
• S07.1 · inverse_equivalence · mko_expectation_lin — Linearity is an equation and can be used either way.
• S07 · inverse_equivalence · L_scale — Both sides are the same number (by the lemma) and can replace each other.
• S06.2 · inverse_equivalence · eq_replace, add_inverse, add_comm — Term-by-term replacement of equals; it holds both ways.
• S06.1 · inverse_equivalence · mko_expectation_lin — Linearity is an equation and can be used either way.
• S06 · inverse_equivalence · L_shift — Both sides are the same number (by the lemma) and can replace each other.
• S05 · premise_audit · square_nonneg, order_basics, finite_sum_rules — It needs nonnegative weights; with a negative weight the conclusion could fail. This is one-way and does not claim Var(X)>0.
• S04 · inverse_equivalence · mko_variance_def, numeric_evaluation — Unfolding the definition and exact arithmetic; both sides have the same value.
• S03 · inverse_equivalence · numeric_evaluation — Integer subtraction, checkable backwards (deviation plus μ returns the value).
• S02 · inverse_equivalence · mko_expectation_lin, numeric_evaluation — Unfolding the definition plus exact arithmetic; both sides have the same value.
• S01 · premise_audit · G2, support_def, numeric_evaluation — Exact arithmetic and reading a definition; independently recomputable.

Error controls and negative controls

Zero variance constrains only positive-weight outcomes

One misconception identified in the MKO is requiring a zero-variance variable to agree at zero-probability outcomes as well. Z is not constant on S (Z(4)=7), but w₄=0 and Var(Z)=0 (S13). The correct characterization of zero variance is constancy on the support (S12).

Distribution variance is not the sample variance

The other misconception is to mix in the sample variance. Treating 1, 3, −1, 10 as four data points with denominator n−1=3 gives 275/12, not this model's Var(X)=2. Variance here is weighted by the probabilities and uses no n−1 denominator; the standard deviation √2 is a different quantity not treated here.

The factor is squared, and a shift is not added to the variance

Var(−3X)=(−3)²·2=18, not −3·2=−6 nor 3·2=6; Var(X+5)=2, not 2+5=7. The reasons are the square in S07.2 and the unchanged deviations in S06.2.

• Z(4)=7≠2, so Var(Z)>0 → reject — w₄=0, so the term of outcome 4 is 0·25=0; Z is constantly 2 on the support and Var(Z)=0.
• Var(−3X)=−3Var(X)=−6 → reject — Variance is nonnegative; the correct value is (−3)²·2=18.
• Var(X+5)=Var(X)+5=7 → reject — The shift also adds 5 to the mean, the deviations are unchanged, and Var(X+5)=2.
• The variance of X is the sample variance 275/12 of 1, 3, −1, 10 → reject — This model's variance is weighted by (1/2,1/4,1/4,0) and equals 2; a sample estimator is a different thing.

Result and limitations

In every valid finite model Var(X)≥0, Var(X+c)=Var(X) and Var(kX)=k²Var(X), and Var(X)=0 exactly when X takes one common value throughout the positive-weight support. Instance: μ=1, Var(X)=2, Var(X+5)=2, Var(−3X)=18; Z=(2,2,2,7) is constantly 2 on the support {1,2,3}, so Var(Z)=0 and Z(4)=7 does not matter.

• Var(X+Y), covariance and standard deviation are outside this guide; the formula E[X²]−μ² is not used either.
• Linearity of expectation is cited from mko-expectation; its proof belongs to that MKO's guide and is not repeated here.

Verification and source binding

15 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: ce0f84e07a301a2959c247b101c66b419e062d8b1325ebf04f27a9c4914677a1
• original source SHA-256: ce0f84e07a301a2959c247b101c66b419e062d8b1325ebf04f27a9c4914677a1
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)