LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Conditional variance is well-defined and has the second-moment formula

Statement

Assume AC. For real $X \in L^{2} (P)$ , conditional variance is an integrable nonnegative class independent of representatives and satisfies $Var (X ∣ G) = E [X^{2} ∣ G] - (E [X ∣ G])^{2}$ almost surely.

Facts & Assumptions

Given: AC, real $X \in L^{2} (P)$ , a sub-sigma-algebra G and the proposed conditional-variance definition.

[F1]

Conditional variance is the conditional expectation of the squared residual. (Conditional variance)

[F2]

The conditional mean of X is square integrable. (Conditional lp contraction)

[F3]

Products of $L^{2}$ functions are integrable. (Cauchy-Schwarz inequality for $L^{2}$ )

[F4]

The known factor can be taken outside after product integrability is checked. (Taking out what is known)

[F5]

Conditional expectation is positive and linear. (Basic algebra and order properties of conditional expectation)

[F6]

Almost-everywhere equal integrable functions have identical event integrals. (Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree)

[F7]

Conditional expectation fixes an integrable known variable. (Conditioning a known variable and an independent variable)

Proof

technique · direct

1.1

Write $U = E [X ∣ G]$ . It is in $L^{2}$ by [F2]. Since $(X - U)^{2} \leq 2 X^{2} + 2 U^{2}$ , the squared residual is integrable; it is nonnegative and measurable. Thus [F1] exists as an integrable nonnegative class by [F5]. If X or U is replaced by an almost-surely equal measurable representative, the square changes only on the union of those two measurable null sets. Its event integrals are unchanged by [F6], so its conditional class is unchanged.

F1F2F5F6

2.1

The product XU is integrable by [F3]; U is finite and G-measurable. Hence [F4] yields $E [X U ∣ G] = U E [X ∣ G] = U^{2}$ . Also U squared is integrable and G-measurable, so [F7] gives $E [U^{2} ∣ G] = U^{2}$ . Expanding the residual square and using [F5] gives $E [(X - U)^{2} ∣ G] = E [X^{2} ∣ G] - 2 U^{2} + U^{2} = E [X^{2} ∣ G] - U^{2}$ . All three conditional inputs are integrable, so the subtraction involves finite classes only.

step 1.1F3F4F5F7∎

Source notes

Durrett Theorems 4.1.9, 4.1.11, 4.1.14–4.1.15, printed pp.210–213. The local square expansion supplies the formula and checks every product before taking-out.

Depends on

Used by

Conditional variance decomposition Corollary

Cited to discharge well-definedness by Conditional variance.

Dependency tree · two levels

26 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Durrett, Probability: Theory and Examples, 5th ed. (standard reference, not scraped)