Prove2Me

The innovation is orthogonal to past data

Proved
VectorSpaceOpt.innovation_orthogonal

by Shuze Chen · Aug 23, 2026 · Mathlib c5ea003 (Lean v4.30.0)

estimationhilbert-spacekalman-filter

Throughout, we work in the Hilbert space of random variables: zero-mean random variables with finite second moments, under the inner product ⟨a,b⟩=E[ab]\langle a, b\rangle = E[ab]. In this space, orthogonality is uncorrelatedness, and the best linear estimate of a variable given some data is its orthogonal projection onto the subspace the data generates.

Let SS be the subspace generated by past data, let β\beta be a random nn-vector, and let β^\hat\beta be its componentwise orthogonal projection onto SS — the best estimate of β\beta from the past. Let new measurements arrive as

y=Wβ+ε,y = W\beta + \varepsilon,

with WW a known m×nm \times n matrix and each noise component εi\varepsilon_i orthogonal to SS. Then the innovation

y~=y−Wβ^\tilde y = y - W\hat\beta

is orthogonal to SS: every component of y~\tilde y is uncorrelated with every element of the past-data subspace.

The innovation is the part of the new measurement that could not have been anticipated from the old data. Its orthogonality to SS is what makes recursive estimation possible: updating an estimate requires only the innovation, never a recomputation over the whole data history.

Formalization Note. The action of a matrix on a random vector is componentwise, (Wβ)i=∑jWij βj(W\beta)_i = \sum_j W_{ij}\,\beta_j with scalar multiplication in the abstract space. Zero means are implicit in this representation, so no expectation operator appears — only inner products.

Preamble
import Mathlib
open scoped RealInnerProductSpace
Formal statement
namespace VectorSpaceOpt

theorem innovation_orthogonal {H : Type} [NormedAddCommGroup H]
    [InnerProductSpace ℝ H] {n m : ℕ} (S : Submodule ℝ H)
    (β βh : Fin n → H)
    (hproj : ∀ i, ∀ s ∈ S, ⟪β i - βh i, s⟫ = 0)
    (W : Matrix (Fin m) (Fin n) ℝ) (ε : Fin m → H)
    (hεS : ∀ i, ∀ s ∈ S, ⟪ε i, s⟫ = 0)
    (y : Fin m → H) (hy : ∀ i, y i = ∑ j, W i j • β j + ε i) :
    ∀ i, ∀ s ∈ S, ⟪y i - ∑ j, W i j • βh j, s⟫ = 0 := by sorry

end VectorSpaceOpt
Source
David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, §4.6 (updating) and §4.7, pp. 92–93
Read-back

What the Lean code literally says, in plain math · claude-fable-5

Read-back of VectorSpaceOpt.innovation_orthogonal

Let HH be a real inner product space (a real vector space with an inner product ⟨⋅,⋅⟩\langle \cdot,\cdot\rangle and its induced norm; no completeness is assumed), and let nn and mm be natural numbers, either of which may be 00. Let SS be an arbitrary linear subspace of HH (it is not required to be closed, finite-dimensional, or non-trivial). The theorem takes the following data and hypotheses:

  • two families of vectors β1,…,βn∈H\beta_1,\dots,\beta_n \in H and β^1,…,β^n∈H\hat\beta_1,\dots,\hat\beta_n \in H (indexed by i∈{1,…,n}i \in \{1,\dots,n\}), together with the hypothesis that for every index ii and every s∈Ss \in S,
⟨βi−β^i, s⟩=0,\langle \beta_i - \hat\beta_i,\ s\rangle = 0,

i.e. each difference βi−β^i\beta_i - \hat\beta_i is orthogonal to every element of SS;

  • a real m×nm \times n matrix WW with entries WijW_{ij};
  • a family of vectors ε1,…,εm∈H\varepsilon_1,\dots,\varepsilon_m \in H with the hypothesis that for every index i∈{1,…,m}i \in \{1,\dots,m\} and every s∈Ss \in S,
⟨εi, s⟩=0,\langle \varepsilon_i,\ s\rangle = 0,

i.e. each εi\varepsilon_i is orthogonal to every element of SS;

  • a family of vectors y1,…,ym∈Hy_1,\dots,y_m \in H with the hypothesis that for every i∈{1,…,m}i \in \{1,\dots,m\},
yi=∑j=1nWij βj+εi,y_i = \sum_{j=1}^{n} W_{ij}\, \beta_j + \varepsilon_i,

where the sum ranges over all j∈{1,…,n}j \in \{1,\dots,n\} (an empty sum, equal to 00, when n=0n = 0).

Under these hypotheses, the conclusion is: for every index i∈{1,…,m}i \in \{1,\dots,m\} and every element s∈Ss \in S,

⟨ yi−∑j=1nWij β^j,  s⟩=0,\Big\langle\, y_i - \sum_{j=1}^{n} W_{ij}\, \hat\beta_j,\ \ s \Big\rangle = 0,

that is, each residual vector yi−∑jWijβ^jy_i - \sum_j W_{ij}\hat\beta_j is orthogonal to every element of the subspace SS.

Remarks on what the statement silently includes: all orthogonality conditions (hypotheses and conclusion alike) are phrased element-wise, as the vanishing of the inner product against each member of SS, with the vector in question in the first slot of the (real, hence symmetric) inner product. If m=0m = 0 the conclusion is vacuously true, and if n=0n = 0 the sums are zero, so the statement reduces to: yi=εiy_i = \varepsilon_i is orthogonal to SS. The families β\beta, β^\hat\beta and the hypothesis on βi−β^i\beta_i - \hat\beta_i place no constraint relating β^\hat\beta to SS individually — only the differences are constrained. Nothing requires WW, β\beta, β^\hat\beta, ε\varepsilon, or yy to be non-zero or distinct, and SS may be the zero subspace (making every orthogonality hypothesis trivially satisfiable) or all of HH.

Human review

  • Endorsed by Community (Bot) · Aug 23, 2026

  • Endorsed by Shuze Chen · Aug 23, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph