Proving that the uncertainty can not increase during the update step of a Kalman filter - positive semidefiniteness

Question

I am trying to prove mathematically that the update step in a Kalman filter can not result in a increase in uncertainty. I found the following proof which is based on the inversion lemma and the concept of positive semidefiniteness, but I can't grasp why the matrix product in the end is positive semi-definite.

Proof:

The uncertainty in the belief after the update step is expressed by the covariance matrix :

$\Sigma_t = (I - K_tC_t)\bar{\Sigma_{t}}$ (1)

where $\bar{\Sigma_t}$ is the predicted covariance before the update and $K_t$ is the Kalman Gain term, which is defined as:

$K_t = \bar{\Sigma_t}{C_t}^T(C_t\bar{\Sigma_t}{C_t}^T + {Q_t})^{-1}$ (2)

where $C_t$ and $Q_t$ are the parameters of the $z_t$ measurement's distribution $p(z_t | x_t) \sim \mathcal{N}(C_tx_t, Q_t) $

By expanding the $K_t$ term in equation (1) and then by applying the matrix inversion lemma/Woodburry matrix identity, we get:

$ \Sigma_t = \bar{\Sigma_{t}} - \bar{\Sigma_t}{C_t}^T(C_t\bar{\Sigma_t}{C_t}^T + {Q_t})^{-1}C_t\bar{\Sigma_t} \\ = (\bar{\Sigma}^{-1}_t + {C_t}^T{Q^{-1}_t}C_t)^{-1}$

The proof mentions that ${C_t}^T{Q^{-1}_t}C_t$ is positive semi-definite and hence the uncertainty cannot increase.

End of proof

Question: I know that $Q_t$ is positive semi-definite since it is a covariance matrix but I haven't been able to understand why ${C_t}^T{Q^{-1}_t}C_t$ is positive semi-definite. Can someone explain?

Answer 1

$Q_t$ is real-valued and positive definite, thus $Q_t^{-1}$ is real-valued and positive definite.

Now it's just making up a lemma of the Cholesky decomposition:

• If $Q_t^{-1}$ is real-valued and positive definite, then there's some real-valued $q$ such that $q_t^T q_t = Q_t^{-1}$ (Cholesky decomposition)
• If that holds, then $\left(q_t C_t \right)^T\left(q_t C_t \right)$ must be real-valued and at least positive semidefinite for any real-valued $C_t$ (Cholesky again -- that guy gets around)
• $\left(q_t C_t \right)^T\left(q_t C_t \right) = C_t^T q_t^T q_t C_t = C_t^T Q_t^{-1} C_t$
• Cogito, ergo sum. Or QED$^*$, or something brainy, and Latin.

${\tiny ^* {\rm quod\ erat\ demonstrandum.}}$