26. Update a Gaussian model from one observation

On this page

All examples · Glossary: posterior · Papers, proofs, Lean, and code

Certified Inference and its Bayesian research companion separate the exact posterior from an approximation built using a candidate gain. Here is a two-coordinate example with exact rational mean and covariance calculations.

Declare the model

Let the prior state be \(X\sim\mathcal N(0,I_2)\). Observe

\[Y=HX+V,\qquad H=\begin{pmatrix}1&1\end{pmatrix},\qquad V\sim\mathcal N(0,1), \]

where \(V\) is independent of \(X\). Take the observed value to be \(y=3\). The model describes a noisy sum of the two state coordinates. In the package's factor convention, \(L=I_2\), a zero noise factor and \(\sigma=1\) give the declared prior covariance \(P=I_2\) and noise covariance \(R=1\).

Calculate the gain and posterior mean

The innovation is \(d=y-Hm=3\), where the prior mean \(m\) is zero. The innovation variance and exact gain are

\[S=HPH^{\mathsf T}+R=2+1=3,\qquad K=PH^{\mathsf T}S^{-1}=\begin{pmatrix}1/3\\1/3\end{pmatrix}. \]

Thus the posterior mean is \(m+Kd=(1,1)^{\mathsf T}\). The noise means that the posterior mean of the sum, two, need not equal the observed value, three.

Calculate and check the covariance

For the exact gain,

\[C_*=P-KHP =\begin{pmatrix}2/3&-1/3\\-1/3&2/3\end{pmatrix}. \]

The normalized sum direction \((1,1)^{\mathsf T}/\sqrt2\) has posterior variance \(1/3\). The normalized difference direction \((1,-1)^{\mathsf T}/\sqrt2\) still has variance one. This observation informs the sum and leaves the independent difference unchanged.

We can check the posterior directly by completing the square in its density. The prior times the likelihood is proportional to

\[\exp\!\left[-\frac12\bigl(x_1^2+x_2^2+(3-x_1-x_2)^2\bigr)\right]. \]

Write \(\mu=(1,1)^{\mathsf T}\) and set

\[J=\begin{pmatrix}2&1\\1&2\end{pmatrix}. \]

The expression inside parentheses is

\[(x-\mu)^{\mathsf T}J(x-\mu)+3. \]

The constant affects normalization. The precision matrix is \(J\), and direct multiplication gives \(JC_*=I_2\), confirming the same covariance.

Keep a candidate gain's covariance valid

For a general gain \(B\), use the Joseph covariance

\[C_B=(I_2-BH)P(I_2-BH)^{\mathsf T}+BRB^{\mathsf T}. \]

Choose \(B=(1/4,1/4)^{\mathsf T}\). Its mean is \((3/4,3/4)^{\mathsf T}\), and

\[I_2-BH=\begin{pmatrix}3/4&-1/4\\-1/4&3/4\end{pmatrix},\qquad C_B=\begin{pmatrix}11/16&-5/16\\-5/16&11/16\end{pmatrix}. \]

The residual \(PH^{\mathsf T}-BS=(1/4,1/4)^{\mathsf T}\) is nonzero. This candidate defines a Gaussian approximation, with a different mean and covariance from the posterior. Substituting \(B\) into \(P-BHP\) would give a different matrix and is not the general candidate covariance formula.

Try it

Keep the original model but observe \(y=-3\). Find the exact posterior mean and covariance.

Answer: The mean becomes \((-1,-1)^{\mathsf T}\). The covariance stays \(C_*\) because \(P,H,R\), and hence the exact gain, are unchanged.

This tutorial checks the model's matrix identities. A certified tolerance for an approximate law and certified output intervals require the package's full checks. No new Lean instance or sampler is claimed here.

Papers, proofs, Lean, and code

Terms in this example: Finite-dimensional Gaussian model · Prior distribution · Likelihood · Posterior distribution · Covariance matrix · Precision matrix · Observation innovation · Exact Gaussian gain · Joseph covariance

These calculations explain the exact Gaussian model and a candidate Joseph covariance. The release’s law-error tolerance, interval output and emitted Lean-instance checks require their full contracts.

Certified Inference

Read · Written proofs · Lean coverage · Code and setup · Evidence

Certified Bayesian Inference

Read · Written proofs · Lean coverage · Code and setup · Evidence

Source passages:

Edition guide and reproduction instructions. Use each work’s Code and setup link for its implementation. The arithmetic check below covers this tutorial separately.

Python arithmetic check for this example: gaussian_update(). This checks the displayed rational, modular or finite-set calculations exactly.

The Lean links open each work’s recorded coverage and sources. They do not certify this tutorial. A work may have limited coverage or no linked Lean or code. Its page states what is available.