Every L^∞ system is zero-class (Theorem 1.5)

Theorem 1.5 (thm:p-infty-zero-class). Let X, U be Banach spaces and (𝕋, Φ) an abstract linear control system with p = ∞. Then the system is of the zero-class, i.e. ‖Φ_t‖ → 0 as t → 0.

The final statement is ALCS.zero_class, at the end of this file. The auxiliary declarations live in the namespace ALCS.ZeroClassProof and follow § 2.3 of the paper:

• ell is the limit ℓ = lim_{t → 0⁺} κ(t) = inf_{t > 0} κ(t) (eq:ell), and norm_Phi_tendsto identifies it as the limit along any positive null sequence.
• Step 1, doubling: the doubling inequality eq:doubling, 2 ‖Φ_h u‖ ≤ κ(2h) + ‖(T_h - Id) Φ_h u‖ for ‖u‖ ≤ 1.
• Step 2, data, h, x: nearly extremal pulses u_n on rapidly decreasing time scales h_n, with states x_n = Φ_{h_n} u_n (eq:xn-extremal, eq:hn-fast).
• Step 3, packing, packedOperator: the pulses are packed into one bounded operator S : ℓ^∞ → X, and packedOperator_close is eq:Sen-xn.
• Step 4, x_moves_tendsto: Lemma 2.3 (Phillips.uniform) gives ‖(T_{h_n} - Id) x_n‖ → 0, which is the second half of eq:goal.

Difference with the paper in Step 3

The paper plays the pulses one after the other on consecutive intervals [s_n, s_{n+1}) and evaluates at the accumulated time H = Σ h_k. Here each pulse gets its own free-evolution time r_n ∈ (0, h_n], chosen in Step 2 so that ‖T_{r_n} x_n - x_n‖ ≤ 2^{-n}, and the n-th pulse is played on [1 - r_n - h_n, 1 - r_n), with zero input in the gaps; the operator is evaluated at time 1. Then S e_n = T_{r_n} x_n exactly. This changes the bookkeeping, not the argument. The scalar field is ℝ or ℂ (RCLike 𝕜), as required by Phillips' lemma.

Step 1: the doubling inequality

theorem AbstractLinearControl.ALCS.ZeroClassProof.doubling {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) {h : ℝ} (hh : 0 ≤ h) (u : ↥(MeasureTheory.Lp U ⊤ muPlus)) (hu : ‖u‖ ≤ 1) : 2 * ‖(S.Φ h) u‖ ≤ ‖S.Φ (2 * h)‖ + ‖(S.T h) ((S.Φ h) u) - (S.Φ h) u‖

Step 1, the doubling inequality eq:doubling: for h ≥ 0 and ‖u‖ ≤ 1, 2 ‖Φ_h u‖ ≤ κ(2h) + ‖T_h (Φ_h u) - Φ_h u‖, obtained by playing u twice in a row.

Step 2: nearly extremal pulses on rapidly decreasing time scales

theorem AbstractLinearControl.ALCS.ZeroClassProof.exists_near_extremal {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (h ε : ℝ) (hε : 0 < ε) : ∃ (u : ↥(MeasureTheory.Lp U ⊤ muPlus)), ‖u‖ ≤ 1 ∧ ‖S.Φ h‖ - ε ≤ ‖(S.Φ h) u‖

An input of norm at most one which almost realizes κ(h) = ‖Φ h‖.

structure AbstractLinearControl.ALCS.ZeroClassProof.Pulse (U : Type u_4) [NormedAddCommGroup U] (h : ℝ) : Type u_4

A pulse of length h: a control of norm at most one, given by an actual (everywhere defined) representative vanishing outside [0, h).

• f : ℝ → U

  the representative

• measurable : MeasureTheory.StronglyMeasurable self.f
• bound (t : ℝ) : ‖self.f t‖ ≤ 1
• off (t : ℝ) : t < 0 ∨ h ≤ t → self.f t = 0

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.Pulse.input {U : Type u_3} [NormedAddCommGroup U] {h : ℝ} (P : Pulse U h) : ↥(MeasureTheory.Lp U ⊤ muPlus)

The pulse, as an element of L^∞(ℝ₊; U).

Equations

• P.input = MeasureTheory.MemLp.toLp P.f ⋯

theorem AbstractLinearControl.ALCS.ZeroClassProof.Pulse.coe_input {U : Type u_3} [NormedAddCommGroup U] {h : ℝ} (P : Pulse U h) : ↑↑P.input =ᵐ[muPlus] P.f

theorem AbstractLinearControl.ALCS.ZeroClassProof.Pulse.norm_input {U : Type u_3} [NormedAddCommGroup U] {h : ℝ} (P : Pulse U h) : ‖P.input‖ ≤ 1

theorem AbstractLinearControl.ALCS.ZeroClassProof.Pulse.free_rep {U : Type u_3} [NormedAddCommGroup U] {h : ℝ} (P : Pulse U h) : ↑↑P.input =ᵐ[muPlus] concat h ↑↑P.input ↑↑0

A pulse of length h is switched off after time h: P = P ⋄_h 0.

theorem AbstractLinearControl.ALCS.ZeroClassProof.exists_pulse {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (h : ℝ) (hh : 0 ≤ h) (ε : ℝ) (hε : 0 < ε) : ∃ (P : Pulse U h), ‖S.Φ h‖ - ε ≤ ‖(S.Φ h) P.input‖

A nearly extremal input can be chosen to be a pulse (by causality eq:causality, truncating it at time h does not change Φ_h u).

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.err (n : ℕ) : ℝ

The accuracy 2^{-n} of the n-th selection.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.err n = (1 / 2) ^ n

theorem AbstractLinearControl.ALCS.ZeroClassProof.err_pos (n : ℕ) : 0 < err n

theorem AbstractLinearControl.ALCS.ZeroClassProof.err_tendsto : Filter.Tendsto err Filter.atTop (nhds 0)

structure AbstractLinearControl.ALCS.ZeroClassProof.FrozenPulse {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) (h : ℝ) : Type u_3

The data selected at step n of Step 2: a nearly extremal pulse of length h (eq:xn-extremal), and a free-evolution time r ∈ (0, h] during which its state is essentially frozen by the semigroup (the analogue of eq:hn-fast).

• pulse : Pulse U h

  The bounded input pulse whose output nearly attains the operator norm.

• near : ‖S.Φ h‖ - err n ≤ ‖(S.Φ h) self.pulse.input‖
• r : ℝ

  the free-evolution time

• r_pos : 0 < self.r
• r_le : self.r ≤ h
• close : ‖(S.T self.r) ((S.Φ h) self.pulse.input) - (S.Φ h) self.pulse.input‖ ≤ err n

theorem AbstractLinearControl.ALCS.ZeroClassProof.frozenPulse_nonempty {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) (h : ℝ) (hh : 0 < h) : Nonempty (FrozenPulse S n h)

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.choosePulse {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) (h : ℝ) (hh : 0 < h) : FrozenPulse S n h

Classical choice is used only to choose actual witnesses to proved existences.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.choosePulse S n h hh = Classical.choice ⋯

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.positiveTimes {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : ℕ → { h : ℝ // 0 < h }

The time scales, defined recursively: h 0 = 1/4 and h (n + 1) = r n / 4, so that the next pulse fits inside the free-evolution interval of the previous one.

Equations

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

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.h {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : ℝ

The time scale h_n.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.h S n = ↑(AbstractLinearControl.ALCS.ZeroClassProof.positiveTimes S n)

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.data {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : FrozenPulse S n (h S n)

The pulse u_n and the free-evolution time r_n selected at step n.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.data S n = AbstractLinearControl.ALCS.ZeroClassProof.choosePulse S n (AbstractLinearControl.ALCS.ZeroClassProof.h S n) ⋯

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.r {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : ℝ

The free-evolution time r_n ∈ (0, h_n].

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.r S n = (AbstractLinearControl.ALCS.ZeroClassProof.data S n).r

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.x {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : X

The state x_n = Φ_{h_n} u_n.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.x S n = (S.Φ (AbstractLinearControl.ALCS.ZeroClassProof.h S n)) (AbstractLinearControl.ALCS.ZeroClassProof.data S n).pulse.input

theorem AbstractLinearControl.ALCS.ZeroClassProof.h_pos {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : 0 < h S n

theorem AbstractLinearControl.ALCS.ZeroClassProof.r_pos {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : 0 < r S n

theorem AbstractLinearControl.ALCS.ZeroClassProof.r_le_h {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : r S n ≤ h S n

theorem AbstractLinearControl.ALCS.ZeroClassProof.h_zero {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : h S 0 = 1 / 4

theorem AbstractLinearControl.ALCS.ZeroClassProof.h_succ {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : h S (n + 1) = r S n / 4

theorem AbstractLinearControl.ALCS.ZeroClassProof.h_succ_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : h S (n + 1) ≤ h S n / 2

theorem AbstractLinearControl.ALCS.ZeroClassProof.h_le_quarter {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : h S n ≤ 1 / 4

theorem AbstractLinearControl.ALCS.ZeroClassProof.h_geometric {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : h S n ≤ err n / 4

theorem AbstractLinearControl.ALCS.ZeroClassProof.h_tendsto {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : Filter.Tendsto (h S) Filter.atTop (nhds 0)

theorem AbstractLinearControl.ALCS.ZeroClassProof.x_near {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : ‖S.Φ (h S n)‖ - err n ≤ ‖x S n‖

theorem AbstractLinearControl.ALCS.ZeroClassProof.x_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : ‖x S n‖ ≤ ‖S.Φ (h S n)‖

theorem AbstractLinearControl.ALCS.ZeroClassProof.x_frozen {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : ‖(S.T (r S n)) (x S n) - x S n‖ ≤ err n

Step 3: packing the pulses into one bounded operator ℓ^∞ → X

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.start {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : ℝ

The n-th pulse is played on window n = [start n, start n + h n), where start n = 1 - r n - h n. These windows are pairwise disjoint subsets of [0, 1).

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.start S n = 1 - AbstractLinearControl.ALCS.ZeroClassProof.r S n - AbstractLinearControl.ALCS.ZeroClassProof.h S n

def AbstractLinearControl.ALCS.ZeroClassProof.window {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : Set ℝ

The interval on which the n-th pulse is played.

Equations

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

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.block {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) (t : ℝ) : U

The n-th pulse, delayed so that it is played on window n.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.block S n t = (AbstractLinearControl.ALCS.ZeroClassProof.data S n).pulse.f (t - AbstractLinearControl.ALCS.ZeroClassProof.start S n)

theorem AbstractLinearControl.ALCS.ZeroClassProof.start_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : 0 ≤ start S n

theorem AbstractLinearControl.ALCS.ZeroClassProof.finish_le_next {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : start S n + h S n ≤ start S (n + 1)

theorem AbstractLinearControl.ALCS.ZeroClassProof.start_mono {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : Monotone (start S)

theorem AbstractLinearControl.ALCS.ZeroClassProof.finish_le_start {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) {i j : ℕ} (hij : i < j) : start S i + h S i ≤ start S j

theorem AbstractLinearControl.ALCS.ZeroClassProof.window_unique {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) {i j : ℕ} {t : ℝ} (hi : t ∈ window S i) (hj : t ∈ window S j) : i = j

theorem AbstractLinearControl.ALCS.ZeroClassProof.block_measurable {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : MeasureTheory.StronglyMeasurable (block S n)

theorem AbstractLinearControl.ALCS.ZeroClassProof.block_bound {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) (t : ℝ) : ‖block S n t‖ ≤ 1

theorem AbstractLinearControl.ALCS.ZeroClassProof.block_off {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) {t : ℝ} (ht : t ∉ window S n) : block S n t = 0

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.packRaw {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) : ℝ → U

The packed control u^α (raw function): on window n it is α_n times the n-th pulse, and it vanishes outside the windows.

Equations

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

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_on {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) {n : ℕ} {t : ℝ} (ht : t ∈ window S n) : packRaw S a t = a n • block S n t

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_off {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) {t : ℝ} (ht : ¬∃ (n : ℕ), t ∈ window S n) : packRaw S a t = 0

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_add {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a b : Phillips.Linfty 𝕜) (t : ℝ) : packRaw S (a + b) t = packRaw S a t + packRaw S b t

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_smul {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (c : 𝕜) (a : Phillips.Linfty 𝕜) (t : ℝ) : packRaw S (c • a) t = c • packRaw S a t

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_bound {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) (t : ℝ) : ‖packRaw S a t‖ ≤ ‖a‖

theorem AbstractLinearControl.ALCS.ZeroClassProof.partial_sums_eventually {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) (t : ℝ) : ∀ᶠ (N : ℕ) in Filter.atTop, ∑ n ∈ Finset.range N, a n • block S n t = packRaw S a t

At every time the partial sums eventually equal the glued function. This uses pointwise disjointness, not convergence of a series in the L-infinity norm.

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_measurable {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) : MeasureTheory.StronglyMeasurable (packRaw S a)

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_memLp {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) : MeasureTheory.MemLp (packRaw S a) ⊤ muPlus

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.packedInput {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) : ↥(MeasureTheory.Lp U ⊤ muPlus)

The packed control u^α ∈ L^∞(ℝ₊; U).

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.packedInput S a = MeasureTheory.MemLp.toLp (AbstractLinearControl.ALCS.ZeroClassProof.packRaw S a) ⋯

theorem AbstractLinearControl.ALCS.ZeroClassProof.packedInput_ae {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) : ↑↑(packedInput S a) =ᵐ[muPlus] packRaw S a

theorem AbstractLinearControl.ALCS.ZeroClassProof.packedInput_norm {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) : ‖packedInput S a‖ ≤ ‖a‖

theorem AbstractLinearControl.ALCS.ZeroClassProof.packedInput_add {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a b : Phillips.Linfty 𝕜) : packedInput S (a + b) = packedInput S a + packedInput S b

theorem AbstractLinearControl.ALCS.ZeroClassProof.packedInput_smul {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (c : 𝕜) (a : Phillips.Linfty 𝕜) : packedInput S (c • a) = c • packedInput S a

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.packing {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : Phillips.Linfty 𝕜 →L[𝕜] ↥(MeasureTheory.Lp U ⊤ muPlus)

The contraction α ↦ u^α from ℓ^∞ to L^∞(ℝ₊; U).

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.packing S = { toFun := AbstractLinearControl.ALCS.ZeroClassProof.packedInput S, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem AbstractLinearControl.ALCS.ZeroClassProof.packing_ae {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (a : Phillips.Linfty 𝕜) : ↑↑((packing S) a) =ᵐ[muPlus] packRaw S a

theorem AbstractLinearControl.ALCS.ZeroClassProof.packRaw_e {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) (t : ℝ) : packRaw S (Phillips.e n) t = block S n t

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.packedOperator {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : Phillips.Linfty 𝕜 →L[𝕜] X

The operator S : ℓ^∞ → X, S α = Φ_1 u^α.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.packedOperator S = S.Φ 1 ∘SL AbstractLinearControl.ALCS.ZeroClassProof.packing S

theorem AbstractLinearControl.ALCS.ZeroClassProof.packedOperator_e {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : (packedOperator S) (Phillips.e n) = (S.T (r S n)) (x S n)

S e_n = T_{r_n} x_n: the n-th state, after it has evolved freely during the time r_n (by eq:delay and then eq:free).

theorem AbstractLinearControl.ALCS.ZeroClassProof.packedOperator_close {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (n : ℕ) : ‖(packedOperator S) (Phillips.e n) - x S n‖ ≤ err n

‖S e_n - x_n‖ ≤ 2^{-n}, equation eq:Sen-xn.

The limit ℓ of κ(t) as t → 0⁺ (eq:ell)

def AbstractLinearControl.ALCS.ZeroClassProof.normRange {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : Set ℝ

The possible input-map norms at strictly positive times.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.normRange S = (fun (t : ℝ) => ‖S.Φ t‖) '' Set.Ioi 0

theorem AbstractLinearControl.ALCS.ZeroClassProof.normRange_nonempty {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : (normRange S).Nonempty

theorem AbstractLinearControl.ALCS.ZeroClassProof.normRange_bddBelow {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : BddBelow (normRange S)

noncomputable def AbstractLinearControl.ALCS.ZeroClassProof.ell {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : ℝ

ℓ = inf_{t > 0} κ(t), equation eq:ell.

Equations

• AbstractLinearControl.ALCS.ZeroClassProof.ell S = sInf (AbstractLinearControl.ALCS.ZeroClassProof.normRange S)

theorem AbstractLinearControl.ALCS.ZeroClassProof.ell_nonneg {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : 0 ≤ ell S

theorem AbstractLinearControl.ALCS.ZeroClassProof.ell_le {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (t : ℝ) (ht : 0 < t) : ell S ≤ ‖S.Φ t‖

theorem AbstractLinearControl.ALCS.ZeroClassProof.exists_norm_lt {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (ε : ℝ) (hε : 0 < ε) : ∃ (t : ℝ), 0 < t ∧ ‖S.Φ t‖ < ell S + ε

theorem AbstractLinearControl.ALCS.ZeroClassProof.norm_Phi_tendsto {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) (t : ℕ → ℝ) (htpos : ∀ (n : ℕ), 0 < t n) (ht : Filter.Tendsto t Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ‖S.Φ (t n)‖) Filter.atTop (nhds (ell S))

Monotonicity identifies the norm limit along every positive null sequence.

theorem AbstractLinearControl.ALCS.ZeroClassProof.x_norm_tendsto {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) : Filter.Tendsto (fun (n : ℕ) => ‖x S n‖) Filter.atTop (nhds (ell S))

First half of eq:goal: ‖x_n‖ → ℓ.

Step 4: conclusion with Lemma 2.3

theorem AbstractLinearControl.ALCS.ZeroClassProof.x_moves_tendsto {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] (S : ALCS 𝕜 X U ⊤) [CompleteSpace X] : Filter.Tendsto (fun (n : ℕ) => ‖(S.T (h S n)) (x S n) - x S n‖) Filter.atTop (nhds 0)

Second half of eq:goal: ‖T_{h_n} x_n - x_n‖ → 0. By Lemma 2.3 (Phillips.uniform), ‖(T_{h_n} - Id) S e_n‖ → 0, and S e_n is 2^{-n}-close to x_n.

theorem AbstractLinearControl.ALCS.zero_class {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} [NormedAddCommGroup X] [NormedSpace 𝕜 X] {U : Type u_3} [NormedAddCommGroup U] [NormedSpace 𝕜 U] [CompleteSpace X] (S : ALCS 𝕜 X U ⊤) : S.IsZeroClass

Theorem 1.5 (thm:p-infty-zero-class). Let X, U be real or complex Banach spaces and S = (𝕋, Φ) an abstract linear control system with p = ∞. Then S is of the zero-class: ‖Φ t‖ → 0 as t → 0⁺.

Proof: by Steps 2–4, ‖x_n‖ → ℓ and ‖T_{h_n} x_n - x_n‖ → 0; passing to the limit in the doubling inequality of Step 1 gives 2ℓ ≤ ℓ, hence ℓ = 0.