4.3. Stability🔗

We have two notions of stability, Lp-stability and finite gain stability.

A nonlinear operator f is called Lp stable if for every u : Lp the output is again in Lp. We use unbundled Lp functions using MemLp.

structure

SetRel.IsLpStable.{u_2, u_3, u_4} {α : Type u_2} {E : Type u_3}
  {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F]
  [MeasurableSpace α] (f : SetRel (α → E) (α → F)) (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop
SetRel.IsLpStable.{u_2, u_3, u_4}
  {α : Type u_2} {E : Type u_3}
  {F : Type u_4} [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [MeasurableSpace α]
  (f : SetRel (α → E) (α → F))
  (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop

A relation is called Lp-stable if it maps Lp to Lp.

Constructor

SetRel.IsLpStable.mk.{u_2, u_3, u_4}

Fields

memLp : ∀ ⦃u : α → E⦄, MeasureTheory.MemLp u p μ → ∀ (y : α → F), (u, y) ∈ f → MeasureTheory.MemLp y p μ

For every pair (u, y) ∈ f if u is in Lp then y is also in Lp.

structure

Function.IsLpStable.{u_2, u_3, u_4} {α : Type u_2} {E : Type u_3}
  {F : Type u_4} [NormedAddCommGroup E] [NormedAddCommGroup F]
  [MeasurableSpace α] (f : (α → E) → α → F) (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop
Function.IsLpStable.{u_2, u_3, u_4}
  {α : Type u_2} {E : Type u_3}
  {F : Type u_4} [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [MeasurableSpace α]
  (f : (α → E) → α → F) (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop

A map is called Lp-stable if it maps Lp to Lp.

Constructor

Function.IsLpStable.mk.{u_2, u_3, u_4}

Fields

memLp : ∀ ⦃u : α → E⦄, MeasureTheory.MemLp u p μ → MeasureTheory.MemLp (f u) p μ

Every u in Lp gets mapped to Lp.

The second notion is finite gain stability. A map f is finite gain stable if there exist k and β such that ‖(f u)ₜ‖ ≤ k * ‖uₜ‖ + β for all local Lp functions u.

def

SetRel.IsFiniteGainStableWith.{u_1, u_2, u_3, u_4} {ι : Type u_1}
  {α : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E]
  [NormedAddCommGroup F] [MeasurableSpace α] [Bornology α]
  (f : SetRel (α → E) (α → F)) (k β : NNReal) (s : ι → Set α)
  (p : ENNReal) (μ : MeasureTheory.Measure α) : Prop
SetRel.IsFiniteGainStableWith.{u_1, u_2,
    u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [MeasurableSpace α] [Bornology α]
  (f : SetRel (α → E) (α → F))
  (k β : NNReal) (s : ι → Set α)
  (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop

A map is called finite gain stable with gain less than k if there exists β such that for all local Lp functions u, we have the Lp-norm estimate ‖(f u)ₜ‖ ≤ k * ‖uₜ‖ + β.

Version for relations.

structure

Function.IsFiniteGainStableWith.{u_1, u_2, u_3, u_4} {ι : Type u_1}
  {α : Type u_2} {E : Type u_3} {F : Type u_4} [NormedAddCommGroup E]
  [NormedAddCommGroup F] [MeasurableSpace α] [Bornology α]
  (f : (α → E) → α → F) (k β : NNReal) (s : ι → Set α) (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop
Function.IsFiniteGainStableWith.{u_1, u_2,
    u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [MeasurableSpace α] [Bornology α]
  (f : (α → E) → α → F) (k β : NNReal)
  (s : ι → Set α) (p : ENNReal)
  (μ : MeasureTheory.Measure α) : Prop

A map is called finite gain stable with gain less than k if there exists β such that for all local Lp functions u, we have the Lp-norm estimate ‖(f u)ₜ‖ ≤ k * ‖uₜ‖ + β.

Constructor

Function.IsFiniteGainStableWith.mk.{u_1, u_2, u_3, u_4}

Fields

memLpLoc : ∀ ⦃u : α → E⦄, MeasureTheory.MemLpLoc u p μ → MeasureTheory.MemLpLoc (f u) p μ

Every u in Lp gets mapped to Lp.

stableWith : ∀ (t : ι) (u : α → E),
  MeasureTheory.MemLpLoc u p μ →
    MeasureTheory.eLpNorm (f u) p (μ.restrict (s t)) ≤ ↑k * MeasureTheory.eLpNorm u p (μ.restrict (s t)) + ↑β

For every u in LpLoc, we have ‖yₜ‖ ≤ k * ‖(f u)ₜ‖ + β.

It can easily be shown that every finite gain stable system is Lp stable

theorem

Function.IsFiniteGainStableWith.isLpStable.{u_1, u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E] [NormedAddCommGroup F] [MeasurableSpace α]
  [Bornology α] {f : (α → E) → α → F} {k β : NNReal} {s : ι → Set α}
  {p : ENNReal} {μ : MeasureTheory.Measure α} [Preorder ι] [Countable ι]
  [Nonempty ι] [IsDirectedOrder ι]
  (hf : Function.IsFiniteGainStableWith f k β s p μ)
  (hfu :
    ∀ (u : α → E),
      MeasureTheory.MemLp u p μ →
        MeasureTheory.AEStronglyMeasurable (f u) μ)
  (hs : MeasureTheory.AECover μ Filter.atTop s) :
  Function.IsLpStable f p μ
Function.IsFiniteGainStableWith.isLpStable.{u_1,
    u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [MeasurableSpace α] [Bornology α]
  {f : (α → E) → α → F} {k β : NNReal}
  {s : ι → Set α} {p : ENNReal}
  {μ : MeasureTheory.Measure α}
  [Preorder ι] [Countable ι] [Nonempty ι]
  [IsDirectedOrder ι]
  (hf :
    Function.IsFiniteGainStableWith f k β
      s p μ)
  (hfu :
    ∀ (u : α → E),
      MeasureTheory.MemLp u p μ →
        MeasureTheory.AEStronglyMeasurable
          (f u) μ)
  (hs :
    MeasureTheory.AECover μ Filter.atTop
      s) :
  Function.IsLpStable f p μ

Every finite gain stable system is Lp stable.

and every causal system that satisfies for every u : L^p$ the estimate ‖f u‖ ≤ k * ‖u‖ + β is finite gain stable:

theorem

Function.IsCausal.isFiniteGainStableWith.{u_1, u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E] [NormedAddCommGroup F] [MeasurableSpace α]
  [Bornology α] {f : (α → E) → α → F} {s : ι → Set α} {p : ENNReal}
  {μ : MeasureTheory.Measure α} (hf : Function.IsCausal f s p μ)
  (k β : NNReal)
  (hs : ∀ (t : ι), MeasurableSet (s t) ∧ Bornology.IsBounded (s t))
  (h :
    ∀ (u : α → E),
      MeasureTheory.MemLp u p μ →
        MeasureTheory.eLpNorm (f u) p μ ≤
          ↑k * MeasureTheory.eLpNorm u p μ + ↑β) :
  Function.IsFiniteGainStableWith f k β s p μ
Function.IsCausal.isFiniteGainStableWith.{u_1,
    u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [MeasurableSpace α] [Bornology α]
  {f : (α → E) → α → F} {s : ι → Set α}
  {p : ENNReal}
  {μ : MeasureTheory.Measure α}
  (hf : Function.IsCausal f s p μ)
  (k β : NNReal)
  (hs :
    ∀ (t : ι),
      MeasurableSet (s t) ∧
        Bornology.IsBounded (s t))
  (h :
    ∀ (u : α → E),
      MeasureTheory.MemLp u p μ →
        MeasureTheory.eLpNorm (f u) p μ ≤
          ↑k *
              MeasureTheory.eLpNorm u p
                μ +
            ↑β) :
  Function.IsFiniteGainStableWith f k β s
    p μ

Every system that is causal and satisfies the finite gain estimate is for Lp functions is finite gain stable.

Proposition 1.2.3 in van der Schaft.

Moreover, it is easy to see that the composition of two finite gain stable systems is again finite gain stable:

theorem

Function.IsFiniteGainStableWith.comp.{u_1, u_2, u_3, u_4, u_5}
  {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4}
  {G : Type u_5} [NormedAddCommGroup E] [NormedAddCommGroup F]
  [NormedAddCommGroup G] [MeasurableSpace α] [Bornology α]
  {f : (α → E) → α → F} {g : (α → F) → α → G} {k k' β β' : NNReal}
  {s : ι → Set α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  (hg : Function.IsFiniteGainStableWith g k' β' s p μ)
  (hf : Function.IsFiniteGainStableWith f k β s p μ) :
  Function.IsFiniteGainStableWith (g ∘ f) (k * k') (β * k' + β') s p μ
Function.IsFiniteGainStableWith.comp.{u_1,
    u_2, u_3, u_4, u_5}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  {G : Type u_5} [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  [NormedAddCommGroup G]
  [MeasurableSpace α] [Bornology α]
  {f : (α → E) → α → F}
  {g : (α → F) → α → G}
  {k k' β β' : NNReal} {s : ι → Set α}
  {p : ENNReal}
  {μ : MeasureTheory.Measure α}
  (hg :
    Function.IsFiniteGainStableWith g k'
      β' s p μ)
  (hf :
    Function.IsFiniteGainStableWith f k β
      s p μ) :
  Function.IsFiniteGainStableWith (g ∘ f)
    (k * k') (β * k' + β') s p μ

The composition of two finite gain stable maps is finite gain stable.

4.3.1. Feedback systems and small-gain theorems🔗

We now consider the negative feedback connection of two maps f₁ : (α → E) → (α → F) and f₂ : (α → F) → (α → E). The feedback connection is given by the equations \begin{aligned} u₁ &= e₁ - y₂\,,\\ u₂ &= e₂ + y₁\,,\\ y₁ &= f₁(u₁)\,,\\ y₂ &= f₂(u₂)\,. \end{aligned} These equations determine two relations, the relation SetRel.closedLoop.inputState mapping e to u and the relation SetRel.closedLoop.inputOutput mapping e to y.

In general, these relations do not define maps, but in all practical situations this is the case and it can usually proved directly.

The well-known small-gain theorem asserts that if f₁ and f₂ are finite gain stable and the product of the gains is less than one, then the feedback connection is finite gain stable as well.

theorem

SetRel.closedLoop.inputStateLp_isFiniteGainStableWith.{u_1, u_2, u_3,
    u_4}
  {ι : Type u_1} {α : Type u_2} {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E] [NormedAddCommGroup F]
  {loop : SetRel.closedLoop α E F} [MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [Bornology α] {s : ι → Set α}
  {p : ENNReal} {k₁ k₂ β₁ β₂ : NNReal} [hp : Fact (1 ≤ p)] (hp' : p ≠ ⊤)
  {G₁ : (α → E) → α → F} (hG₁ : Function.graph G₁ = loop.topRel)
  (hG₁' : Function.IsFiniteGainStableWith G₁ k₁ β₁ s p μ)
  {G₂ : (α → F) → α → E} (hG₂ : Function.graph G₂ = loop.botRel)
  (hG₂' : Function.IsFiniteGainStableWith G₂ k₂ β₂ s p μ)
  (hk : k₁ * k₂ < 1)
  (ht : ∀ (t : ι), MeasurableSet (s t) ∧ Bornology.IsBounded (s t)) :
  (loop.inputStateLp p).IsFiniteGainStableWith
    (SetRel.closedLoop.inputStateLoopGainLp p.toReal k₁ k₂)
    (SetRel.closedLoop.loopBias k₁ k₂ β₁ β₂) s p μ
SetRel.closedLoop.inputStateLp_isFiniteGainStableWith.{u_1,
    u_2, u_3, u_4}
  {ι : Type u_1} {α : Type u_2}
  {E : Type u_3} {F : Type u_4}
  [NormedAddCommGroup E]
  [NormedAddCommGroup F]
  {loop : SetRel.closedLoop α E F}
  [MeasurableSpace α]
  {μ : MeasureTheory.Measure α}
  [Bornology α] {s : ι → Set α}
  {p : ENNReal} {k₁ k₂ β₁ β₂ : NNReal}
  [hp : Fact (1 ≤ p)] (hp' : p ≠ ⊤)
  {G₁ : (α → E) → α → F}
  (hG₁ : Function.graph G₁ = loop.topRel)
  (hG₁' :
    Function.IsFiniteGainStableWith G₁ k₁
      β₁ s p μ)
  {G₂ : (α → F) → α → E}
  (hG₂ : Function.graph G₂ = loop.botRel)
  (hG₂' :
    Function.IsFiniteGainStableWith G₂ k₂
      β₂ s p μ)
  (hk : k₁ * k₂ < 1)
  (ht :
    ∀ (t : ι),
      MeasurableSet (s t) ∧
        Bornology.IsBounded (s t)) :
  (loop.inputStateLp
        p).IsFiniteGainStableWith
    (SetRel.closedLoop.inputStateLoopGainLp
      p.toReal k₁ k₂)
    (SetRel.closedLoop.loopBias k₁ k₂ β₁
      β₂)
    s p μ

The small-gain theorem states that if two maps G₁ and G₂ are finite gain stable with gain less than k₁ and k₂, respectively, and k₁ * k₁ < 1, then the closed feedback loop is finite gain stable as well.

Version for the map from inputs to states.