# Finite conditional expectation: computing E[X|G] for a partition-generated σ-algebra, including a zero-mass block [← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-conditional-expectation/) This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented. derivation-mko-conditional-expectation-01 · production-20261019-adopted-96 ## Goal and scope On Ω={0,1,2,3,4} with masses 1/8, 3/8, 1/4, 1/4, 0 and X taking the values 4, 0, 2, 6, 10 in order, let G be generated by the partition {0,1}, {2,3}, {4}. From the two defining conditions of conditional expectation (G-measurable, same integral on every event of G), find all versions of E[X|G]: prove they must equal 1 and 4 on the two positive-mass blocks and may take any value on the zero-mass block {4} (determined only almost surely), and explain why pointwise conditioning, checking only the total expectation, and the unweighted mean are all wrong. Works inside the MKO's scope: the complete finite outcomes, exact rational masses, X values and conditioning partition all belong to one probability space (assumption a1); the main computation uses positive-mass blocks, and versions are unique almost surely, while the zero-mass block retains pointwise freedom without a forced value (assumption a2). It does not treat existence of conditional expectation in general (non-discrete) spaces, filtrations or martingales, and does not change the canonical MKO or its English edition. ## Givens and symbols - prob_axioms - finite_sum_rules - set_operations_def - frac_rules - mul_inverse_nonzero - G1 — Ω={0,1,2,3,4}; P({0})=1/8, P({1})=3/8, P({2})=1/4, P({3})=1/4, P({4})=0 (summing to 1); X(0)=4, X(1)=0, X(2)=2, X(3)=6, X(4)=10; all on the same space (MKO assumption a1). - G2 — The conditioning partition B_1={0,1}, B_2={2,3}, B_3={4}; G=σ(B_1,B_2,B_3). - G3 — Definition: Y is a version of E[X|G] if (i) Y is G-measurable and (ii) E[Y𝟏_A]=E[X𝟏_A] for every A∈G, where E[Z𝟏_A]=Σ_{ω∈A} Z(ω)P({ω}). - \Omega,\ P — the sample space and the probability - B_1,B_2,B_3 — the three blocks {0,1}, {2,3}, {4} of the conditioning partition - \mathcal{G}=\sigma(B_1,B_2,B_3) — the σ-algebra generated by the partition - E[Z\mathbf{1}_A] — the integral of Z over A, Σ_{ω∈A} Z(ω)P({ω}) - Y_c — a version of E[X|G] taking the value c on B_3 ## Rules and sources - 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). - 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. - set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A. - frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0. - mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined. - numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable. - image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse. - subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B). - forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds. - distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu. - 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. - and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q. - iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold. - 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. - mko_condexp_def · cited — On the same finite probability space, E[X|G] must be G-measurable and have the same integral as X on every G-measurable event. When G is generated by a partition, its value is the weighted mean on each positive-mass block. On zero-mass blocks it is determined only almost surely; division by zero is not performed. · mko-conditional-expectation - sigma_partition · prerequisite — The σ-algebra σ(𝒫) generated by a partition 𝒫 of a finite set Ω consists exactly of the unions of blocks (including the empty union ∅); it has 2^{|𝒫|} events. - meas_def · prerequisite — On a finite Ω, a function Y is G-measurable exactly when Y^{-1}(S)∈G for every set S of reals. - L_meas_const · lemma — Y is σ(𝒫)-measurable exactly when Y is constant on each block of 𝒫. - L_block_reduce · lemma — For σ(𝒫), condition (ii) holds for every A∈σ(𝒫) exactly when it holds for every block. ## Main derivation S01 · equivalentBefore \mathcal{G}=\sigma(B_1,B_2,B_3) After \mathcal{G}=\{\varnothing,B_1,B_2,B_3,B_1\cup B_2,B_1\cup B_3,B_2\cup B_3,\Omega\} Conditions: none Rule: sigma_partition · Uses: G2, sigma_partition Leaf basis: sigma_partition + set_operations_def + numeric_evaluation The σ-algebra generated by a partition consists exactly of the unions of blocks. Each of the three blocks is either included or not, giving 2^3=8 events (N9), listed on the right. The event {0} is not in G: it is not a union of blocks. S02 · equivalentBefore Y\ \mathcal{G}\text{-measurable} After Y=c_1\ \text{on}\ B_1,\ Y=c_2\ \text{on}\ B_2,\ Y=c_3\ \text{on}\ B_3 Conditions: none Rule: L_meas_const · Uses: S01, G3 Leaf basis: meas_def + sigma_partition + set_operations_def By Lemma L_meas_const (proved in S02.1 and S02.2), condition (i) says exactly that Y is constant on each block; call the values c_1, c_2, c_3. Measurability is a set-level condition independent of the masses, so Y must be constant on the zero-mass block B_3 as well. S03 · equivalentBefore \forall A\in\mathcal{G}:\ E[Y\mathbf{1}_A]=E[X\mathbf{1}_A] After \forall j:\ E[Y\mathbf{1}_{B_j}]=E[X\mathbf{1}_{B_j}] Conditions: none Rule: L_block_reduce · Uses: S01, G3 Leaf basis: finite_sum_rules + sigma_partition + forall_elim By Lemma L_block_reduce (proved in S03.1 and S03.2), condition (ii) on the 8 events reduces to the condition on the 3 blocks. Note that 3 conditions remain, not 1: checking only A=Ω (the total expectation) is not enough. S04 · equivalentBefore E[Y\mathbf{1}_{B}]=E[X\mathbf{1}_{B}],\ Y=c\ \text{on}\ B,\ P(B)>0 After c=\frac{E[X\mathbf{1}_B]}{P(B)} Conditions: P(B)>0 Rule: mul_inverse_nonzero · Uses: S02, S03, G3 Leaf basis: distributive + finite_sum_rules + mul_inverse_nonzero Y equals c on B, so E[Y𝟏_B]=Σ_{ω∈B} c·P({ω})=c·P(B) (distributivity). The condition becomes c·P(B)=E[X𝟏_B]. If P(B)>0, multiplying both sides by 1/P(B) gives c=E[X𝟏_B]/P(B): the mass-weighted mean over the block. If P(B)=0 no division is possible; see S07. S05 · impliesBefore B_1=\{0,1\} After P(B_1)=\tfrac12,\ E[X\mathbf{1}_{B_1}]=\tfrac12,\ c_1=1 Conditions: P(B_1)>0 Rule: numeric_evaluation · Uses: S04, G1, G2 Leaf basis: numeric_evaluation + frac_rules + prob_axioms P(B_1)=1/8+3/8=1/2 (N1); E[X𝟏_{B_1}]=4·1/8+0·3/8=1/2 (N2); P(B_1)>0, so by S04, c_1=(1/2)/(1/2)=1 (N3). S06 · impliesBefore B_2=\{2,3\} After P(B_2)=\tfrac12,\ E[X\mathbf{1}_{B_2}]=2,\ c_2=4 Conditions: P(B_2)>0 Rule: numeric_evaluation · Uses: S04, G1, G2 Leaf basis: numeric_evaluation + frac_rules + prob_axioms P(B_2)=1/4+1/4=1/2; E[X𝟏_{B_2}]=2·1/4+6·1/4=2 (N4); by S04, c_2=2/(1/2)=4 (N5). S07 · impliesBefore B_3=\{4\},\ P(B_3)=0 After c_3\cdot 0=10\cdot 0\ \text{for every}\ c_3\in\mathbb{R} Conditions: P(B_3)=0 Rule: mul_zero · Uses: S02, S03, G1, G2 Leaf basis: mul_zero + finite_sum_rules On the zero-mass block, E[Y𝟏_{B_3}]=c_3·0=0 and E[X𝟏_{B_3}]=10·0=0, so condition (ii) holds for every real c_3. No division is performed: E[X𝟏_{B_3}]/P(B_3)=0/0 is undefined. c_3 only has to make Y constant on B_3 (S02); its value is unrestricted. S08 · equivalentBefore c_1=1,\ c_2=4,\ c_3\ \text{arbitrary} After E[X|\mathcal{G}]=Y_c,\ Y_c=\begin{cases}1&\text{on }B_1\\4&\text{on }B_2\\c&\text{on }B_3\end{cases},\ c\in\mathbb{R} Conditions: none Rule: mko_condexp_def · Uses: S02, S03, S04, S05, S06, S07 Leaf basis: and_intro_elim + iff_intro + def_unfold By S02 and S03, Y is a version exactly when it is constant on the blocks and all three block conditions hold; by S05 and S06 (through the equivalence of S04), c_1=1 and c_2=4 are the only possibilities; by S07, c_3 is arbitrary. So the versions are exactly the Y_c with c∈ℝ. Any two versions can differ only on B_3, and P(B_3)=0, so they agree almost surely: E[X|G] is determined exactly on the positive-mass blocks and only almost surely on the zero-mass block. S09 · impliesBefore A=B_1\cup B_2,\ A=\Omega After E[Y_c\mathbf{1}_A]=E[X\mathbf{1}_A]=\tfrac52 Conditions: none Rule: finite_sum_rules · Uses: S08, S01, G1 Leaf basis: finite_sum_rules + numeric_evaluation Backward check on two non-block events: for A=B_1∪B_2, E[Y_c𝟏_A]=1·1/2+4·1/2=5/2 and E[X𝟏_A]=4·1/8+0·3/8+2·1/4+6·1/4=5/2; for A=Ω, the contributions c·0=0 and 10·0=0 from B_3 are added and both sides stay 5/2 (N6). This agrees with the reduction of S03, but it is a check on two events only; the proof is S03. S10 · impliesBefore Z=X After Z\ \text{not}\ \mathcal{G}\text{-measurable} Conditions: none Rule: L_meas_const · Uses: S02, G1 Leaf basis: meas_def + sigma_partition Contrast (pointwise conditioning): take X itself as the answer. X(0)=4≠0=X(1), while 0 and 1 lie in the same block B_1, so X is not constant on B_1; by L_meas_const, X is not G-measurable and (i) fails. G knows only which block occurred, not the exact outcome inside it. S11 · impliesBefore W\equiv\tfrac52 After E[W]=E[X]\ \text{but}\ E[W\mathbf{1}_{B_1}]=\tfrac54\neq\tfrac12 Conditions: none Rule: numeric_evaluation · Uses: S03, S05, G1 Leaf basis: numeric_evaluation + forall_elim Contrast (checking only the total expectation): the constant W≡5/2 is G-measurable and E[W]=5/2=E[X], so the condition for A=Ω holds. But E[W𝟏_{B_1}]=(5/2)(1/2)=5/4 while E[X𝟏_{B_1}]=1/2 (N7), so (ii) fails on B_1 and W is not E[X|G]. S12 · impliesBefore c_1'=\tfrac{4+0}{2}=2 After E[c_1'\mathbf{1}_{B_1}]=1\neq\tfrac12 Conditions: none Rule: numeric_evaluation · Uses: S04, S05, G1 Leaf basis: numeric_evaluation + frac_rules Contrast (unweighted mean): on B_1 take the plain average of the X values, (4+0)/2=2. Then 2·P(B_1)=1≠1/2=E[X𝟏_{B_1}] (N8), so the condition fails. Because outcome 1 has mass 3/8, larger than the mass 1/8 of outcome 0, the correct weighted mean 1 lies closer to X(1)=0 than 2 does. S13 · impliesBefore \text{S08, S10 to S12} After E[X|\mathcal{G}]=1\ \text{on}\ B_1,\ 4\ \text{on}\ B_2,\ \text{arbitrary on the null block}\ B_3 Conditions: none Rule: mko_condexp_def · Uses: S08, S10, S11, S12 Leaf basis: and_intro_elim The versions of E[X|G] are exactly the Y_c: 1 on {0,1}, 4 on {2,3} and an arbitrary constant c on the zero-mass {4}; all versions agree almost surely. The pointwise X, the constant overall mean and the unweighted mean are not conditional expectations. ## Substeps and lemmas S02.1 · impliesBefore Y=c_j\ \text{on}\ B_j\ (j=1,2,3) After Y^{-1}(S)=\bigcup_{j:\,c_j\in S}B_j\in\mathcal{G} Conditions: none Rule: meas_def · Uses: meas_def, sigma_partition Leaf basis: image_preimage_def + sigma_partition + set_operations_def (⇐) If Y equals c_j throughout B_j, then for any set S of reals, Y^{-1}(S) is exactly the union of the blocks with c_j∈S, so it lies in G and Y is G-measurable. S02.2 · impliesBefore Y\ \mathcal{G}\text{-measurable},\ \omega\in B_j,\ y=Y(\omega) After Y=y\ \text{on all of}\ B_j Conditions: none Rule: meas_def · Uses: meas_def, sigma_partition Leaf basis: image_preimage_def + sigma_partition + subset_def (⇒) Y^{-1}({y})∈G, so it is a union of blocks; it contains ω, and ω belongs only to the block B_j, so B_j is one of the blocks in that union and B_j⊆Y^{-1}({y}), i.e. Y equals y throughout B_j. S02.1 and S02.2 together prove Lemma L_meas_const. S03.1 · impliesBefore \forall A\in\mathcal{G}:\ E[Y\mathbf{1}_A]=E[X\mathbf{1}_A] After \forall j:\ E[Y\mathbf{1}_{B_j}]=E[X\mathbf{1}_{B_j}] Conditions: none Rule: forall_elim · Uses: S01 Leaf basis: forall_elim (⇒) Each block B_j belongs to G (S01), so instances of the universal condition give the equalities on the blocks. S03.2 · impliesBefore \forall j:\ E[Y\mathbf{1}_{B_j}]=E[X\mathbf{1}_{B_j}] After \forall A\in\mathcal{G}:\ E[Y\mathbf{1}_A]=E[X\mathbf{1}_A] Conditions: none Rule: finite_sum_rules · Uses: S01, finite_sum_rules Leaf basis: finite_sum_rules + set_operations_def + sigma_partition (⇐) Any A∈G is a union of disjoint blocks, so the sum over ω∈A splits by blocks: E[Z𝟏_A]=Σ_{B_j⊆A} E[Z𝟏_{B_j}], for Z=X and for Z=Y; the right sides agree term by term, so the left sides agree. For A=∅ both sides are the empty sum 0. S03.1 and S03.2 together prove Lemma L_block_reduce. ## Reverse audits - S13 · sufficient_goal_reduction · S08, S10, S11, S12 — Goal G: find all versions and refute the three wrong methods. Sufficient condition H: S08 together with S10 to S12; H⇒G by conjunction. H is proved forwards from G1 to G3; G is never used as a premise, and no division is done on the zero-mass block. - S12 · premise_audit · S04, S05, numeric_evaluation — On a block B of positive probability, the weighted and plain means agree for every real-valued X on B if and only if each conditional point weight P({ω})/P(B) equals 1/|B|. Necessity follows by taking the point indicators, and sufficiency by substitution. Unequal weights may still give agreement for particular X; on B₁ here the plain mean is 2 and the weighted mean is 1. - S11 · premise_audit · S03, S05, numeric_evaluation — One failing block suffices to refute; this shows that every block is still needed after the reduction of S03. - S10 · premise_audit · S02, L_meas_const — Two different values inside one block suffice to refute measurability. - S09 · premise_audit · S08, S03, numeric_evaluation — The numbers can be recomputed; this step does not claim to replace the argument of S03 for all 8 events. - S08 · inverse_equivalence · S02, S03, S04, S07 — ⇒: every version must be some Y_c (S02, S04). ⇐: every Y_c satisfies (i) and (ii) (S02, S03, S05 to S07). Both directions have reasons. - S07 · premise_audit · S02, mul_zero, mul_inverse_nonzero — The equivalence of S04 needs P(B)≠0, which fails here, so S04's formula cannot be reused; only u·0=0 is used. - S06 · premise_audit · S04, G1, numeric_evaluation — Backward check 4·(1/2)=2=E[X𝟏_{B_2}]. - S05 · premise_audit · S04, G1, numeric_evaluation — Recomputable; backward check 1·(1/2)=1/2=E[X𝟏_{B_1}]. - S04 · inverse_equivalence · mul_inverse_nonzero, distributive — Multiplying by 1/P(B) and by P(B) undo each other, given P(B)≠0; so on a positive-mass block c is unique. - S03.2 · premise_audit · S01, finite_sum_rules, set_operations_def — It needs the blocks to be disjoint, so that the sum splits without double counting. - S03.1 · premise_audit · S01, forall_elim — It needs only that the blocks lie in G. - S03 · inverse_equivalence · L_block_reduce — Both directions are proved in the sub-steps. - S02.2 · premise_audit · meas_def, sigma_partition — The key is that blocks are disjoint: ω lies in exactly one block, so a union of blocks containing ω must contain all of B_j. - S02.1 · premise_audit · meas_def, sigma_partition — Only one direction is proved here; the other is S02.2. - S02 · inverse_equivalence · L_meas_const — Both directions of the lemma are proved in the sub-steps. - S01 · inverse_equivalence · sigma_partition, set_operations_def — The 8 listed sets are exactly all unions of blocks, and sigma_partition says G consists of exactly these; the two descriptions determine each other. ## Error controls and negative controls Pointwise conditioning and division by zero massOne MKO misconception is pointwise conditioning: the answer X itself takes the values 4 and 0 on B_1 and is not G-measurable (S10). Another is dividing on a zero-mass block: E[X𝟏_{B_3}]/P(B_3)=0/0 is undefined; the correct conclusion is that any constant works and versions are unique only almost surely (S07, S08). Checking the total expectation is not enoughAnother MKO misconception: declaring a full conditional expectation after checking only E[Y]=E[X]. The constant 5/2 matches the total expectation but integrates to 5/4≠1/2 over B_1 (S11). Condition (ii) must hold on every event of G, which after reduction still means every block (S03). Weight by massOn a block of positive probability, the value is E[X𝟏_B]/P(B); it cannot in general be replaced by the plain average. Agreement for every real-valued X on that block holds if and only if all conditional point weights equal 1/|B|. For a particular X the means may coincide even with unequal weights. On B₁ here the plain mean is 2 and the correct value is 1 (S12). No division is made on a zero-probability block, whose versions remain as in S07 and S08. - Every value of X is known, so E[X|G]=X → reject — X is not constant on the block B_1, so it is not G-measurable (S10). - On B_3, E[X|G]=E[X𝟏_{B_3}]/P(B_3)=0/0=0 → reject — 0/0 is undefined; every constant satisfies the condition, and the value is determined only almost surely (S07). - W≡5/2 satisfies E[W]=E[X], so W=E[X|G] → reject — E[W𝟏_{B_1}]=5/4≠1/2 (S11). - On B_1, E[X|G]=(4+0)/2=2 → reject — Masses must be used: 2·(1/2)=1≠1/2; the correct value is 1 (S05, S12). - Conditional expectation is unique pointwise, so its value at outcome 4 must be X(4)=10 → reject — Y_0 (taking 0 on B_3) is also a version; versions are unique only almost surely (S08). ## Result and limitations The versions of E[X|G] are exactly the Y_c: on B_1={0,1} the mass-weighted mean (4·1/8+0·3/8)/(1/2)=1, on B_2={2,3} the value (2·1/4+6·1/4)/(1/2)=4, and on the zero-mass block B_3={4} any constant c, with no 0/0 division; all versions agree almost surely, and the total expectation 5/2 is preserved. The pointwise candidate Y=X is not G-measurable, although its integral equality itself holds. The other two candidates, W≡5/2 based only on the total expectation and the unweighted block mean, violate the integral condition on B_1. - This guide treats only partition-generated σ-algebras; existence of conditional expectation on general probability spaces (for example via Radon–Nikodym) and filtrations and martingales (the MKO's next step) are outside its scope. ## Verification and source binding 10 declared checks for this guide; only the listed expressions are covered. - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: fb6d81a6503a7c7ed987151c144cb532f48bda0ba9ff318c35b0da5747915922 - original source SHA-256: f1f1276883bf28f45ac381b84049dc540bebe522aa5588bd14a827b966580991 - Lean: NOT_RUN · independent AI: NOT_MEASURED [Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-conditional-expectation-01.json)