Expectation in finite models: proving linearity, with an instance of dependent variables

Goal and scope

For a nonempty finite sample space S with nonnegative weights w_s summing to 1, prove E[c]=c, E[aX+b]=aE[X]+b and E[X+Y]=E[X]+E[Y] (X, Y on the same S, independence not assumed). Then on S={1,2,3} with w₁=1/2, w₂=1/4, w₃=1/4, X=(2,−2,0), Y=(1,3,−1), compute E[X], E[Y], E[X+Y] and E[−3X+5], show that X and Y are not independent while linearity still holds, and use E[XY]≠E[X]E[Y] to show that linearity does not give a product formula.

Stays inside the MKO's finite known probability model: weights nonnegative and summing exactly to 1, variables total on the same finite S, the general finite-sum properties allow the real coefficients a,b,c and normalized nonnegative weights of G1; the worked example uses integer coefficients and explicit rational weights, all computed exactly (a1, a2). The general properties are proved with finite sums; the instance serves only as verification and counterexample. Sample means, long-run convergence, infinite sample spaces and integrability are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• finite_sum_rules
• distributive
• function_def
• prob_axioms
• numeric_evaluation

• G1 — General model: S is nonempty and finite, w_s≥0 for all s, Σ_{s∈S} w_s=1; X, Y:S→ℝ are total on the same S; a, b, c are reals.
• G2 — Instance: S={1,2,3}, w₁=1/2, w₂=1/4, w₃=1/4.
• G3 — X(1)=2, X(2)=−2, X(3)=0; Y(1)=1, Y(2)=3, Y(3)=−1.

• w_s — the weight of outcome s
• E[Z]=\sum_{s\in S}w_sZ(s) — the expectation of Z
• X,Y — two random variables on the same S
• a,b,c — real constants
• XY — the pointwise product s↦X(s)Y(s)

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.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• prob_axioms · prerequisite — Probability axioms: P(A)≥0; P(Ω)=1; the probability of a (countable) union of pairwise disjoint events is the sum of their probabilities. Hence P(∅)=0 and P(Aᶜ)=1−P(A).
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• mul_one · prerequisite — Multiplicative identity: 1·u=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.
• mul_assoc · prerequisite — Associativity of multiplication: (uv)w=u(vw).
• 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.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_expectation_def · 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
• pointwise_rv · prerequisite — Random variables on the same S are combined pointwise: (aX+b)(s)=aX(s)+b, (X+Y)(s)=X(s)+Y(s), (XY)(s)=X(s)Y(s); the constant c is the function s↦c.
• indep_def · prerequisite — In a finite model, X and Y are independent when P(X=x and Y=y)=P(X=x)P(Y=y) for all reals x, y, each probability being the sum of the weights of the qualifying outcomes.
• L_const · lemma — In the model of G1, for a constant c: E[c]=c.
• L_affine · lemma — In the model of G1: E[aX+b]=aE[X]+b.
• L_sum · lemma — In the model of G1, with X and Y on the same S: E[X+Y]=E[X]+E[Y].

Main derivation

Z:S\to\mathbb{R}

E[Z]=\sum_{s\in S}w_sZ(s)

w_1=\tfrac12,\ w_2=\tfrac14,\ w_3=\tfrac14

w_s\ge0,\ \sum_s w_s=1

E[c]

c

E[aX+b]

aE[X]+b

E[X+Y]

E[X]+E[Y]

E[X]

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

E[Y]

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

E[X+Y],\ X+Y=(3,1,-1)

E[X+Y]=\tfrac32=E[X]+E[Y]

E[-3X+5],\ -3X+5=(-1,11,5)

E[-3X+5]=-3\cdot\tfrac12+5=\tfrac72

P(X=2,\,Y=1)=w_1=\tfrac12,\ P(X=2)P(Y=1)=\tfrac14

X,Y\ \text{not independent}

XY=(2,-6,0)

E[XY]=-\tfrac12\neq\tfrac12=E[X]E[Y]

\tfrac{2+(-2)+0}{3}=0

0\neq\tfrac12=E[X]

\text{S03 to S12}

E[c]=c,\ E[aX+b]=aE[X]+b,\ E[X+Y]=E[X]+E[Y];\ E[XY]\neq E[X]E[Y]\ \text{here}

Substeps and lemmas

\sum_{s\in S}w_s\,c

c\sum_{s\in S}w_s=c\cdot 1=c

\sum_{s}w_s\,(aX(s)+b)

\sum_{s}\bigl(a\,w_sX(s)+b\,w_s\bigr)

\sum_{s}\bigl(a\,w_sX(s)+b\,w_s\bigr)

a\sum_{s}w_sX(s)+b\sum_{s}w_s

a\sum_{s}w_sX(s)+b\sum_{s}w_s

aE[X]+b\cdot1=aE[X]+b

\sum_{s}w_s\,(X(s)+Y(s))

\sum_{s}\bigl(w_sX(s)+w_sY(s)\bigr)

\sum_{s}\bigl(w_sX(s)+w_sY(s)\bigr)

\sum_{s}w_sX(s)+\sum_{s}w_sY(s)=E[X]+E[Y]

Reverse audits

• S13 · sufficient_goal_reduction · S03, S04, S05, S08, S09, S10, S11, 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.
• S12 · premise_audit · S06, numeric_evaluation — This compares the two numbers in this instance. The plain average is guaranteed to equal the expectation for every real-valued X if and only if every weight is 1/|S|; for a particular X, equality can also occur with nonuniform weights (for example, a constant X).
• S11 · premise_audit · mko_expectation_def, pointwise_rv, numeric_evaluation — One counterexample suffices to refute 'the expectation of a product always equals the product of expectations'; the step does not discuss whether the product formula holds under independence.
• S10 · premise_audit · indep_def, numeric_evaluation, quantifier_negation — Independence requires the identity for all x, y; one failing pair (x,y) suffices to refute it.
• S09 · premise_audit · S04, S06 — A negative coefficient a is fine because the lemma holds for all real a, b; the direct computation is only a check.
• S08 · premise_audit · S05, S06, S07 — The conclusion comes from the general lemma; the direct computation is a cross-check, not the source of the proof.
• S07 · inverse_equivalence · mko_expectation_def, numeric_evaluation — Unfolding the definition and exact arithmetic.
• S06 · inverse_equivalence · mko_expectation_def, numeric_evaluation — Unfolding the definition and exact arithmetic; both sides name the same number.
• S05.2 · inverse_equivalence · finite_sum_rules, def_unfold — Splitting the sum and folding back the definition are equations and hold both ways.
• S05.1 · inverse_equivalence · distributive, pointwise_rv, eq_replace — Term-by-term replacement of equals; it holds both ways.
• S05 · inverse_equivalence · L_sum — The lemma is proved by two equational sub-steps, and their chain is an equation.
• S04.3 · inverse_equivalence · def_unfold, G1, mul_one — Folding back the definition and substituting a known value are replacements of equals and hold both ways.
• S04.2 · inverse_equivalence · finite_sum_rules — Both finite-sum rules are equations and can be used in either direction.
• S04.1 · inverse_equivalence · distributive, mul_comm, eq_replace — Term-by-term replacement of equals leaves the sum unchanged, so it holds both ways.
• S04 · inverse_equivalence · L_affine — Each sub-step of the lemma is an equation, and chaining them gives an equation.
• S03.1 · inverse_equivalence · finite_sum_rules, mul_one, G1 — Each equals sign is an identity or the substitution of a known value, so the step holds both ways.
• S03 · inverse_equivalence · L_const — This is an equality of numbers; both sides name the same number and can replace each other.
• S02 · premise_audit · G2, numeric_evaluation — Exact rational arithmetic, independently recomputable.
• S01 · premise_audit · G1, mko_expectation_def, pointwise_rv — This is only a definition; it presupposes valid weights and a finite S so that the sum makes sense.

Error controls and negative controls

Do not average the values when equal likelihood is not given

One misconception identified in the MKO is averaging all values without looking at the weights. The plain average of the values 2, −2, 0 of X is 0, but the weights are 1/2, 1/4, 1/4 and E[X]=1/2 (S12). Expectation is a weighted sum: each outcome's value is multiplied by its own probability.

Linearity neither needs nor implies independence

The other misconception is to infer independence or a product formula from linearity. S10 shows X and Y are not independent, yet E[X+Y]=E[X]+E[Y] holds; S11 shows E[XY]=−1/2≠E[X]E[Y]=1/2. Linearity is only the splitting of a finite sum and has nothing to do with the joint distribution.

The constant term is multiplied by the total weight 1

The b in E[aX+b] comes from bΣw_s=b·1 (S04.3). Dropping b gives −3/2, and multiplying b by the number of outcomes 3 gives −3/2+15=27/2; both are wrong, and the correct value is 7/2.

• E[X]=(2+(−2)+0)/3=0 → reject — The weights are not equal; E[X]=1/2·2+1/4·(−2)+1/4·0=1/2.
• E[X+Y]=E[X]+E[Y] holds here, so X and Y are independent → reject — Linearity holds for any variables on the same model; P(X=2 and Y=1)=1/2≠1/4=P(X=2)P(Y=1), so X and Y are not independent.
• E[XY]=E[X]E[Y]=1/2 → reject — Direct computation gives E[XY]=1/2·2+1/4·(−6)+1/4·0=−1/2.
• E[−3X+5]=−3E[X]=−3/2 → reject — The constant term was dropped: E[−3X+5]=−3/2+5=7/2.

Result and limitations

In every nonempty finite model with nonnegative weights summing to 1, E[c]=c, E[aX+b]=aE[X]+b and E[X+Y]=E[X]+E[Y]; the proof uses only finite-sum rules and pointwise operations on one sample space, with no independence. In the instance E[X]=1/2, E[Y]=1, E[X+Y]=3/2, E[−3X+5]=7/2; X and Y are not independent; E[XY]=−1/2≠1/2=E[X]E[Y]; the plain average 0 of the values of X is not E[X].

• N12 to N14 verify the identities only for this instance's weight vector (1/2,1/4,1/4) (polynomial grid checks); the general proofs are S03 to S05.
• This guide does not treat expectation on infinite sample spaces, integrability, or convergence of sample means.

Verification and source binding

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

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

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