Abstract linear control systems (Section 1 and § 2.1 of the paper)

• ALCS 𝕜 X U p : Definition 1.1, an abstract linear control system (𝕋, Φ).
• ALCS.IsZeroClass : Definition 1.4, zero-class systems.
• ALCS.Phi_zero : Φ_0 = 0 (§ 1.2).
• ALCS.norm_Phi_mono : equation eq:Phi-monotone, κ(t) ≤ κ(t + τ), where κ(t) = ‖Φ t‖.
• ALCS.causality, ALCS.delay, ALCS.free : Lemma 2.1 (lem:Phi-properties), equations eq:causality, eq:delay, eq:free.

Formalization choices

• Scalars: any nontrivially normed field 𝕜 here; the main theorem uses ℝ or ℂ (RCLike 𝕜). Completeness of X and U is assumed only where it is used.
• L^p(ℝ₊; U) is Lp U p muPlus (see ALCS/Background/Lp.lean).
• Like the semigroup T, the input maps form a function Φ : ℝ → (L^p →L X); only nonnegative times play a role in the axioms and in the results.
• Instead of constructing u ⋄_τ v as an element of L^p, the composition property is required for every w ∈ L^p whose representative is a.e. equal to concat τ ⇑u ⇑v. Since u ⋄_τ v does belong to L^p and a.e. classes are unique, this is exactly the identity of the paper.

structure AbstractLinearControl.ALCS (𝕜 : Type u_4) (X : Type u_5) (U : Type u_6) [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup U] [NormedSpace 𝕜 U] (p : ENNReal) [Fact (1 ≤ p)] extends AbstractLinearControl.C0Semigroup 𝕜 X : Type (max u_5 u_6)

Definition 1.1 (abstract linear control system). An abstract linear control system with state space X, input space U and exponent p ∈ [1, ∞] is a strongly continuous semigroup T on X (the parent structure C0Semigroup) together with bounded linear input maps Φ t : L^p(ℝ₊; U) → X satisfying the composition property eq:composition.

• T : ℝ → X →L[𝕜] X
• T_zero : self.T 0 = ContinuousLinearMap.id 𝕜 X
• T_add (t s : ℝ) : 0 ≤ t → 0 ≤ s → self.T (t + s) = self.T t ∘SL self.T s
• T_cont (y : X) : Filter.Tendsto (fun (t : ℝ) => (self.T t) y) (nhdsWithin 0 (Set.Ici 0)) (nhds y)
• Φ : ℝ → ↥(MeasureTheory.Lp U p muPlus) →L[𝕜] X

  the input maps Φ t : L^p(ℝ₊; U) → X

• composition (τ t : ℝ) : 0 ≤ τ → 0 ≤ t → ∀ (u v w : ↥(MeasureTheory.Lp U p muPlus)), ↑↑w =ᵐ[muPlus] concat τ ↑↑u ↑↑v → (self.Φ (τ + t)) w = (self.T t) ((self.Φ τ) u) + (self.Φ t) v

  composition property eq:composition: Φ (τ + t) (u ⋄_τ v) = T t (Φ τ u) + Φ t v, where w is any input representing u ⋄_τ v

def AbstractLinearControl.ALCS.IsZeroClass {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] {p : ENNReal} [Fact (1 ≤ p)] (S : ALCS 𝕜 X U p) : Prop

Definition 1.4 (zero-class system): κ(t) = ‖Φ t‖ → 0 as t → 0⁺ (equation eq:kappa-0).

Equations

• S.IsZeroClass = Filter.Tendsto (fun (t : ℝ) => ‖S.Φ t‖) (nhdsWithin 0 (Set.Ici 0)) (nhds 0)

Elementary consequences of the composition property (§ 1.2 and Lemma 2.1)

theorem AbstractLinearControl.ALCS.Phi_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] {p : ENNReal} [Fact (1 ≤ p)] (S : ALCS 𝕜 X U p) : S.Φ 0 = 0

Φ 0 = 0 (§ 1.2): composition with τ = t = 0 and u = v, since u ⋄_0 u = u.

theorem AbstractLinearControl.ALCS.causality {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] {p : ENNReal} [Fact (1 ≤ p)] (S : ALCS 𝕜 X U p) (τ : ℝ) (hτ : 0 ≤ τ) (u v w : ↥(MeasureTheory.Lp U p muPlus)) (hw : ↑↑w =ᵐ[muPlus] concat τ ↑↑u ↑↑v) : (S.Φ τ) w = (S.Φ τ) u

Lemma 2.1 (lem:Phi-properties), causality eq:causality: Φ τ (u ⋄_τ v) = Φ τ u, i.e. Φ τ u only depends on the restriction of u to [0, τ). (Composition with t = 0.)

theorem AbstractLinearControl.ALCS.delay {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] {p : ENNReal} [Fact (1 ≤ p)] (S : ALCS 𝕜 X U p) (s t : ℝ) (hs : 0 ≤ s) (ht : 0 ≤ t) (v w : ↥(MeasureTheory.Lp U p muPlus)) (hw : ↑↑w =ᵐ[muPlus] concat s ↑↑0 ↑↑v) : (S.Φ (s + t)) w = (S.Φ t) v

Lemma 2.1 (lem:Phi-properties), delay eq:delay: Φ (s + t) (0 ⋄_s v) = Φ t v, i.e. an initial period of zero input has no effect. (Composition with u = 0.)

theorem AbstractLinearControl.ALCS.free {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] {p : ENNReal} [Fact (1 ≤ p)] (S : ALCS 𝕜 X U p) (τ t : ℝ) (hτ : 0 ≤ τ) (ht : 0 ≤ t) (u w : ↥(MeasureTheory.Lp U p muPlus)) (hw : ↑↑w =ᵐ[muPlus] concat τ ↑↑u ↑↑0) : (S.Φ (τ + t)) w = (S.T t) ((S.Φ τ) u)

Lemma 2.1 (lem:Phi-properties), free evolution eq:free: Φ (τ + t) (u ⋄_τ 0) = T t (Φ τ u), i.e. once the input is switched off, the state evolves freely. (Composition with v = 0.)

theorem AbstractLinearControl.ALCS.norm_Phi_mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] {p : ENNReal} [Fact (1 ≤ p)] (S : ALCS 𝕜 X U p) {s t : ℝ} (hs : 0 ≤ s) (hst : s ≤ t) : ‖S.Φ s‖ ≤ ‖S.Φ t‖

Monotonicity of κ(t) = ‖Φ t‖, equation eq:Phi-monotone: ‖Φ s‖ ≤ ‖Φ t‖ for 0 ≤ s ≤ t. Indeed Φ s u = Φ t (0 ⋄_{t-s} u) by delay.