Conditional Expectation Refinement Pythagoras

Abstract

Nested conditioning sigma-algebras split squared prediction risk into later risk and conditional-expectation innovation.

Theorem 1.1 (Refinement splits conditional-expectation risk).

$$\begin{array}{c}\forall X:\mathrm{Type},\\ mu:\mathrm{Measure}\left(X\right),\\ G_q,G_r,Sigma:\mathrm{MeasurableSpace}\left(X\right),\\ T:L2\left(X,mu,\mathbb{R}\right),\\ G_q\subseteq G_r\wedge G_r\subseteq Sigma\\ \Rightarrow ({L2Norm\left(T-condExpL2\left(T,G_q\right),mu\right)}^2={L2Norm\left(T-condExpL2\left(T,G_r\right),mu\right)}^2+{L2Norm\left(condExpL2\left(T,G_r\right)-condExpL2\left(T,G_q\right),mu\right)}^2)\wedge \\ {L2Norm\left(T-condExpL2\left(T,G_r\right),mu\right)}^2\le {L2Norm\left(T-condExpL2\left(T,G_q\right),mu\right)}^2.\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Prediction/ConditionalExpectationRefinementPythagoras.conditional_expectation_refinement_pythagoras (✓ std3). ∎

Source. Repository-derived.

Commentary.

The target is a real square-integrable random variable. The coarse and refined measurable spaces are both sub-sigma-algebras of the ambient space, with the coarse one contained in the refined one. The two displayed estimates are Mathlib’s canonical L2 conditional expectations.

The refined-minus-coarse estimate is measurable for the refined sigma-algebra. It is therefore orthogonal to the residual after refined conditioning. Expanding that orthogonal sum gives the exact squared-norm identity; nonnegativity of the innovation term gives risk monotonicity.

For real L2 functions, squared L2 norm is the integral of the squared error, so the public norm identity is the canonical L2 carrier of the source’s expected-square formula.

References

• Truth anchor: D5/S3/ConceptDynamics/Prediction/ConditionalExpectationRefinementPythagoras.conditional_expectation_refinement_pythagoras
• Dependency: D5/S3/ConceptDynamics/Prediction/ConditionalExpectationOptimality