Linear_filter.Make
module Linear : sig ... end
The linear space in which the filters are defined.
A source describes a source of measures, for instance a specific sensor, that is treated at each iteration by the filter. Measures can be centered around any scalar, and are thus described by a center and a deviation. The source's delay is hidden inside the type.
val source :
matrix:('n Nat.succ, 'm Nat.succ) Linear.matrix ->
center:Field.scalar ->
deviation:Field.scalar ->
'n Nat.succ source
Sources constructor. The inputs are as following :
matrix
is the source matrix, describing how the current and past measures are taken into account ;center
is the measures center ;deviation
is the measures deviation.A value of type n filter
describes a filter of order n
(i.e with n
state variables). The sources delays are contained by each one of them.
val create :
state:('n Nat.succ, 'n Nat.succ) Linear.matrix ->
center:'n Nat.succ Linear.vector ->
sources:'n Nat.succ source list ->
'n Nat.succ filter
Filters constructors. The inputs are as following :
center
is the filter's center ;state
is the filter's state matrix ;sources
is the list of the filter's sources.val pretty : Stdlib.Format.formatter -> 'n filter -> unit
Filters pretty printer.
Representation of a filter's invariant. Bounds for each dimension can be accessed using the corresponding functions.
val lower : 'n Finite.finite -> 'n invariant -> Field.scalar
val upper : 'n Finite.finite -> 'n invariant -> Field.scalar
val bounds : 'n Finite.finite -> 'n invariant -> Field.scalar * Field.scalar
Invariant computation. The computation of invariant filter k
relies on the search of an exponent such as the norm of the state matrix is strictly lower than one. For the filter to converge, there must exist an α such as, for every β greater than α, ||A^β|| < 1 with A the filter's state matrix. As such, the search does not have to find α, but instead any exponent such as the property is satisfied. As the computed invariant will be more precise with a larger exponent, the computation always uses k
, the largest authorized exponent, and thus only check that indeed ||A^k|| < 1. If the property is not verified, the function returns None as it cannot prove that the filter converges.
The only thing limiting the invariant optimality is k
. However, for most simple filters, k = 200 will gives exact bounds up to at least ten digits, which is more than enough. Moreover, for those simple filters, the computation is immediate, even when using rational numbers.