Lyapunov Minimization Condition

LyapunovMinimizationCondition(check_nonnegativity, strength, rectifier, check_fixed_point)

Specifies the form of the Lyapunov minimization condition to be used.

Fields

• check_nonnegativity::Bool: whether or not to train for positivity/nonnegativity of $V(x)$.
• strength: specifies the level of strictness for positivity training; should be zero when the two inputs are equal and nonnegative otherwise; used when check_nonnegativity is true.
• rectifier: positive when the input is positive and (approximately) zero when the input is negative.
• check_fixed_point: whether or not to train for $V(x_0) = 0$.

Training conditions

If check_nonnegativity is true, training will attempt to enforce:

$V(x) ≥ \texttt{strength}(x, x_0).$

The inequality will be approximated by the equation:

$\texttt{rectifier}(\texttt{strength}(x, x_0) - V(x_0)) = 0.$

Note that the approximate equation and inequality are identical when $\texttt{rectifier}(t) = \max(0, t)$.

If check_fixed_point is true, then training will also attempt to enforce $V(x_0) = 0$.

Examples

When training for a strictly positive definite $V$, an example of an appropriate strength is $\texttt{strength}(x, x_0) = \lVert x - x_0 \rVert^2$. This form is used in StrictlyPositiveDefinite.

If $V$ were structured such that it is always nonnegative, then $V(x_0) = 0$ is all that must be enforced in training for the Lyapunov function to be uniquely minimized at $x_0$. In that case, we would use check_nonnegativity = false; check_fixed_point = true. This can also be accomplished with DontCheckNonnegativity(true).

In either case, the rectified linear unit rectifier(t) = max(zero(t), t) exactly represents the inequality, but differentiable approximations of this function may be employed.

StrictlyPositiveDefinite(; C, check_fixed_point, rectifier)

Construct a LyapunovMinimizationCondition representing $V(x) ≥ C \lVert x - x_0 \rVert^2$. If check_fixed_point == true (as is the default), then training will also attempt to enforce $V(x_0) = 0$.

The inequality is approximated by $\texttt{rectifier}(C \lVert x - x_0 \rVert^2 - V(x)) = 0$, and the default rectifier is the rectified linear unit (t) -> max(zero(t), t), which exactly represents $V(x) ≥ C \lVert x - x_0 \rVert^2$. $C$ defaults to 1e-6.

Examples

julia> StrictlyPositiveDefinite()
LyapunovMinimizationCondition
    Trains for V(x) ≥ 1.0e-6((x - x_0)²)
    with approximation a ≤ 0 => max(0, a) ≈ 0
    Trains for V(x_0) = 0

julia> softplus = (t) -> log(one(t) + exp(t));

julia> StrictlyPositiveDefinite(C = 0.1, rectifier = softplus, check_fixed_point = false)
LyapunovMinimizationCondition
    Trains for V(x) ≥ 0.1((x - x_0)²)
    with approximation a ≤ 0 => log(1 + exp(a)) ≈ 0
    Does not train for V(x_0) = 0

PositiveSemiDefinite(; check_fixed_point, rectifier)

Construct a LyapunovMinimizationCondition representing $V(x) ≥ 0$. If check_fixed_point == true (as is the default), then training will also attempt to enforce $V(x_0) = 0$.

The inequality is approximated by $\texttt{rectifier}( -V(x) ) = 0$ and the default rectifier is the rectified linear unit (t) -> max(zero(t), t), which exactly represents $V(x) ≥ 0$.

Examples

julia> PositiveSemiDefinite()
LyapunovMinimizationCondition
    Trains for V(x) ≥ 0.0
    with approximation a ≤ 0 => max(0, a) ≈ 0
    Trains for V(x_0) = 0

julia> softplus = (t) -> log(one(t) + exp(t));

julia> PositiveSemiDefinite(rectifier = softplus, check_fixed_point = false)
LyapunovMinimizationCondition
    Trains for V(x) ≥ 0.0
    with approximation a ≤ 0 => log(1 + exp(a)) ≈ 0
    Does not train for V(x_0) = 0

DontCheckNonnegativity(; check_fixed_point)

Construct a LyapunovMinimizationCondition which represents not checking for nonnegativity of the Lyapunov function. This is appropriate in cases where this condition has been structurally enforced.

Even in this case, it is still possible to check for $V(x_0) = 0$, for example if V is structured to be positive for $x ≠ x_0$ but does not guarantee $V(x_0) = 0$ (such as NonnegativeStructure). check_fixed_point defaults to true, since in cases where $V(x_0) = 0$ is enforced structurally, the equation will reduce to 0.0 ~ 0.0, which gets automatically removed in most cases.

Examples

julia> DontCheckNonnegativity()
LyapunovMinimizationCondition
    Does not train for nonnegativity of V(x)
    Trains for V(x_0) = 0

julia> DontCheckNonnegativity(check_fixed_point = false)
LyapunovMinimizationCondition
    Does not train for nonnegativity of V(x)
    Does not train for V(x_0) = 0

AbstractLyapunovMinimizationCondition

Developer interface for the minimization condition in a neural Lyapunov problem.

A subtype must implement check_nonnegativity, check_minimal_fixed_point, and get_minimization_condition. The first two generic functions return Bools. If check_nonnegativity(cond) is true, get_minimization_condition(cond) must return a callable (V, state, fixed_point) -> residual, where V is callable as V(state) and residual is a scalar or a vector whose entries are all zero when the condition is satisfied. If the flag is false, the returned condition may be nothing, because no minimization equation is generated. The check_minimal_fixed_point flag independently controls whether V(fixed_point) = 0 is added by NeuralLyapunovPDESystem.

Implementations should extend these generic functions for their own subtype and should not depend on the fields of another package's concrete condition.

Example

struct MyMinimizationCondition <: AbstractLyapunovMinimizationCondition end

NeuralLyapunov.check_nonnegativity(::MyMinimizationCondition) = true
NeuralLyapunov.check_minimal_fixed_point(::MyMinimizationCondition) = true
NeuralLyapunov.get_minimization_condition(::MyMinimizationCondition) =
    (V, state, fixed_point) -> V(state) - V(fixed_point)

check_nonnegativity(cond::AbstractLyapunovMinimizationCondition)

Return true if cond specifies training to meet the Lyapunov minimization condition, and false if cond specifies no training to meet this condition.

Arguments

• cond: the minimization condition being queried.

Returns

A Bool. When true, the generic PDESystem construction consumes the residual returned by get_minimization_condition.

check_minimal_fixed_point(cond::AbstractLyapunovMinimizationCondition)

Return true if cond specifies training for the Lyapunov function to equal zero at the fixed point, and false if cond specifies no training to meet this condition.

Arguments

• cond: the minimization condition being queried.

Returns

A Bool controlling whether the generic PDESystem construction adds the equation V(fixed_point) = 0.

get_minimization_condition(cond::AbstractLyapunovMinimizationCondition)

Return a function of $V$, $x$, and $x_0$ that equals zero when the Lyapunov minimization condition is met for the Lyapunov candidate function $V$ at the point $x$, and is greater than zero if it's violated.

Note that the first input, $V$, is a function, so the minimization condition can depend on the value of the candidate Lyapunov function at multiple points.

If the returned function returns a vector, all elements of the vector must be zero for the condition to be considered met. NeuralLyapunovPDESystem will create one equation per element of the vector.

Arguments

• cond: the minimization condition being queried.

Returns

Either nothing when no nonnegativity equation is requested, or a callable (V, state, fixed_point) -> residual returning a scalar or vector residual.