# Total expectation with a nonempty null block

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-law-of-total-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-law-of-total-expectation-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

Audit the partition and compute E[X] by two routes.

Finite law; no conditional division on a null cell.





## Givens and symbols


- work


- G1 — Omega={a,b,c,d,e} has masses(1/8,3/8,1/4,1/4,0), X=(0,2,4,4,99); B1={a,b}, B2={c,d}, B0={e}, and G is their generated sigma-algebra.


- G — partition-generated sigma-algebra
- Y — conditional-expectation version
- k — null-block version value





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- mko_definition · cited — Let G be the sigma-algebra generated by a complete partition. The tower identity is E(E(X|G))=E(X). Cells are pairwise disjoint and cover the sample space. Positive-mass cells contribute P(B_i)E[X|B_i]. Conditional expectation is determined only almost surely: a null-cell quotient is undefined, but any integrable version there has zero weighted contribution. Do not divide by zero. No independence is required, and this is not Bayes formula. · mko-law-of-total-expectation
- work · prerequisite — On a positive-mass block, a conditional mean is its probability-weighted sum divided by the block mass; on a null block, any finite version value may be chosen; finite sums may be regrouped.





## Main derivation

S01 · impliesBefore

\{B_1,B_2,B_0\}

After

B_i\cap B_j=\varnothing\ (i\ne j),\quad\bigcup_iB_i=\Omega

Conditions: none

Rule: work · Uses: G1, work

Leaf basis: work

The three blocks are nonempty, disjoint and contain all five atoms.



S02 · impliesBefore

P(B_1),P(B_2),P(B_0)

After

(P(B_1),P(B_2),P(B_0))=(1/2,1/2,0)

Conditions: none

Rule: work · Uses: G1, S01, work

Leaf basis: work

Sum block masses and identify the zero denominator first.



S03 · impliesBefore

E[X\mid B_1]=\frac{0/8+2(3/8)}{1/2}

After

E[X\mid B_1]=3/2

Conditions: none

Rule: work · Uses: G1, S02, work

Leaf basis: work

Normalize the first block by its positive mass 1/2.



S04 · impliesBefore

E[X\mid B_2]=\frac{4/4+4/4}{1/2}

After

E[X\mid B_2]=4

Conditions: none

Rule: work · Uses: G1, S03, work

Leaf basis: work

X is constant 4 on the second block, giving conditional mean 4.



S05 · impliesBefore

P(B_0)=0

After

Y=E[X\mid G]=(3/2,3/2,4,4,k),\quad k\in\mathbb R

Conditions: none

Rule: work · Uses: G1, S04, work

Leaf basis: work

Choose any finite version value k on the null block, with no0/0 quotient.



S06 · impliesBefore

E[Y]=\tfrac12\tfrac32+\tfrac12 4+0k

After

E[Y]=11/4

Conditions: none

Rule: work · Uses: G1, S05, work

Leaf basis: work

The complete outer weighting includes the null block's zero contribution.



S07 · impliesBefore

E[X]=0/8+2(3/8)+4/4+4/4+99(0)

After

E[X]=11/4

Conditions: none

Rule: work · Uses: G1, S06, work

Leaf basis: work

The direct five-atom sum agrees with the conditional route.



S08 · impliesBefore

\sum_{i:P(B_i)>0}P(B_i)\frac{\sum_{\omega\in B_i}p_\omega X(\omega)}{P(B_i)}

After

\sum_{\omega\in\Omega}p_\omega X(\omega)=E[X]

Conditions: none

Rule: work · Uses: G1, S07, work

Leaf basis: work

Cancel positive denominators and regroup the finite partition sum to obtain the tower identity.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S07, work — The original weighted sum on null atoms is zero as well.
- S07 · premise_audit · G1, S06, work — The term99 times zero does not force a conditional version value 99.
- S06 · premise_audit · G1, S05, work — Every finite k gives the same outer expectation.
- S05 · premise_audit · G1, S04, work — Versions may differ at e only on a null set.
- S04 · premise_audit · G1, S03, work — The numerator 2 must be divided by 1/2.
- S03 · premise_audit · G1, S02, work — The numerator 3/4 is not the conditional mean.
- S02 · premise_audit · G1, S01, work — B0 is{e}, not the empty set.
- S01 · premise_audit · G1, work — The zero-mass atom e must not disappear from the carrier.





## Error controls and negative controls

Null blockCompute cell masses before deciding whether division is allowed.

Two-route auditCompare the direct sum and outer conditional sum at 11/4.


- E[X|B0]=0/0=0. → reject — The quotient is undefined; one may choose a version, not define it by division.
- The partition blocks must be independent. → reject — Total expectation needs disjointness and exhaustiveness, not independence.
- Omitting b leaves the same partition. → reject — b has positive mass 3/8 and coverage would fail.





## Result and limitations

E(E[X|G])=E[X]=11/4, independently of the null-block version value.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 24bfde5c0b3950c83c7e98fb04fbc75973b2b5a7422e8b9f5843de4153da3a73
- original source SHA-256: 743b092227a8a2ca350616cc5f1b13f4b757db1ac765c638dd10d4dd33fe489d
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-law-of-total-expectation-01.json)