Nonlinear dynamical systems & control theory

2. Basics🔗

In this section, we collect definitions and results needed for the abstract treatment of dynamical systems, which are not yet in mathlib. The previous section was concerned with properties of differential equations, but here we take the view that a

2.1. Local Lp spaces🔗

🔗def
MeasureTheory.MemLpLoc.{u_1, u_4} {α : Type u_1} {E : Type u_4}
  {m : MeasurableSpace α} [NormedAddCommGroup E] [Bornology α]
  (u : α → E) (p : ENNReal)
  (μ : MeasureTheory.Measure α := by volume_tac) : Prop
MeasureTheory.MemLpLoc.{u_1, u_4}
  {α : Type u_1} {E : Type u_4}
  {m : MeasurableSpace α}
  [NormedAddCommGroup E] [Bornology α]
  (u : α → E) (p : ENNReal)
  (μ : MeasureTheory.Measure α := by
    volume_tac) :
  Prop

A function u is locally in Lp if for every bounded measurable set s, u is in Lp with respect to measure μ restricted to s.

2.2. Abstract solution operators🔗

For autonomous equations, the solution operator can be represented using Flow as a map ℝ → E → E. For non-autonomous systems, the solution operator is not time-covariant, therefore one has to take the initial time into account. We prove a bundled map

🔗structure
NonautonomousFlow.{u_1, u_2} (τ : Type u_1) (E : Type u_2) :
  Type (max u_1 u_2)
NonautonomousFlow.{u_1, u_2}
  (τ : Type u_1) (E : Type u_2) :
  Type (max u_1 u_2)

A non-autonomous flow is a map u from τ × τ × E to E such that u t₀ t₀ x = x and u t₀ t₁ (u t₁ t₂ x) = u t₀ t₂ x.

We do not impose any continuity property.

Constructor

NonautonomousFlow.mk.{u_1, u_2}

Fields

toFun : τ → τ → E → E

The underlying map

map_id : ∀ (t₀ : τ) (x : E), self.toFun t₀ t₀ x = x

Consistency: the solution operator acts as the identity at initial time

map_comp : ∀ (t₀ t₁ t₂ : τ) (x : E), self.toFun t₀ t₁ (self.toFun t₁ t₂ x) = self.toFun t₀ t₂ x

Semigroup property: the solution operator satisfies Φ t₀ t₁ (Φ t₁ t₂ x) = Φ t₀ t₂ x

Note that this does not automatically imply Flow in the autonomous case, because we do not assume continuity here.

2.3. Comparison functions🔗

🔗structure
MemK (f : NNReal → NNReal) : Prop
MemK (f : NNReal → NNReal) : Prop

A function of class K.

Constructor

MemK.mk

Fields

cont : Continuous f

The function f is continuous.

strictMono : StrictMono f

The function f is strictly increasing.

zero : f 0 = 0

The functionf maps 0 to 0.

🔗structure
MemKOn (f : NNReal → NNReal) (a : NNReal) : Prop
MemKOn (f : NNReal → NNReal)
  (a : NNReal) : Prop

A function of class K.

Constructor

MemKOn.mk

Fields

contOn : ContinuousOn f (Set.Icc 0 a)

The function f is continuous on the interval [0, a].

strictMonoOn : StrictMonoOn f (Set.Icc 0 a)

The function f is strictly increasing on the interval [0, a].

zero : f 0 = 0

The functionf maps 0 to 0.