Continuity of the input response for p < ∞ (Proposition 1.3)

Proposition 1.3 (prop:finite-p-solution-continuous). Assume p ∈ [1, ∞). For all u ∈ L^p(ℝ₊; U), t ↦ Φ_t u is continuous on ℝ₊.

The paper refers to [Weiss 1989, Proposition 2.3] and does not write out a proof. We formalize the classical argument, which uses p < ∞ twice:

1. ‖u‖_{L^p(0, t)} → 0 as t → 0 (ALCS.tendsto_norm_truncate). With causality and monotonicity of κ, this gives Φ_t u → 0 as t → 0⁺ (ALCS.tendsto_Phi_zero).
2. Right continuity at τ ≥ 0 then follows from the composition property Φ_{τ+h} u = T_h Φ_τ u + Φ_h u(τ + ·) (ALCS.tendsto_Phi_right).
3. Left continuity at τ > 0 uses u = u ⋄_h u(h + ·), which gives Φ_τ u - Φ_{τ-h} u = T_{τ-h} Φ_h u + Φ_{τ-h} (u(h + ·) - u), and the continuity of translations in L^p (ALCS.tendsto_norm_shiftLeft_sub); see ALCS.tendsto_Phi_left.

The main statement is ALCS.continuousOn_Phi_of_ne_top.

theorem AbstractLinearControl.ALCS.tendsto_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) (hp : p ≠ ⊤) (u : ↥(MeasureTheory.Lp U p muPlus)) : Filter.Tendsto (fun (t : ℝ) => (S.Φ t) u) (nhdsWithin 0 (Set.Ici 0)) (nhds 0)

Step 1: for p < ∞, Φ t u → 0 as t → 0⁺. For t ∈ [0, 1], ‖Φ_t u‖ = ‖Φ_t (u ⋄_t 0)‖ ≤ ‖Φ_1‖ ‖u‖_{L^p(0, t)}.

theorem AbstractLinearControl.ALCS.tendsto_Phi_right {𝕜 : 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) (hp : p ≠ ⊤) (u : ↥(MeasureTheory.Lp U p muPlus)) (τ : ℝ) (hτ : 0 ≤ τ) : Filter.Tendsto (fun (h : ℝ) => (S.Φ (τ + h)) u) (nhdsWithin 0 (Set.Ici 0)) (nhds ((S.Φ τ) u))

Step 2 (right continuity): for p < ∞ and τ ≥ 0, Φ (τ + h) u → Φ τ u as h → 0⁺, since Φ (τ + h) u = T h (Φ τ u) + Φ h u(τ + ·).

theorem AbstractLinearControl.ALCS.tendsto_Phi_left {𝕜 : 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) [CompleteSpace X] (hp : p ≠ ⊤) (u : ↥(MeasureTheory.Lp U p muPlus)) (τ : ℝ) (hτ : 0 < τ) : Filter.Tendsto (fun (h : ℝ) => (S.Φ (τ - h)) u) (nhdsWithin 0 (Set.Ici 0)) (nhds ((S.Φ τ) u))

Step 3 (left continuity): for p < ∞ and τ > 0, Φ (τ - h) u → Φ τ u as h → 0⁺. With u_h := u (h + ·), one has u = u ⋄_h u_h, hence Φ τ u - Φ (τ - h) u = T (τ - h) (Φ h u) + Φ (τ - h) (u_h - u), so that ‖Φ τ u - Φ (τ - h) u‖ ≤ K ‖Φ h u‖ + ‖Φ τ‖ ‖u_h - u‖, where K bounds ‖T s‖ on [0, τ].

theorem AbstractLinearControl.ALCS.continuousOn_Phi_of_ne_top {𝕜 : 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) [CompleteSpace X] (hp : p ≠ ⊤) (u : ↥(MeasureTheory.Lp U p muPlus)) : ContinuousOn (fun (t : ℝ) => (S.Φ t) u) (Set.Ici 0)

Proposition 1.3 (prop:finite-p-solution-continuous). For p ∈ [1, ∞) and every input u ∈ L^p(ℝ₊; U), the map t ↦ Φ t u is continuous on ℝ₊ = [0, ∞).