Systems.Continuous — the general continuous-time system

The most general continuous-time system the library considers,

• ContinuousSystem E U Y — ẋ = F(t, x, u), y = h(t, x, u), with t ∈ ℝ,

with state space E, input space U and output space Y. The linear systems of LinearSystems.Continuous are special cases. Its discrete-time counterpart is DiscreteSystem in Systems.Discrete, which carries the same API under the same names.

Special cases

Each special case is a constructor building the general object from the special data, together with a predicate recognising it inside a general system and a lemma relating the two:

• Time invariance — t is dropped: timeInvariant f h builds F(t, x, u) = f(x, u), and IsTimeInvariant says F and h do not depend on time.
• Autonomy — u is dropped: autonomous f h builds a system with input space Unit, and IsAutonomous says F and h do not depend on the input.

The two combine: timeInvariant applied to input-free data gives ẋ = f(x).

"Autonomous" here means without input, the control-theory convention. Much of the dynamical-systems literature, including Khalil, uses it for time-invariant instead.

Trajectories

There are two trajectory predicates, for two kinds of input.

• IsTrajectoryOn s u x I is the derivative form, Mathlib's IsIntegralCurveOn: ẋ(t) = F(t, x(t), u(t)) for every t ∈ I, the derivative taken within I. It is the form the Lyapunov machinery works with, and the natural one for continuous inputs. Two caveats: at an isolated point of I the derivative within I is unconstrained, so I should be a nondegenerate segment [t₀, t₁] or a ray [t₀, ∞); and x must be differentiable everywhere on I, which excludes the solutions produced by discontinuous inputs (under a step input, ẋ = u has a corner).
• IsCaratheodoryTrajectoryOn s u x I is the integral form: between any a ≤ b in I, x(b) - x(a) = ∫ₐᵇ F(τ, x(τ), u(τ)) dτ. It needs E complete but not x differentiable, so it admits piecewise-constant, sampled-data, bang-bang and merely measurable inputs. Input-driven notions such as input-to-state stability are stated with it.

When τ ↦ F(τ, x(τ), u(τ)) is continuous the two agree on segments and on rays (isCaratheodoryTrajectoryOn_iff_isTrajectoryOn), via the integral-solution bridge isIntegralSolution_iff_isIntegralCurveOn. Neither handles discontinuity in the state, such as discontinuous feedback, which needs Filippov solutions.

Why separate continuous- and discrete-time objects

The same reasons as for ContinuousLTV and DiscreteLTV: the data is the same shape, but its reading is not. A continuous trajectory is an integral curve and needs a normed space; a discrete one is a recursion and needs nothing. A change of coordinates picks up a time-derivative term in continuous time and none in discrete time. Separate files also keep the analysis imports out of discrete-time developments, and leave room for further classes, such as hybrid systems, as files of their own.

Conventions

• The structure carries no typeclasses: structure on E, U, Y goes on the operations that need it.
• The API lives in the namespace ContinuousSystem, so dot notation resolves.

structure ContinuousSystem (E : Type u_1) (U : Type u_2) (Y : Type u_3) : Type (max (max u_1 u_2) u_3)

A continuous-time system: the data (F, h) of

ẋ(t) = F(t, x(t), u(t)), y(t) = h(t, x(t), u(t))

with states in E, inputs in U and outputs in Y. The structure is only the data.

• F : ℝ → E → U → E

  State equation: ẋ = F(t, x, u).

• h : ℝ → E → U → Y

  Output equation: y = h(t, x, u).

def ContinuousSystem.timeInvariant {E : Type u_1} {U : Type u_2} {Y : Type u_3} (f : E → U → E) (g : E → U → Y) : ContinuousSystem E U Y

The time-invariant system ẋ = f(x, u), y = g(x, u).

Equations

• ContinuousSystem.timeInvariant f g = { F := fun (x : ℝ) => f, h := fun (x : ℝ) => g }

@[simp]

theorem ContinuousSystem.timeInvariant_F {E : Type u_1} {U : Type u_2} {Y : Type u_3} (f : E → U → E) (g : E → U → Y) (t : ℝ) : (timeInvariant f g).F t = f

@[simp]

theorem ContinuousSystem.timeInvariant_h {E : Type u_1} {U : Type u_2} {Y : Type u_3} (f : E → U → E) (g : E → U → Y) (t : ℝ) : (timeInvariant f g).h t = g

def ContinuousSystem.IsTimeInvariant {E : Type u_1} {U : Type u_2} {Y : Type u_3} (s : ContinuousSystem E U Y) : Prop

The system is time-invariant: its equations take the same form at every time.

Equations

• s.IsTimeInvariant = ∀ (t t' : ℝ), s.F t = s.F t' ∧ s.h t = s.h t'

theorem ContinuousSystem.isTimeInvariant_timeInvariant {E : Type u_1} {U : Type u_2} {Y : Type u_3} (f : E → U → E) (g : E → U → Y) : (timeInvariant f g).IsTimeInvariant

A system built by timeInvariant is time-invariant.

theorem ContinuousSystem.IsTimeInvariant.exists_eq {E : Type u_1} {U : Type u_2} {Y : Type u_3} {s : ContinuousSystem E U Y} (hs : s.IsTimeInvariant) : ∃ (f : E → U → E) (g : E → U → Y), s = timeInvariant f g

A time-invariant system is built by timeInvariant.

def ContinuousSystem.autonomous {E : Type u_1} {Y : Type u_3} (f : ℝ → E → E) (g : ℝ → E → Y) : ContinuousSystem E Unit Y

The autonomous (input-free) system ẋ = f(t, x), y = g(t, x), with input space Unit.

Equations

• ContinuousSystem.autonomous f g = { F := fun (t : ℝ) (x : E) (x_1 : Unit) => f t x, h := fun (t : ℝ) (x : E) (x_1 : Unit) => g t x }

@[simp]

theorem ContinuousSystem.autonomous_F {E : Type u_1} {Y : Type u_3} (f : ℝ → E → E) (g : ℝ → E → Y) (t : ℝ) (x : E) (u : Unit) : (autonomous f g).F t x u = f t x

@[simp]

theorem ContinuousSystem.autonomous_h {E : Type u_1} {Y : Type u_3} (f : ℝ → E → E) (g : ℝ → E → Y) (t : ℝ) (x : E) (u : Unit) : (autonomous f g).h t x u = g t x

def ContinuousSystem.IsAutonomous {E : Type u_1} {U : Type u_2} {Y : Type u_3} (s : ContinuousSystem E U Y) : Prop

The system is autonomous: its equations do not depend on the input.

Equations

• s.IsAutonomous = ∀ (t : ℝ) (x : E) (u u' : U), s.F t x u = s.F t x u' ∧ s.h t x u = s.h t x u'

theorem ContinuousSystem.isAutonomous_autonomous {E : Type u_1} {Y : Type u_3} (f : ℝ → E → E) (g : ℝ → E → Y) : (autonomous f g).IsAutonomous

A system built by autonomous is autonomous.

theorem ContinuousSystem.IsAutonomous.exists_eq {E : Type u_1} {U : Type u_2} {Y : Type u_3} [Nonempty U] {s : ContinuousSystem E U Y} (hs : s.IsAutonomous) : ∃ (f : ℝ → E → E) (g : ℝ → E → Y), ∀ (t : ℝ) (x : E) (u : U), s.F t x u = f t x ∧ s.h t x u = g t x

An autonomous system is input-free data in disguise: its equations are those of some f and g that do not take an input. It equals autonomous f g only up to the input space, which is U rather than Unit.

Semantics

def ContinuousSystem.vectorField {E : Type u_1} {U : Type u_2} {Y : Type u_3} (s : ContinuousSystem E U Y) (u : ℝ → U) : ℝ → E → E

The right-hand side of the state equation under the input signal u, (t, x) ↦ F(t, x, u(t)): a time-dependent vector field on the state space, the shape the ODE machinery consumes.

Equations

• s.vectorField u t x = s.F t x (u t)

def ContinuousSystem.outputMap {E : Type u_1} {U : Type u_2} {Y : Type u_3} (s : ContinuousSystem E U Y) (u : ℝ → U) : ℝ → E → Y

The output equation under the input signal u, (t, x) ↦ h(t, x, u(t)).

Equations

• s.outputMap u t x = s.h t x (u t)

@[simp]

theorem ContinuousSystem.vectorField_apply {E : Type u_1} {U : Type u_2} {Y : Type u_3} (s : ContinuousSystem E U Y) (u : ℝ → U) (t : ℝ) (x : E) : s.vectorField u t x = s.F t x (u t)

@[simp]

theorem ContinuousSystem.outputMap_apply {E : Type u_1} {U : Type u_2} {Y : Type u_3} (s : ContinuousSystem E U Y) (u : ℝ → U) (t : ℝ) (x : E) : s.outputMap u t x = s.h t x (u t)

def ContinuousSystem.IsTrajectoryOn {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) (x : ℝ → E) (I : Set ℝ) : Prop

x is a trajectory of s under the input u on the set I: ẋ(t) = F(t, x(t), u(t)) for every t ∈ I, the derivative taken within I.

Stated on a set rather than on all of ℝ, because a map can satisfy the equation on an interval without being defined for all time. Which set — a segment [t₀, t₁] or a ray [t₀, ∞) — is chosen by the notions built on this one, not here. The output is s.outputMap u t (x t); it is not part of this predicate, because the output equation constrains nothing about x.

Equations

• s.IsTrajectoryOn u x I = IsIntegralCurveOn x (s.vectorField u) I

def ContinuousSystem.IsTrajectory {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) (x : ℝ → E) : Prop

x is a trajectory of s under the input u for all time.

Equations

• s.IsTrajectory u x = IsIntegralCurve x (s.vectorField u)

theorem ContinuousSystem.isTrajectoryOn_univ {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : ContinuousSystem E U Y} {u : ℝ → U} {x : ℝ → E} : s.IsTrajectoryOn u x Set.univ ↔ s.IsTrajectory u x

theorem ContinuousSystem.IsTrajectory.isTrajectoryOn {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : ContinuousSystem E U Y} {u : ℝ → U} {x : ℝ → E} (h : s.IsTrajectory u x) (I : Set ℝ) : s.IsTrajectoryOn u x I

The derivative of a function along the system

noncomputable def ContinuousSystem.lieDerivative {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (V : ℝ → E → ℝ) (t : ℝ) (x : E) (u : U) : ℝ

The derivative of V(t, x) along the system at the input value u, ∂V/∂t + ∂V/∂x · F(t, x, u): the rate of change of V along a trajectory through x at time t while the input takes the value u. It is the Lie derivative (_root_.lieDerivative) of V along the field F(·, ·, u), so the lemmas of Analysis.LieDerivative apply to it directly: a trajectory is an integral curve of s.vectorField. Input-free notions such as Lyapunov stability use u = (); input-to-state notions use a general u.

Equations

• s.lieDerivative V t x u = lieDerivative V (fun (t : ℝ) (x : E) => s.F t x u) t x

Well-posedness

def ContinuousSystem.IsForwardCompleteOn {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) (t₀ : ℝ) (S : Set E) : Prop

Every solution segment starting at time t₀ in the set S extends to a solution on [t₀, ∞): such solutions do not escape in finite time.

Forward completeness is kept apart from the notions that need it. Statements about limits as t → ∞ quantify over solutions on [t₀, ∞), and without it a solution that escapes in finite time would be silently left out of them.

Equations

• One or more equations did not get rendered due to their size.

def ContinuousSystem.IsForwardComplete {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) : Prop

Every solution segment, from any initial time and state, extends to a solution on [t₀, ∞).

Equations

• s.IsForwardComplete u = ∀ (t₀ : ℝ), s.IsForwardCompleteOn u t₀ Set.univ

def ContinuousSystem.HasUniqueSolutions {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) : Prop

Solutions are unique forward in time: two solution segments on [t₀, t₁] that agree at t₀ agree on the whole segment.

Kept apart from the stability notions, which quantify over every solution and so need no uniqueness: theorems that use it assume it.

Equations

• s.HasUniqueSolutions u = ∀ (t₀ t₁ : ℝ) (x y : ℝ → E), s.IsTrajectoryOn u x (Set.Icc t₀ t₁) → s.IsTrajectoryOn u y (Set.Icc t₀ t₁) → x t₀ = y t₀ → Set.EqOn x y (Set.Icc t₀ t₁)

theorem ContinuousSystem.hasUniqueSolutions_of_lipschitz {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : ContinuousSystem E U Y} {u : ℝ → U} {K : NNReal} (hL : ∀ (t : ℝ), LipschitzWith K (s.vectorField u t)) : s.HasUniqueSolutions u

Lipschitz right-hand sides have unique solutions. If x ↦ F(t, x, u(t)) is K-Lipschitz for every t, solutions are unique forward in time.

theorem ContinuousSystem.isForwardComplete_of_lipschitz {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {s : ContinuousSystem E U Y} {u : ℝ → U} {K : NNReal} (hF : Continuous (Function.uncurry (s.vectorField u))) (hL : ∀ (t : ℝ), LipschitzWith K (s.vectorField u t)) : s.IsForwardComplete u

Globally Lipschitz systems are forward complete. If (t, x) ↦ F(t, x, u(t)) is continuous and K-Lipschitz in x uniformly in t, every trajectory segment extends to [t₀, ∞).

Global Lipschitz is what rules out escape in finite time here; a local Lipschitz condition alone does not (ẋ = x²).

Invariance

def ContinuousSystem.IsForwardInvariant {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) (S : Set E) : Prop

S is forward invariant (positively invariant) under the input u: every trajectory segment that starts in S stays in S for as long as it is defined. This is for the one input signal u; robust and controlled invariance quantify over u.

Stated on segments [t₀, t₁] and for every initial time, so it constrains solutions that escape in finite time up to their escape, and it makes sense for time-varying systems.

Equations

• s.IsForwardInvariant u S = ∀ (t₀ t₁ : ℝ) (x : ℝ → E), s.IsTrajectoryOn u x (Set.Icc t₀ t₁) → x t₀ ∈ S → ∀ t ∈ Set.Icc t₀ t₁, x t ∈ S

The unforced system

def ContinuousSystem.zeroInput {E : Type u_1} {U : Type u_2} {Y : Type u_3} [Zero U] (s : ContinuousSystem E U Y) : ContinuousSystem E Unit Y

The unforced system: the input held at 0, as an autonomous system ẋ = F(t, x, 0), y = h(t, x, 0). Stability of a system with input is stability of this system; input–output notions such as input-to-state stability are stated on the system itself.

Equations

• s.zeroInput = ContinuousSystem.autonomous (fun (t : ℝ) (x : E) => s.F t x 0) fun (t : ℝ) (x : E) => s.h t x 0

@[simp]

theorem ContinuousSystem.zeroInput_F {E : Type u_1} {U : Type u_2} {Y : Type u_3} [Zero U] (s : ContinuousSystem E U Y) (t : ℝ) (x : E) (v : Unit) : s.zeroInput.F t x v = s.F t x 0

@[simp]

theorem ContinuousSystem.zeroInput_h {E : Type u_1} {U : Type u_2} {Y : Type u_3} [Zero U] (s : ContinuousSystem E U Y) (t : ℝ) (x : E) (v : Unit) : s.zeroInput.h t x v = s.h t x 0

theorem ContinuousSystem.isAutonomous_zeroInput {E : Type u_1} {U : Type u_2} {Y : Type u_3} [Zero U] (s : ContinuousSystem E U Y) : s.zeroInput.IsAutonomous

The unforced system is autonomous.

theorem ContinuousSystem.zeroInput_isTrajectoryOn_iff {E : Type u_1} {U : Type u_2} {Y : Type u_3} [Zero U] [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) {x : ℝ → E} {I : Set ℝ} : s.zeroInput.IsTrajectoryOn (fun (x : ℝ) => ()) x I ↔ s.IsTrajectoryOn 0 x I

The trajectories of the unforced system are those of the system under the zero input.

Carathéodory trajectories

def ContinuousSystem.IsCaratheodoryTrajectoryOn {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) (x : ℝ → E) (I : Set ℝ) : Prop

x is a Carathéodory trajectory of s under the input u on the set I: between any two times a ≤ b in I, the map τ ↦ F(τ, x(τ), u(τ)) is integrable and x(b) - x(a) = ∫ₐᵇ F(τ, x(τ), u(τ)) dτ.

This is the integral form of IsTrajectoryOn. It does not ask x to be differentiable, so it admits the solutions produced by discontinuous inputs (piecewise-constant, sampled-data, bang-bang, or merely measurable and bounded), which have corners where the input jumps and are not classical trajectories. Input-driven notions such as input-to-state stability need this form. When τ ↦ F(τ, x(τ), u(τ)) is continuous the two notions agree on every interval (isCaratheodoryTrajectoryOn_iff_isTrajectoryOn).

Because the equation links every pair of points of I, there is no vacuity at isolated points: on {0, 1} it ties x 1 to x 0, and on a singleton it says nothing, which is correct.

Completeness of E is required: without it the Bochner integral is 0 by convention, and the definition would silently say that x is constant.

Equations

• One or more equations did not get rendered due to their size.

def ContinuousSystem.IsCaratheodoryTrajectory {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] (s : ContinuousSystem E U Y) (u : ℝ → U) (x : ℝ → E) : Prop

x is a Carathéodory trajectory of s under the input u for all time.

Equations

• s.IsCaratheodoryTrajectory u x = s.IsCaratheodoryTrajectoryOn u x Set.univ

theorem ContinuousSystem.IsCaratheodoryTrajectoryOn.mono {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] {s : ContinuousSystem E U Y} {u : ℝ → U} {x : ℝ → E} {I J : Set ℝ} (h : s.IsCaratheodoryTrajectoryOn u x I) (hJI : J ⊆ I) : s.IsCaratheodoryTrajectoryOn u x J

theorem ContinuousSystem.isCaratheodoryTrajectoryOn_Icc_iff {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {s : ContinuousSystem E U Y} {u : ℝ → U} {x : ℝ → E} {t₀ t₁ : ℝ} (hle : t₀ ≤ t₁) (hg : ContinuousOn (fun (τ : ℝ) => s.vectorField u τ (x τ)) (Set.Icc t₀ t₁)) : s.IsCaratheodoryTrajectoryOn u x (Set.Icc t₀ t₁) ↔ s.IsTrajectoryOn u x (Set.Icc t₀ t₁)

On a segment, the integral and derivative forms agree when τ ↦ F(τ, x(τ), u(τ)) is continuous there.

theorem ContinuousSystem.isCaratheodoryTrajectoryOn_iff_isTrajectoryOn {E : Type u_1} {U : Type u_2} {Y : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {s : ContinuousSystem E U Y} {u : ℝ → U} {x : ℝ → E} {I : Set ℝ} (hI : I.OrdConnected) (hg : ContinuousOn (fun (τ : ℝ) => s.vectorField u τ (x τ)) I) : s.IsCaratheodoryTrajectoryOn u x I ↔ s.IsTrajectoryOn u x I

On any interval, the integral and derivative forms agree when τ ↦ F(τ, x(τ), u(τ)) is continuous there.

The interval may be closed, open, half-open, a ray, all of ℝ, or a single point. Order-connectedness is exactly what is needed: the integral form integrates along [a, b] ⊆ I, while the derivative form only looks near each point, and on a set with a gap the two differ.