The figure below shows a discrete-time linear system.
Discrete-time linear system
represents the discrete time instants. , and represent the state of the system, input to the system and measurement of the system at time respectively. The system is governed by the following equations -
is the modeling noise of the state and is the measurement noise of the sensors. , , and are random variables, and , , and are deterministic. The task of filtering is to obtain an estimate of state , given observations . The Kalman filter is a linear unbiased estimator which minimizes the mean squared error. We present the proof of Kalman filter here for a discrete-time linear system.
Notations
We use the following notations:
Assumptions
We assume the following:
and are zero-mean white noise.
and are symmetric positive-definite matrices.
and are uncorrelated with and .
and are the given initial state conditions. is uncorrelated with and .
Kalman Filter
Kalman filter gives a recursive formula for the estimates in prediction and update steps.
Prediction
Update
The Kalman filter propagates the conditional mean and variance of the state, by expressing and in terms of and .
is the prior estimate of before observing , and is the posterior estimate of after the measurement of the state. Similarly and are the prior and posterior estimates of the variance of the state.
is called the Kalman Gain at time , because it weighs the information gained from the measurement by taking its difference with the predicted measurement .
We prove three lemmas in the next section, two of which involve taking the gradient of trace operations and the other concerns with uncorrelated random variables. We use those to prove the Kalman Filter equations in section.
Lemmas
Lemma 1
, if and are uncorrelated, and one of or is 0.
Proof
Proof
and are uncorrelated, therefore . One of or equals 0, therefore .
Similarly, .
Expanding ,
Therefore .
Lemma 2
Proof
Proof
Let and .
Taking gradient with respect to ,
Therefore .
Lemma 3
Proof
Proof
Let and .
Taking gradient with respect to ,
Therefore,
Proof
We prove the prediction and update equations of Kalman Filter.
Let us rewrite the equations governing the discrete-time linear system.
We find using the Kalman Filter state equation.
We substitute in the definition of using equation .
From definition, we know that for some function , and is uncorrelated with and .
Therefore is uncorrelated with . , and we can use Lemma 1.
Kalman filter is an unbiased linear optimal estimator. This implies the following:
Unbiased - The expected value of an unbiased estimator equals the expected value of the parameter. Therefore, and .
Linear - A linear estimator means it is a linear combination of the observations, which in this case is .
is a function of . Therefore let , for some matrix and .
Optimal - The estimator minimizes the mean squared error. Therefore, .
We use these three conditions to find and .
Substituting in the expression of ,
We substitute in the definition of using equation ,
for some function , and is uncorrelated with and . Therefore is uncorrelated with . . Therefore we can use Lemma 1.
We find by minimizing the conditional mean squared error of , .
We express as a trace of , and use equation to write it in terms of . We then minimize and find .
Taking the gradient of with respect to and setting it equal to 0,
We can simplify the expression of in equation using equation .