Prove2Me

The single-step updating formula

Proved
VectorSpaceOpt.estimate_update

by Shuze Chen · Aug 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

estimationhilbert-spacekalman-filter

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

Suppose an optimal estimate β^\hat\beta of a random nn-vector β\beta has been formed from past data generating a subspace SS, with error covariance

Rij=⟨βi−β^i, βj−β^j⟩.R_{ij} = \big\langle \beta_i - \hat\beta_i,\ \beta_j - \hat\beta_j \big\rangle .

Now additional measurements arrive,

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

where the noise ε\varepsilon has covariance Qij=⟨εi,εj⟩Q_{ij} = \langle \varepsilon_i, \varepsilon_j\rangle, is orthogonal to SS, and is uncorrelated with β\beta; assume WRW⊤+QW R W^\top + Q is invertible. Then the updated optimal estimate is

β~  =  β^  +  RW⊤(WRW⊤+Q)−1 (y−Wβ^),\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−RW⊤(WRW⊤+Q)−1WR.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 SS together with the components of yy.

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β^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

View graph