Smooth dependence of Lyapunov--Perron solutions on the parameter

Let A and P be bounded operators on a real Banach space X satisfying the forward and backward exponential estimates of the Lyapunov--Perron construction, with constant K and rate α, and let the nonlinearity N be ε-Lipschitz with 2 K ε < α. The Lyapunov--Perron solution ContinuousLinearMap.lyapunovPerronSolution ξ is the fixed point of the operator

T ξ γ = (t ↦ exp (t A) (P ξ)) + I (N ∘ γ)

on bounded continuous curves on [0, ∞), where I is the bounded linear integral operator ContinuousLinearMap.lyapunovPerronIntegralCLM. It is Lipschitz in ξ.

This file shows that it is C¹ in ξ wherever the nonlinearity is C¹ along the solution. Suppose that N has derivative N' x at every point x of a set s, that N' is uniformly continuous on s, and that the values of the solution with parameter ξ₀ stay a fixed distance δ > 0 inside s. The superposition operator γ ↦ N ∘ γ is then C¹ near that solution (BoundedContinuousFunction.contDiffAt_comp), with derivative pointwise multiplication by N' (γ t), of operator norm at most ε. So the partial derivative in γ of the equation γ - T ξ γ = 0 is the identity minus an operator of norm at most 2 K ε / α < 1, hence invertible, and the implicit function theorem (ContDiffAt.implicitFunction) gives a C¹ solution of the equation near ξ₀. Uniqueness of fixed points of the contraction T ξ identifies it with the Lyapunov--Perron solution.

Differentiating the fixed-point equation then shows that the derivative η in the direction v solves the variational Lyapunov--Perron equation, the linearization of the integral equation along the solution γ₀:

η t = exp (t A) (P v) + lyapunovPerronIntegral A P (s ↦ N' (γ₀ s) (η s)) t.

The Lyapunov--Perron graph map, the value at time 0 minus P ξ, is therefore C¹ as well. After a cutoff, the graph map describes the local stable manifold at a hyperbolic equilibrium (TauCeti/Analysis/ODE/LyapunovPerron/Local.lean), so these results upgrade that Lipschitz graph to a C¹ one.

Main declarations

• ContinuousLinearMap.contDiffAt_lyapunovPerronSolution: the Lyapunov--Perron solution is C¹ in its parameter at every parameter whose solution stays a positive distance inside the region where the nonlinearity is C¹ with uniformly continuous derivative.
• ContinuousLinearMap.fderiv_lyapunovPerronSolution_apply: its derivative solves the variational Lyapunov--Perron equation.
• ContinuousLinearMap.contDiffAt_lyapunovPerronGraphMap: the Lyapunov--Perron graph map is C¹ at such parameters.

References

• C. Chicone, Ordinary Differential Equations with Applications, 2nd ed., Springer, 2006, Section 4.3 (smoothness of the stable manifold via the fixed-point equation).
• W. A. Coppel, Dichotomies in Stability Theory, Lecture Notes in Mathematics 629, Springer, 1978, Chapter 5.

theorem ContinuousLinearMap.contDiffAt_lyapunovPerronSolution {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} {A P : X →L[ℝ] X} {N : X → 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 < α) (hN : LipschitzWith ε N) (hsmall : 2 * K * ε < α) {N' : X → X →L[ℝ] X} {s : Set X} {δ : ℝ} {ξ₀ : X} (hNs : ∀ x ∈ s, HasFDerivAt N (N' x) x) (hN' : UniformContinuousOn N' s) (hδ : 0 < δ) (hξ₀ : ∀ (t : NNReal), Metric.ball ((A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ₀) t) δ ⊆ s) : ContDiffAt ℝ 1 (A.lyapunovPerronSolution P N hs hu hα hN hsmall) ξ₀

The Lyapunov--Perron solution is C¹ in its parameter. Suppose that the nonlinearity N has derivative N' x at every point x of a set s, with N' uniformly continuous on s, and that the values of the Lyapunov--Perron solution with parameter ξ₀ stay a distance δ > 0 inside s. Then the solution, as a bounded continuous curve with the sup norm, depends continuously differentiably on the parameter near ξ₀.

theorem ContinuousLinearMap.fderiv_lyapunovPerronSolution_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} {A P : X →L[ℝ] X} {N : X → 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 < α) (hN : LipschitzWith ε N) (hsmall : 2 * K * ε < α) {N' : X → X →L[ℝ] X} {s : Set X} {δ : ℝ} {ξ₀ : X} (hNs : ∀ x ∈ s, HasFDerivAt N (N' x) x) (hN' : UniformContinuousOn N' s) (hδ : 0 < δ) (hξ₀ : ∀ (t : NNReal), Metric.ball ((A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ₀) t) δ ⊆ s) (v : X) (t : NNReal) : ((fderiv ℝ (A.lyapunovPerronSolution P N hs hu hα hN hsmall) ξ₀) v) t = (NormedSpace.exp (↑t • A)) (P v) + A.lyapunovPerronIntegral P (fun (s : ℝ) => (N' ((A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ₀) s.toNNReal)) (((fderiv ℝ (A.lyapunovPerronSolution P N hs hu hα hN hsmall) ξ₀) v) s.toNNReal)) ↑t

The derivative of the Lyapunov--Perron solution solves the variational equation. Under the hypotheses of ContinuousLinearMap.contDiffAt_lyapunovPerronSolution, the derivative η of the solution γ₀ at ξ₀ in the direction v satisfies the Lyapunov--Perron equation of the linearization along γ₀:

η t = exp (t A) (P v) + lyapunovPerronIntegral A P (s ↦ N' (γ₀ s) (η s)) t.

theorem ContinuousLinearMap.contDiffAt_lyapunovPerronGraphMap {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {K α ε : NNReal} {A P : X →L[ℝ] X} {N : X → 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 < α) (hN : LipschitzWith ε N) (hsmall : 2 * K * ε < α) {N' : X → X →L[ℝ] X} {s : Set X} {δ : ℝ} {ξ₀ : X} (hNs : ∀ x ∈ s, HasFDerivAt N (N' x) x) (hN' : UniformContinuousOn N' s) (hδ : 0 < δ) (hξ₀ : ∀ (t : NNReal), Metric.ball ((A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ₀) t) δ ⊆ s) : ContDiffAt ℝ 1 (A.lyapunovPerronGraphMap P N hs hu hα hN hsmall) ξ₀

The Lyapunov--Perron graph map is C¹ at every parameter whose solution stays a positive distance inside the region where the nonlinearity is C¹ with uniformly continuous derivative.