For p < ∞, not every system is zero-class (Proposition 3.1)

Proposition 3.1 (prop:example-finite-p-not-zero-class). Let p ∈ [1, ∞). There exist Banach spaces X and U and an abstract linear control system (𝕋, Φ) such that κ(t) = 1 for all t > 0.

As in the paper, X = L^p(ℝ₊), U = ℝ, and

• T t is the right shift: (T t f)(s) = f (s - t) for s ≥ t and 0 for s < t;
• Φ t reverses the input on [0, t]: (Φ t u)(s) = u (t - s) for 0 < s ≤ t and 0 otherwise. (The paper uses 0 ≤ s < t; this changes a null set only, and makes the concatenation identity hold pointwise.)

Main declarations

• ShiftExample.shiftSystem : the system, an ALCS ℝ (Lp ℝ p muPlus) ℝ p.
• ShiftExample.norm_Phi_eq_one : ‖Φ t‖ = 1 for all t > 0.
• exists_system_norm_Phi_eq_one : Proposition 3.1, as an existence statement.
• ShiftExample.not_zero_class : the system is not of the zero-class (Definition 1.4).

Implementation

All operators are built in one way (op): extend f by zero to ℝ (zext), compose with a measure-preserving map φ : ℝ → ℝ, multiply by the indicator of a set A, and restrict to ℝ₊. Then T t = op (· - t) univ and Φ t = op (t - ·) (Ioc 0 t). Strong continuity of the shift reduces to the continuity of translations in L^p(ℝ), which is Filter.Tendsto.compMeasurePreservingLp in Mathlib; it fails for p = ∞.

Raw functions

noncomputable def AbstractLinearControl.ShiftExample.zext (f : ℝ → ℝ) : ℝ → ℝ

Extension by zero of f from [0, ∞) to ℝ.

Equations

• AbstractLinearControl.ShiftExample.zext f = AbstractLinearControl.ALCS.zeroExt f

noncomputable def AbstractLinearControl.ShiftExample.rawOp (φ : ℝ → ℝ) (A : Set ℝ) (f : ℝ → ℝ) : ℝ → ℝ

The raw operator: s ↦ 1_A(s) · (zext f)(φ s).

Equations

• AbstractLinearControl.ShiftExample.rawOp φ A f = A.indicator (AbstractLinearControl.ShiftExample.zext f ∘ φ)

theorem AbstractLinearControl.ShiftExample.zext_of_nonneg (f : ℝ → ℝ) (y : ℝ) (h : 0 ≤ y) : zext f y = f y

theorem AbstractLinearControl.ShiftExample.zext_of_neg (f : ℝ → ℝ) (y : ℝ) (h : y < 0) : zext f y = 0

theorem AbstractLinearControl.ShiftExample.rawOp_add {φ : ℝ → ℝ} {A : Set ℝ} (f g : ℝ → ℝ) (x : ℝ) : rawOp φ A (f + g) x = rawOp φ A f x + rawOp φ A g x

theorem AbstractLinearControl.ShiftExample.rawOp_smul {φ : ℝ → ℝ} {A : Set ℝ} (c : ℝ) (f : ℝ → ℝ) (x : ℝ) : rawOp φ A (c • f) x = c • rawOp φ A f x

theorem AbstractLinearControl.ShiftExample.rawOp_congr {φ : ℝ → ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (A : Set ℝ) {f g : ℝ → ℝ} (h : f =ᵐ[muPlus] g) : rawOp φ A f =ᵐ[muPlus] rawOp φ A g

rawOp only depends on the a.e. class of f on ℝ₊.

Evaluation of the raw shift and of the raw input map

theorem AbstractLinearControl.ShiftExample.rawT_apply (f : ℝ → ℝ) (t x : ℝ) : rawOp (fun (y : ℝ) => y - t) Set.univ f x = zext f (x - t)

Raw shift: rawOp (· - t) univ f x = zext f (x - t).

theorem AbstractLinearControl.ShiftExample.rawPhi_of_mem (f : ℝ → ℝ) (a y : ℝ) (h : 0 < y ∧ y ≤ a) : rawOp (fun (z : ℝ) => a - z) (Set.Ioc 0 a) f y = f (a - y)

Raw input map, for 0 < y ≤ a: the value is f (a - y).

theorem AbstractLinearControl.ShiftExample.rawPhi_of_not (f : ℝ → ℝ) (a y : ℝ) (h : ¬(0 < y ∧ y ≤ a)) : rawOp (fun (z : ℝ) => a - z) (Set.Ioc 0 a) f y = 0

Raw input map, outside (0, a]: the value is 0.

theorem AbstractLinearControl.ShiftExample.zext_rawPhi_of_nonpos (f : ℝ → ℝ) (a y : ℝ) (hy : y ≤ 0) : zext (rawOp (fun (z : ℝ) => a - z) (Set.Ioc 0 a) f) y = 0

The raw input map vanishes on (-∞, 0], also after extension by zero.

theorem AbstractLinearControl.ShiftExample.concat_of_lt (u v : ℝ → ℝ) (τ y : ℝ) (h : y < τ) : concat τ u v y = u y

theorem AbstractLinearControl.ShiftExample.concat_of_ge (u v : ℝ → ℝ) (τ y : ℝ) (h : τ ≤ y) : concat τ u v y = v (y - τ)

theorem AbstractLinearControl.ShiftExample.concat_pointwise (u v : ℝ → ℝ) {τ t : ℝ} (hτ : 0 ≤ τ) (ht : 0 ≤ t) (x : ℝ) : rawOp (fun (y : ℝ) => τ + t - y) (Set.Ioc 0 (τ + t)) (concat τ u v) x = rawOp (fun (y : ℝ) => y - t) Set.univ (rawOp (fun (y : ℝ) => τ - y) (Set.Ioc 0 τ) u) x + rawOp (fun (y : ℝ) => t - y) (Set.Ioc 0 t) v x

The concatenation identity, pointwise, for raw functions: Φ (τ + t) (u ⋄_τ v) = T t (Φ τ u) + Φ t v.

Bounded operators on L^p(ℝ₊)

theorem AbstractLinearControl.ShiftExample.memLp_zext {p : ENNReal} (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : MeasureTheory.MemLp (zext ↑↑f) p MeasureTheory.volume

theorem AbstractLinearControl.ShiftExample.eLpNorm_zext {p : ENNReal} (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : MeasureTheory.eLpNorm (zext ↑↑f) p MeasureTheory.volume = MeasureTheory.eLpNorm (↑↑f) p muPlus

theorem AbstractLinearControl.ShiftExample.memLp_rawOp {p : ENNReal} {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : MeasureTheory.MemLp (rawOp φ A ↑↑f) p muPlus

theorem AbstractLinearControl.ShiftExample.eLpNorm_rawOp_le {p : ENNReal} {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : MeasureTheory.eLpNorm (rawOp φ A ↑↑f) p muPlus ≤ MeasureTheory.eLpNorm (↑↑f) p muPlus

noncomputable def AbstractLinearControl.ShiftExample.opFun {p : ENNReal} (φ : ℝ → ℝ) (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (A : Set ℝ) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : ↥(MeasureTheory.Lp ℝ p muPlus)

f ↦ rawOp φ A f, as a map on L^p(ℝ₊).

Equations

• AbstractLinearControl.ShiftExample.opFun φ hφ A hA f = MeasureTheory.MemLp.toLp (AbstractLinearControl.ShiftExample.rawOp φ A ↑↑f) ⋯

theorem AbstractLinearControl.ShiftExample.opFun_ae {p : ENNReal} {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : ↑↑(opFun φ hφ A hA f) =ᵐ[muPlus] rawOp φ A ↑↑f

theorem AbstractLinearControl.ShiftExample.opFun_congr {p : ENNReal} {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) {g : ℝ → ℝ} (h : ↑↑f =ᵐ[muPlus] g) : ↑↑(opFun φ hφ A hA f) =ᵐ[muPlus] rawOp φ A g

theorem AbstractLinearControl.ShiftExample.opFun_add {p : ENNReal} {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f g : ↥(MeasureTheory.Lp ℝ p muPlus)) : opFun φ hφ A hA (f + g) = opFun φ hφ A hA f + opFun φ hφ A hA g

theorem AbstractLinearControl.ShiftExample.opFun_smul {p : ENNReal} {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (c : ℝ) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : opFun φ hφ A hA (c • f) = c • opFun φ hφ A hA f

theorem AbstractLinearControl.ShiftExample.norm_opFun_le {p : ENNReal} {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : ‖opFun φ hφ A hA f‖ ≤ ‖f‖

noncomputable def AbstractLinearControl.ShiftExample.op {p : ENNReal} [Fact (1 ≤ p)] (φ : ℝ → ℝ) (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (A : Set ℝ) (hA : MeasurableSet A) : ↥(MeasureTheory.Lp ℝ p muPlus) →L[ℝ] ↥(MeasureTheory.Lp ℝ p muPlus)

f ↦ rawOp φ A f, as a bounded linear operator on L^p(ℝ₊), of norm at most 1.

Equations

• AbstractLinearControl.ShiftExample.op φ hφ A hA = { toFun := AbstractLinearControl.ShiftExample.opFun φ hφ A hA, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem AbstractLinearControl.ShiftExample.op_apply {p : ENNReal} [Fact (1 ≤ p)] {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : (op φ hφ A hA) f = opFun φ hφ A hA f

theorem AbstractLinearControl.ShiftExample.op_ae {p : ENNReal} [Fact (1 ≤ p)] {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : ↑↑((op φ hφ A hA) f) =ᵐ[muPlus] rawOp φ A ↑↑f

theorem AbstractLinearControl.ShiftExample.op_congr {p : ENNReal} [Fact (1 ≤ p)] {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) {g : ℝ → ℝ} (h : ↑↑f =ᵐ[muPlus] g) : ↑↑((op φ hφ A hA) f) =ᵐ[muPlus] rawOp φ A g

theorem AbstractLinearControl.ShiftExample.norm_op_le {p : ENNReal} [Fact (1 ≤ p)] {φ : ℝ → ℝ} {A : Set ℝ} (hφ : MeasureTheory.MeasurePreserving φ MeasureTheory.volume MeasureTheory.volume) (hA : MeasurableSet A) : ‖op φ hφ A hA‖ ≤ 1

The right-shift semigroup

noncomputable def AbstractLinearControl.ShiftExample.shiftT (p : ENNReal) [Fact (1 ≤ p)] (t : ℝ) : ↥(MeasureTheory.Lp ℝ p muPlus) →L[ℝ] ↥(MeasureTheory.Lp ℝ p muPlus)

The right shift T t: (T t f)(s) = f (s - t) for s ≥ t, 0 for s < t.

Equations

• AbstractLinearControl.ShiftExample.shiftT p t = AbstractLinearControl.ShiftExample.op (fun (x : ℝ) => x - t) ⋯ Set.univ ⋯

theorem AbstractLinearControl.ShiftExample.shiftT_ae {p : ENNReal} [Fact (1 ≤ p)] (t : ℝ) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : ↑↑((shiftT p t) f) =ᵐ[muPlus] rawOp (fun (x : ℝ) => x - t) Set.univ ↑↑f

theorem AbstractLinearControl.ShiftExample.shiftT_congr {p : ENNReal} [Fact (1 ≤ p)] (t : ℝ) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) {g : ℝ → ℝ} (h : ↑↑f =ᵐ[muPlus] g) : ↑↑((shiftT p t) f) =ᵐ[muPlus] rawOp (fun (x : ℝ) => x - t) Set.univ g

theorem AbstractLinearControl.ShiftExample.shiftT_zero {p : ENNReal} [Fact (1 ≤ p)] : shiftT p 0 = ContinuousLinearMap.id ℝ ↥(MeasureTheory.Lp ℝ p muPlus)

theorem AbstractLinearControl.ShiftExample.shiftT_add {p : ENNReal} [Fact (1 ≤ p)] {t s : ℝ} (_ht : 0 ≤ t) (hs : 0 ≤ s) : shiftT p (t + s) = shiftT p t ∘SL shiftT p s

Strong continuity, from the generic half-line translation theorem

theorem AbstractLinearControl.ShiftExample.shiftT_eq_shiftLeft {p : ENNReal} [Fact (1 ≤ p)] (t : ℝ) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : (shiftT p t) f = ALCS.shiftLeft (-t) f

The right shift is the half-line left shift with a negative translation parameter.

theorem AbstractLinearControl.ShiftExample.shiftT_tendsto {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) (y : ↥(MeasureTheory.Lp ℝ p muPlus)) : Filter.Tendsto (fun (t : ℝ) => (shiftT p t) y) (nhdsWithin 0 (Set.Ici 0)) (nhds y)

Strong continuity of the right shift (uses p ≠ ∞).

noncomputable def AbstractLinearControl.ShiftExample.rightShift {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : C0Semigroup ℝ ↥(MeasureTheory.Lp ℝ p muPlus)

The right-shift semigroup on L^p(ℝ₊), for p < ∞.

Equations

• AbstractLinearControl.ShiftExample.rightShift hp = { T := AbstractLinearControl.ShiftExample.shiftT p, T_zero := ⋯, T_add := ⋯, T_cont := ⋯ }

The input maps

noncomputable def AbstractLinearControl.ShiftExample.inputPhi (p : ENNReal) [Fact (1 ≤ p)] (t : ℝ) : ↥(MeasureTheory.Lp ℝ p muPlus) →L[ℝ] ↥(MeasureTheory.Lp ℝ p muPlus)

The input map Φ t: (Φ t u)(s) = u (t - s) for 0 < s ≤ t, 0 otherwise.

Equations

• AbstractLinearControl.ShiftExample.inputPhi p t = AbstractLinearControl.ShiftExample.op (fun (x : ℝ) => t - x) ⋯ (Set.Ioc 0 t) ⋯

theorem AbstractLinearControl.ShiftExample.inputPhi_ae {p : ENNReal} [Fact (1 ≤ p)] (t : ℝ) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) : ↑↑((inputPhi p t) f) =ᵐ[muPlus] rawOp (fun (x : ℝ) => t - x) (Set.Ioc 0 t) ↑↑f

theorem AbstractLinearControl.ShiftExample.inputPhi_congr {p : ENNReal} [Fact (1 ≤ p)] (t : ℝ) (f : ↥(MeasureTheory.Lp ℝ p muPlus)) {g : ℝ → ℝ} (h : ↑↑f =ᵐ[muPlus] g) : ↑↑((inputPhi p t) f) =ᵐ[muPlus] rawOp (fun (x : ℝ) => t - x) (Set.Ioc 0 t) g

theorem AbstractLinearControl.ShiftExample.inputPhi_composition {p : ENNReal} [Fact (1 ≤ p)] {τ t : ℝ} (hτ : 0 ≤ τ) (ht : 0 ≤ t) (u v w : ↥(MeasureTheory.Lp ℝ p muPlus)) (hw : ↑↑w =ᵐ[muPlus] concat τ ↑↑u ↑↑v) : (inputPhi p (τ + t)) w = (shiftT p t) ((inputPhi p τ) u) + (inputPhi p t) v

Composition property: Φ (τ + t) (u ⋄_τ v) = T t (Φ τ u) + Φ t v.

noncomputable def AbstractLinearControl.ShiftExample.shiftSystem {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : ALCS ℝ ↥(MeasureTheory.Lp ℝ p muPlus) ℝ p

The abstract linear control system of Proposition 3.1 (right shift on L^p(ℝ₊)).

Equations

• AbstractLinearControl.ShiftExample.shiftSystem hp = { toC0Semigroup := AbstractLinearControl.ShiftExample.rightShift hp, Φ := AbstractLinearControl.ShiftExample.inputPhi p, composition := ⋯ }

κ(t) = 1 for all t > 0

theorem AbstractLinearControl.ShiftExample.p_ne_zero {p : ENNReal} [Fact (1 ≤ p)] : p ≠ 0

theorem AbstractLinearControl.ShiftExample.muPlus_Ico (t : ℝ) : muPlus (Set.Ico 0 t) = ENNReal.ofReal t

theorem AbstractLinearControl.ShiftExample.muPlus_Ioc (t : ℝ) : muPlus (Set.Ioc 0 t) = ENNReal.ofReal t

theorem AbstractLinearControl.ShiftExample.muPlus_Ico_ne_top (t : ℝ) : muPlus (Set.Ico 0 t) ≠ ⊤

theorem AbstractLinearControl.ShiftExample.muPlus_Ioc_ne_top (t : ℝ) : muPlus (Set.Ioc 0 t) ≠ ⊤

noncomputable def AbstractLinearControl.ShiftExample.testInput (p : ENNReal) (t : ℝ) : ↥(MeasureTheory.Lp ℝ p muPlus)

The test input 1_{[0,t)}.

Equations

• AbstractLinearControl.ShiftExample.testInput p t = MeasureTheory.indicatorConstLp p ⋯ ⋯ 1

noncomputable def AbstractLinearControl.ShiftExample.testOutput (p : ENNReal) (t : ℝ) : ↥(MeasureTheory.Lp ℝ p muPlus)

The corresponding output 1_{(0,t]}.

Equations

• AbstractLinearControl.ShiftExample.testOutput p t = MeasureTheory.indicatorConstLp p ⋯ ⋯ 1

theorem AbstractLinearControl.ShiftExample.inputPhi_testInput {p : ENNReal} [Fact (1 ≤ p)] (t : ℝ) : (inputPhi p t) (testInput p t) = testOutput p t

theorem AbstractLinearControl.ShiftExample.norm_testInput {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {t : ℝ} (ht : 0 ≤ t) : ‖testInput p t‖ = t ^ (1 / p.toReal)

theorem AbstractLinearControl.ShiftExample.norm_testOutput {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {t : ℝ} (ht : 0 ≤ t) : ‖testOutput p t‖ = t ^ (1 / p.toReal)

theorem AbstractLinearControl.ShiftExample.norm_inputPhi_le {p : ENNReal} [Fact (1 ≤ p)] (t : ℝ) : ‖inputPhi p t‖ ≤ 1

theorem AbstractLinearControl.ShiftExample.one_le_norm_inputPhi {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {t : ℝ} (ht : 0 < t) : 1 ≤ ‖inputPhi p t‖

theorem AbstractLinearControl.ShiftExample.norm_Phi_eq_one {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) {t : ℝ} (ht : 0 < t) : ‖(shiftSystem hp).Φ t‖ = 1

κ(t) = ‖Φ t‖ = 1 for all t > 0.

theorem AbstractLinearControl.ShiftExample.not_zero_class {p : ENNReal} [Fact (1 ≤ p)] (hp : p ≠ ⊤) : ¬(shiftSystem hp).IsZeroClass

The system of Proposition 3.1 is not of the zero-class (Definition 1.4).

theorem AbstractLinearControl.exists_system_norm_Phi_eq_one (p : ENNReal) [Fact (1 ≤ p)] (hp : p ≠ ⊤) : ∃ (X : Type) (x : NormedAddCommGroup X) (x_1 : NormedSpace ℝ X) (_ : CompleteSpace X) (U : Type) (x_3 : NormedAddCommGroup U) (x_4 : NormedSpace ℝ U) (_ : CompleteSpace U) (S : ALCS ℝ X U p), ∀ (t : ℝ), 0 < t → ‖S.Φ t‖ = 1

Proposition 3.1 (prop:example-finite-p-not-zero-class). For p ∈ [1, ∞), there exist (real) Banach spaces X, U and an abstract linear control system (T, Φ) with κ(t) = ‖Φ t‖ = 1 for all t > 0.