Revision #2104 → #2799 · back to history
modifiedMutual independence of initial state and noiseab9b8dd83205
| Field | From #2104 | To #2799 |
|---|
| note | General mutual independence of random variables exists, but the specific Kalman noise-independence assumption is not formalized. | General mutual independence of random variables (`iIndepFun`) exists in Mathlib, but the specific Kalman noise-independence assumption is not formalized. |
modifiedMarkov conditional independence of true state935837fb3080
| Field | From #2104 | To #2799 |
|---|
| note | Generic conditional independence exists, but the specific Markov-chain conditional independence is not formalized. | Generic conditional independence (`CondIndepFun`) exists, but the specific Markov-chain conditional independence is not formalized. |
modifiedConditional independence of measurements40e1908d36a7
| Field | From #2104 | To #2799 |
|---|
| note | General conditional independence machinery exists; the specific Kalman measurement independence is not formalized. | General conditional independence machinery (`CondIndepFun`) exists; the specific Kalman measurement independence is not formalized. |
modifiedKalman filter as Gaussian process regression solverfb29059015c9
| Field | From #2104 | To #2799 |
|---|
| note | Gaussian processes are defined in Mathlib, but the Kalman-as-GP-regression viewpoint is not formalized. | Gaussian processes (`IsGaussianProcess`) are defined in Mathlib, but the Kalman-as-GP-regression viewpoint is not formalized. |
addedContinuous-state hidden Markov model analogyac956ede34ea
addedProcess noise as zero-mean multivariate Gaussiandae1fd1e2af9
addedObservation noise as zero-mean Gaussian white noise269b65ad0e63
addedMarginal likelihood as product of Gaussian densities07295fc485da
addedWeighted-average state updateb448c6cfbd67