Inputs: the space L^p(ℝ₊; U), concatenation, shifts and truncations #
This file contains the measure-theoretic plumbing on inputs used throughout the development. Nothing here is specific to control systems.
Conventions #
L^p(ℝ₊; U)is Mathlib'sLp U p muPlus, wheremuPlusis Lebesgue measure restricted toℝ₊ = [0, ∞). Its elements are almost-everywhere classes;⇑u : ℝ → Uis an (arbitrary) representative, whose values at negative times are irrelevant.- The
τ-concatenationu ⋄_τ vof the paper isconcat τ u v, defined on raw functionsℝ → U. Statements about inputs are phrased as "wis an element ofL^p(ℝ₊; U)whose representative is a.e. equal toconcat τ ⇑u ⇑v".
Main declarations #
muPlus,concat,ALCS.concat_congr: definitions, and independence of the concatenation from the chosen representatives.ALCS.shiftLeft a u: the inputs ↦ u (a + s);ALCS.exists_shiftgivesu = u ⋄_a (shiftLeft a u), andALCS.tendsto_norm_shiftLeft_subis the continuity of translations inL^pforp < ∞.ALCS.exists_delay: the delayed input0 ⋄_a u, with the same norm bound.ALCS.truncate τ u: the inputu ⋄_τ 0;ALCS.tendsto_norm_truncatesays that‖u‖_{L^p(0, τ)} → 0asτ → 0forp < ∞.ALCS.exists_concat: forp = ∞, the concatenation of two inputs of norm at mostCis an input of norm at mostC.
Lebesgue measure on ℝ₊ = [0, ∞).
Equations
Instances For
The τ-concatenation u ⋄_τ v of the paper: equal to u s for s < τ and to
v (s - τ) for s ≥ τ ("play u on [0, τ), then play v").
Instances For
Translations of the half-line #
s ↦ a + s sends ℝ₊ to [a, ∞), preserving Lebesgue measure.
s ↦ -a + s sends [a, ∞) to ℝ₊, preserving Lebesgue measure.
Concatenation #
Extension by zero to the whole line #
Extension by zero to ℝ of a function on ℝ₊.
Equations
Instances For
If φ preserves Lebesgue measure on ℝ, then ‖(zeroExt u) ∘ φ‖_{L^p(ℝ₊)} ≤ ‖u‖.
An element of L^p defined from a raw function has norm at most ‖u‖ as soon as
the eLpNorm of the raw function is at most that of u.
Left shifts u ↦ u (a + ·) #
The left shift s ↦ u (a + s) of an input. (For a < 0, the input is first
extended by zero to negative times.)
Equations
- AbstractLinearControl.ALCS.shiftLeft a u = MeasureTheory.MemLp.toLp (AbstractLinearControl.ALCS.zeroExt ↑↑u ∘ fun (s : ℝ) => a + s) ⋯
Instances For
For a ≥ 0, u = u ⋄_a (shiftLeft a u).
Shifted input (used with τ := a in the composition property):
for a ≥ 0, u₁ := u (a + ·) satisfies ‖u₁‖ ≤ ‖u‖ and u = u ⋄_a u₁.
Delays u ↦ 0 ⋄_a u #
Delayed input: the input 0 ⋄_a u (zero on [0, a), then u)
belongs to L^p(ℝ₊; U), with norm at most ‖u‖.
Truncations u ↦ u ⋄_τ 0 #
The truncated input u ⋄_τ 0: equal to u on [0, τ) and to zero afterwards.
Equations
- AbstractLinearControl.ALCS.truncate τ u = MeasureTheory.MemLp.toLp ((Set.Iio τ).indicator ↑↑u) ⋯
Instances For
For p < ∞, ‖u‖_{L^p(0, τ)} → 0 as τ → 0.
Continuity of left shifts for p < ∞ #
The translations s ↦ a + s, as continuous maps depending continuously on a.
Equations
- AbstractLinearControl.ALCS.translation = { toFun := fun (q : ℝ × ℝ) => q.1 + q.2, continuous_toFun := AbstractLinearControl.ALCS.translation._proof_1 }.curry
Instances For
The zero extension of u, as an element of L^p(ℝ).
Equations
Instances For
The zero extension of u, translated by a, as an element of L^p(ℝ).
Equations
Instances For
‖u (a + ·) - u‖_{L^p(ℝ₊)} ≤ ‖Z (a + ·) - Z‖_{L^p(ℝ)}, where Z is the zero
extension of u.
Continuity of translations in L^p(ℝ₊; U) for p < ∞: u (a + ·) → u as a → 0.
Inputs in L^∞(ℝ₊; U) #
A pointwise bound gives membership in L^∞, without a finite-measure assumption.
An everywhere bounded, strongly measurable representative. The representative is
only modified where it exceeds C.
For p = ∞, concatenation preserves a common norm bound: if ‖u‖, ‖v‖ ≤ C, then
u ⋄_a v is an input of norm at most C.
The L^∞ class of a bounded raw function has the same bound.