Alphabeta Math
AlgorithmAlgorithm: Literature-sourcedProof: Not applicablePipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Rauch–Tung–Striebel fixed-interval Gaussian smoother

Definition

Fix a finite-horizon linear-Gaussian model from Linear-Gaussian state-space models with independent noises and data y1:T for which Exact linear-Gaussian Kalman filter is admissible. Its forward output contains filtered means and covariances mk∣k,Pk∣k and predicted means and covariances mk+1∣k,Pk+1∣k. Assume each forecast covariance used below is positive definite, meaning uTPk+1∣ku>0 for every nonzero u∈Rdk+1. Positive semidefinite means the same quadratic form is nonnegative for every u.

The algorithm takes that forward output as input, initializes mT∣T:=mT∣Tfilter,PT∣T:=PT∣Tfilter and for k=T−1,T−2,…,0 performs the following steps:

  1. Form the backward gain Ck=Pk∣kFk+1TPk+1∣k−1. For the computation, factor Pk+1∣k=LkLkT with the unique positive-diagonal Cholesky factor from A matrix admits a Cholesky factorisation with positive diagonal exactly when it is Hermitian positive definite, and that factor is unique, then compute the rows of Uk in increasing order by (Uk)i,⋅=(Fk+1Pk∣k)i,⋅−∑j=1i−1(Lk)ij(Uk)j,⋅(Lk)ii,i=1,…,dk+1, and compute the rows of CkT in decreasing order by (CkT)i,⋅=(Uk)i,⋅−∑j=i+1dk+1(Lk)ji(CkT)j,⋅(Lk)ii,i=dk+1,…,1. These recurrences give LkUk=Fk+1Pk∣k and LkTCkT=Uk, so Ck=Pk∣kFk+1TPk+1∣k−1; no inverse is formed in the procedure.
  2. Update the smoothed mean and covariance: mk∣T=mk∣k+Ck(mk+1∣T−mk+1∣k) Pk∣T=Pk∣k+Ck(Pk+1∣T−Pk+1∣k)CkT

Return (mk∣T,Pk∣T)k=0T. For T=0 the loop is empty and the output is the initial filtered pair. The algorithm is undefined if a forecast covariance to be solved is singular; it makes no pseudoinverse, complexity, rounding-error, or numerical-stability claim. The theorem on this page proves that the outputs are moments of the fixed-interval conditional laws under these hypotheses.

Depends on

Used by

Dependency tree · two levels

14 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources