Solution of the recursive estimation problem (Kalman)

Proved

VectorSpaceOpt.kalman_recursion

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

estimationkalman-filterstochastic-systems

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

Consider the $n$ -dimensional dynamic model: a state evolving linearly with noise, observed through a linear measurement with noise,

x(k+1) = \Phi(k)\,x(k) + u(k), \qquad v(k) = M(k)\,x(k) + w(k), \qquad k = 0, 1, 2, \dots

with $\Phi(k)$ , $M(k)$ known matrices. The process noises are white — $E[u(k)u(l)^\top] = Q(k)\delta_{kl}$ and $E[w(k)w(l)^\top] = R(k)\delta_{kl}$ with each $R(k)$ positive definite — mutually uncorrelated and uncorrelated with the initial state $x(0)$ .

Write $\hat x(k \mid k-1)$ for the estimate of $x(k)$ given the measurements up to time $k-1$ . Starting from $\hat x(0 \mid -1) = 0$ and $P(0) = \operatorname{cov} x(0)$ , generate estimates and matrices by the recursions

\hat x(k+1 \mid k) = \Phi(k) P(k) M^\top(k)\big[M(k)P(k)M^\top(k) + R(k)\big]^{-1}\big(v(k) - M(k)\hat x(k \mid k-1)\big) + \Phi(k)\,\hat x(k \mid k-1),

P(k+1) = \Phi(k) P(k)\Big\{I - M^\top(k)\big[M(k)P(k)M^\top(k) + R(k)\big]^{-1} M(k) P(k)\Big\}\Phi^\top(k) + Q(k).

Then for every $k$ :

each component of $\hat x(k \mid k-1)$ lies in the span of the past measurement components $v(0), \dots, v(k-1)$ ;
each error component $x(k)_i - \hat x(k \mid k-1)_i$ is orthogonal to every past measurement component;
the error covariance is $\big\langle x(k)_i - \hat x(k\mid k-1)_i,\ x(k)_j - \hat x(k \mid k-1)_j \big\rangle = P(k)_{ij}$ .

By the projection theorem, claims 1 and 2 say exactly that $\hat x(k \mid k-1)$ is the linear minimum-variance estimate of $x(k)$ given the past data — so the recursion computes the optimal estimate, and $P(k)$ tracks its error covariance. This is the discrete-time Kalman filter, obtained here with no Gaussian assumption anywhere: only second-order statistics enter, and optimality is among linear estimates.

Formalization Note. The two recursions are supplied as hypotheses defining $\hat x$ and $P$ , so the conclusions assert precisely the optimality and covariance claims. Being the optimal estimate is expressed as span membership plus orthogonality of the error rather than through a projection operator. Zero means are implicit in the Hilbert-space-of-random-variables representation, so expectations appear only as inner products.

Preamble

import Mathlib
open Matrix
open scoped RealInnerProductSpace

Formal statement

namespace VectorSpaceOpt

theorem kalman_recursion {H : Type} [NormedAddCommGroup H]
    [InnerProductSpace ℝ H] {n m : ℕ}
    (Φ : ℕ → Matrix (Fin n) (Fin n) ℝ) (M : ℕ → Matrix (Fin m) (Fin n) ℝ)
    (Q : ℕ → Matrix (Fin n) (Fin n) ℝ) (R : ℕ → Matrix (Fin m) (Fin m) ℝ)
    (hR : ∀ k, (R k).PosDef)
    (x u : ℕ → Fin n → H) (w v : ℕ → Fin m → H)
    (hdyn : ∀ k i, x (k + 1) i = ∑ j, Φ k i j • x k j + u k i)
    (hmeas : ∀ k i, v k i = ∑ j, M k i j • x k j + w k i)
    (hQcov : ∀ k l i j, ⟪u k i, u l j⟫ = if k = l then Q k i j else 0)
    (hRcov : ∀ k l i j, ⟪w k i, w l j⟫ = if k = l then R k i j else 0)
    (huw : ∀ k l i j, ⟪u k i, w l j⟫ = 0)
    (hux0 : ∀ k i j, ⟪u k i, x 0 j⟫ = 0)
    (hwx0 : ∀ k i j, ⟪w k i, x 0 j⟫ = 0)
    (P : ℕ → Matrix (Fin n) (Fin n) ℝ) (xh : ℕ → Fin n → H)
    (hP0 : ∀ i j, P 0 i j = ⟪x 0 i, x 0 j⟫)
    (hxh0 : ∀ i, xh 0 i = 0)
    (hrec : ∀ k i, xh (k + 1) i =
      ∑ j, (Φ k * P k * (M k)ᵀ * (M k * P k * (M k)ᵀ + R k)⁻¹) i j •
          (v k j - ∑ l, M k j l • xh k l) +
        ∑ j, Φ k i j • xh k j)
    (hPrec : ∀ k, P (k + 1) =
      Φ k * P k * (1 - (M k)ᵀ * (M k * P k * (M k)ᵀ + R k)⁻¹ * M k * P k) *
          (Φ k)ᵀ + Q k) :
    (∀ k i, xh k i ∈ Submodule.span ℝ {a : H | ∃ l < k, ∃ j, a = v l j}) ∧
    (∀ k, ∀ l < k, ∀ i j, ⟪x k i - xh k i, v l j⟫ = 0) ∧
    (∀ k i j, ⟪x k i - xh k i, x k j - xh k j⟫ = P k i j) := by sorry

end VectorSpaceOpt

Source

David G. Luenberger, Optimization by Vector Space Methods, John Wiley & Sons, 1969, §4.7, Theorem 1, p. 96; R. E. Kalman, J. Basic Eng. 82 (1960) 35–45, https://doi.org/10.1115/1.3662552

Read-back

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

Read-back — kalman_recursion

Let $H$ be a real inner product space (a normed additive commutative group equipped with a real inner product $\langle\cdot,\cdot\rangle$ ; $H$ may be any such space, including the zero space), and let $n, m$ be natural numbers, both allowed to be $0$ . All "vectors" below are families of elements of $H$ : for each time $k \in \{0,1,2,\dots\}$ , the state $x_k$ and the quantity $u_k$ are families $(x_k^i)_{i}$ , $(u_k^i)_i$ of $n$ elements of $H$ (indices $i$ ranging over an $n$ -element set), while $w_k$ and $v_k$ are families of $m$ elements of $H$ . The data also includes, for every $k$ : an $n\times n$ real matrix $\Phi_k$ , an $m \times n$ real matrix $M_k$ , an $n \times n$ real matrix $Q_k$ , and an $m \times m$ real matrix $R_k$ , with each $R_k$ assumed positive definite (in particular symmetric).

The hypotheses are:

Dynamics: for all $k$ and $i$ ,

x_{k+1}^i = \sum_{j} (\Phi_k)_{ij}\, x_k^j + u_k^i .

Measurement: for all $k$ and $i$ ,

v_k^i = \sum_{j} (M_k)_{ij}\, x_k^j + w_k^i .

Inner-product structure (stated with inner products in $H$ , not with any probabilistic expectation; no zero-mean or distributional assumption appears anywhere):

\langle u_k^i, u_l^j\rangle = \begin{cases}(Q_k)_{ij} & k = l\\ 0 & k \neq l\end{cases}, \qquad \langle w_k^i, w_l^j\rangle = \begin{cases}(R_k)_{ij} & k = l\\ 0 & k \neq l\end{cases},

for all $k, l, i, j$ ; moreover $\langle u_k^i, w_l^j\rangle = 0$ for all $k,l,i,j$ , and $\langle u_k^i, x_0^j\rangle = 0$ , $\langle w_k^i, x_0^j\rangle = 0$ for all $k,i,j$ . Note these force $Q_k$ and $R_k$ to be Gram matrices of vectors in $H$ ; combined with positive definiteness of $R_k$ , the hypotheses can only be satisfied when the $m$ vectors $w_k^1,\dots,w_k^m$ are linearly independent in $H$ (so, e.g., if $m > \dim H$ the hypotheses are unsatisfiable and the theorem is vacuous). $Q_k$ is not assumed positive definite or even semidefinite as a matrix hypothesis.

Given recursions: two further data, a sequence of $n\times n$ real matrices $P_k$ and families $\hat{x}_k = (\hat{x}_k^i)_i$ of $n$ elements of $H$ , are hypothesized (not constructed) to satisfy: initial conditions

(P_0)_{ij} = \langle x_0^i, x_0^j\rangle, \qquad \hat{x}_0^i = 0 \ \text{ for all } i,

the estimate recursion, for all $k, i$ ,

\hat{x}_{k+1}^i = \sum_j (K_k)_{ij}\,\Big(v_k^j - \sum_{l} (M_k)_{jl}\, \hat{x}_k^l\Big) \;+\; \sum_j (\Phi_k)_{ij}\, \hat{x}_k^j, \qquad K_k := \Phi_k P_k M_k^\top \big(M_k P_k M_k^\top + R_k\big)^{-1},

and the matrix recursion, for all $k$ ,

P_{k+1} = \Phi_k\, P_k\, \Big(I - M_k^\top \big(M_k P_k M_k^\top + R_k\big)^{-1} M_k P_k\Big)\, \Phi_k^\top + Q_k .

Here $(\,\cdot\,)^{-1}$ is the total matrix-inverse operation: if $M_k P_k M_k^\top + R_k$ is invertible it is the usual inverse, but if it is singular the operation silently returns the zero matrix, and the recursions are then hypotheses about that degenerate expression. No hypothesis asserts that $M_k P_k M_k^\top + R_k$ is invertible.

Under all of these hypotheses, the theorem asserts the conjunction of three claims:

Span membership: for every $k$ and every $i$ , the element $\hat{x}_k^i$ lies in the linear span (over $\mathbb{R}$ ) of the set of all observation components taken at times strictly before $k$ :

\hat{x}_k^i \in \operatorname{span}_{\mathbb{R}}\{\, v_l^j : l < k,\ j \text{ arbitrary} \,\}.

For $k = 0$ this set is empty, so the claim says $\hat{x}_0^i = 0$ (i.e. $\hat x_0^i$ lies in the zero subspace).

Orthogonality of the error to past observations: for every $k$ , every $l < k$ , and all indices $i, j$ ,

\big\langle x_k^i - \hat{x}_k^i,\; v_l^j \big\rangle = 0.

For $k = 0$ this is vacuous (there is no $l < 0$ ).

Error Gram identity: for every $k$ and all $i, j$ ,

\big\langle x_k^i - \hat{x}_k^i,\; x_k^j - \hat{x}_k^j \big\rangle = (P_k)_{ij}.

If $n = 0$ or $m = 0$ , the corresponding index sets are empty: sums over them are $0$ , and all statements quantified over those indices hold vacuously. The proof is not given (the statement ends in sorry), so this records only what is claimed.

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