The single-step updating formula

Proved

VectorSpaceOpt.estimate_update

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

estimationhilbert-spacekalman-filter

Work in the Hilbert space of zero-mean random variables, $\langle a, b\rangle = E[ab]$ .

Suppose an optimal estimate $\hat\beta$ of a random $n$ -vector $\beta$ has been formed from past data generating a subspace $S$ , with error covariance

R_{ij} = \big\langle \beta_i - \hat\beta_i,\ \beta_j - \hat\beta_j \big\rangle .

Now additional measurements arrive,

y = W\beta + \varepsilon,

where the noise $\varepsilon$ has covariance $Q_{ij} = \langle \varepsilon_i, \varepsilon_j\rangle$ , is orthogonal to $S$ , and is uncorrelated with $\beta$ ; assume $W R W^\top + Q$ is invertible. Then the updated optimal estimate is

\tilde\beta \;=\; \hat\beta \;+\; R W^\top \big(W R W^\top + Q\big)^{-1}\,\big(y - W\hat\beta\big),

and the updated error covariance is

R - R W^\top \big(W R W^\top + Q\big)^{-1} W R .

Precisely: $\tilde\beta$ is the orthogonal projection of $\beta$ onto the enlarged subspace generated by $S$ together with the components of $y$ .

The structure of the formula is the point. The old estimate is not recomputed; it is corrected by a gain matrix applied to the innovation $y - W\hat\beta$ , the part of the new data orthogonal to the old. This is the single step from which the Kalman recursion is built.

Formalization Note. The gain and the updated estimate are named by defining hypotheses rather than constructed. Being the projection onto the enlarged subspace is expressed as membership in it plus orthogonality of the error to it, which characterizes the projection uniquely.

Preamble

import Mathlib
open Matrix
open scoped RealInnerProductSpace

Formal statement

namespace VectorSpaceOpt

theorem estimate_update {H : Type} [NormedAddCommGroup H]
    [InnerProductSpace ℝ H] {n m : ℕ} (S : Submodule ℝ H)
    (β βh : Fin n → H) (hβh : ∀ i, βh i ∈ S)
    (hproj : ∀ i, ∀ s ∈ S, ⟪β i - βh i, s⟫ = 0)
    (R : Matrix (Fin n) (Fin n) ℝ) (hR : ∀ i j, ⟪β i - βh i, β j - βh j⟫ = R i j)
    (W : Matrix (Fin m) (Fin n) ℝ) (ε : Fin m → H)
    (hεS : ∀ i, ∀ s ∈ S, ⟪ε i, s⟫ = 0)
    (hεβ : ∀ (i : Fin m) (j : Fin n), ⟪ε i, β j⟫ = 0)
    (Q : Matrix (Fin m) (Fin m) ℝ) (hQ : ∀ i j, ⟪ε i, ε j⟫ = Q i j)
    (y : Fin m → H) (hy : ∀ i, y i = ∑ j, W i j • β j + ε i)
    (hdet : IsUnit (W * R * Wᵀ + Q).det)
    (G : Matrix (Fin n) (Fin m) ℝ) (hG : G = R * Wᵀ * (W * R * Wᵀ + Q)⁻¹)
    (βt : Fin n → H)
    (hβt : ∀ i, βt i = βh i + ∑ k, G i k • (y k - ∑ j, W k j • βh j)) :
    (∀ i, βt i ∈ S ⊔ Submodule.span ℝ (Set.range y)) ∧
    (∀ i, ∀ s ∈ S ⊔ Submodule.span ℝ (Set.range y), ⟪β i - βt i, s⟫ = 0) ∧
    (∀ i j, ⟪β i - βt i, β j - βt j⟫ =
      (R - R * Wᵀ * (W * R * Wᵀ + Q)⁻¹ * W * R) i j) := by sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, §4.6, Example 1, pp. 92–93

Read-back

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

Read-back of VectorSpaceOpt.estimate_update

This theorem is stated over an arbitrary type $H$ carrying the structure of a normed additive commutative group and a real inner product space; $\langle \cdot,\cdot\rangle$ below denotes its real inner product. It universally quantifies over natural numbers $n$ and $m$ (both may be $0$ ), a submodule ( $\mathbb{R}$ -linear subspace) $S \subseteq H$ , and the following data and hypotheses:

families of vectors $\beta_1,\dots,\beta_n \in H$ $β_{1}, \dots, β_{n} \in H$ and $\hat\beta_1,\dots,\hat\beta_n \in H$ $\hat{β}_{1}, \dots, \hat{β}_{n} \in H$ (indexed by $\{1,\dots,n\}$ ${1, \dots, n}$ ), with:
- $\hat\beta_i \in S$ for every $i$ ;
- $\langle \beta_i - \hat\beta_i,\, s\rangle = 0$ for every $i$ and every $s \in S$ ;
a real $n \times n$ matrix $R$ such that $\langle \beta_i - \hat\beta_i,\, \beta_j - \hat\beta_j\rangle = R_{ij}$ for all $i,j$ ;
a real $m \times n$ $m \times n$ matrix $W$ $W$ and vectors $\varepsilon_1,\dots,\varepsilon_m \in H$ $ε_{1}, \dots, ε_{m} \in H$ , with:
- $\langle \varepsilon_i, s\rangle = 0$ for every $i$ and every $s \in S$ ;
- $\langle \varepsilon_i, \beta_j\rangle = 0$ for every $i \in \{1,\dots,m\}$ and $j \in \{1,\dots,n\}$ ;
a real $m \times m$ matrix $Q$ such that $\langle \varepsilon_i, \varepsilon_j\rangle = Q_{ij}$ for all $i,j$ ;
vectors $y_1,\dots,y_m \in H$ satisfying, for every $i$ ,

y_i = \sum_{j=1}^{n} W_{ij}\,\beta_j + \varepsilon_i;

the hypothesis that the determinant of the $m \times m$ matrix $W R W^{\mathsf T} + Q$ is invertible (i.e. nonzero, so this matrix has a genuine inverse; the symbol ${}^{-1}$ below therefore denotes the true matrix inverse rather than a junk value);
an $n \times m$ real matrix $G$ defined by the hypothesis

G = R\,W^{\mathsf T}\,\bigl(W R W^{\mathsf T} + Q\bigr)^{-1};

vectors $\tilde\beta_1,\dots,\tilde\beta_n \in H$ satisfying, for every $i$ ,

\tilde\beta_i = \hat\beta_i + \sum_{k=1}^{m} G_{ik}\,\Bigl(y_k - \sum_{j=1}^{n} W_{kj}\,\hat\beta_j\Bigr).

Under all of these hypotheses, the theorem asserts the conjunction of three claims, in which $S \vee \operatorname{span}_{\mathbb R}\{y_1,\dots,y_m\}$ denotes the smallest submodule of $H$ containing both $S$ and the $\mathbb{R}$ -linear span of the set of values $\{y_1,\dots,y_m\}$ (i.e. their sum as subspaces):

for every $i \in \{1,\dots,n\}$ , the vector $\tilde\beta_i$ lies in $S \vee \operatorname{span}_{\mathbb R}\{y_1,\dots,y_m\}$ ;
for every $i \in \{1,\dots,n\}$ and every $s \in S \vee \operatorname{span}_{\mathbb R}\{y_1,\dots,y_m\}$ ,

\langle \beta_i - \tilde\beta_i,\, s\rangle = 0;

for all $i, j \in \{1,\dots,n\}$ ,

\langle \beta_i - \tilde\beta_i,\, \beta_j - \tilde\beta_j\rangle = \Bigl(R - R\,W^{\mathsf T}\bigl(W R W^{\mathsf T} + Q\bigr)^{-1} W\,R\Bigr)_{ij},

where the right-hand side is written out explicitly in the conclusion (it equals $(R - G W R)_{ij}$ given the defining hypothesis for $G$ , but the statement itself repeats the full expression).

Edge cases silently included by the quantifiers: if $n = 0$ there are no vectors $\beta_i, \hat\beta_i, \tilde\beta_i$ and all three conclusions are vacuously true; if $m = 0$ there are no $y_k$ or $\varepsilon_k$ , the span $\operatorname{span}_{\mathbb R}\{y_1,\dots,y_m\}$ is the zero subspace, the sum over $k$ in the definition of $\tilde\beta_i$ is empty (so $\tilde\beta_i = \hat\beta_i$ ), and the invertibility hypothesis concerns the empty $0 \times 0$ matrix, whose determinant is $1$ , so it holds automatically. The hypotheses do not require $S$ to be closed, $H$ to be complete or nonzero, or $R$ , $Q$ , $W$ to have any properties (such as symmetry or positive semidefiniteness) beyond the stated inner-product identities; the matrices $R$ , $Q$ are constrained only entrywise by those identities, and nothing asserts uniqueness of any of the data.

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