The Lyapunov--Perron integral as a bounded linear operator

The two integral terms of the Lyapunov--Perron equation act linearly on a bounded continuous forcing term on the nonnegative time axis. Forward and backward exponential estimates bound this operator in the sup norm by 2 K / α. This is the linear part of the derivative of the Lyapunov--Perron map; packaging it as a continuous linear map makes the implicit-function argument for smooth stable and unstable manifolds possible.

The integral and exponential estimates follow Coppel, Dichotomies in Stability Theory, Chapter 5.

noncomputable def ContinuousLinearMap.lyapunovPerronIntegralCLM {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α : NNReal} (A P : X →L[ℝ] X) (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) : BoundedContinuousFunction NNReal X →L[ℝ] BoundedContinuousFunction NNReal X

The integral part of the Lyapunov--Perron equation, acting on bounded continuous curves on [0, ∞). Its value at t is the forward integral of the P component minus the improper backward integral of the remainder v - P v.

Equations

• A.lyapunovPerronIntegralCLM P hs hu hα = { toFun := A.lyapunovPerronMap P id hs hu hα ⋯ 0, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (2 * ↑K / ↑α) ⋯

@[simp]

theorem ContinuousLinearMap.lyapunovPerronIntegralCLM_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (γ : BoundedContinuousFunction NNReal X) (t : NNReal) : ((A.lyapunovPerronIntegralCLM P hs hu hα) γ) t = A.lyapunovPerronIntegral P (fun (s : ℝ) => γ s.toNNReal) ↑t

Evaluation of the bounded linear Lyapunov--Perron integral.

theorem ContinuousLinearMap.norm_lyapunovPerronIntegralCLM_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) : ‖A.lyapunovPerronIntegralCLM P hs hu hα‖ ≤ 2 * ↑K / ↑α

The Lyapunov--Perron integral has sup-operator norm at most 2 K / α.