The Lyapunov--Perron graph

Let A and P be bounded operators on a real Banach space X such that the linear flow exp (t A) damps P v exponentially in forward time and v - P v exponentially in backward time, with constant K and rate α > 0; let N be globally ε-Lipschitz, with 2 K ε < α. When moreover P is idempotent and commutes with A, the initial values of the solutions of y' = A y + N y that stay bounded on [0, ∞) are exactly the fixed points of ξ ↦ lyapunovPerronSolution ξ 0.

This file identifies that fixed-point set as a Lipschitz graph over the range of P. The graph map ContinuousLinearMap.lyapunovPerronGraphMap records how far the initial value of a Lyapunov--Perron solution sits from P ξ. It takes values in the kernel of P, depends only on P ξ, and is Lipschitz with a constant that tends to 0 with ε: in the limit of a vanishing nonlinearity the graph flattens onto the range of P. The projection P and the parametrization v ↦ v + graph map v invert each other, so P is a bijection from the fixed-point set onto the range of P.

When the nonlinearity fixes the origin, the fixed-point set is the set of initial values of forward solutions tending to the equilibrium 0. The graph description is therefore a Lipschitz graph characterization of the global stable set for a globally small nonlinearity. A local stable-manifold theorem additionally requires a cutoff, identification of the resulting graph with the local stable set, and differentiability and tangency of the graph.

Main declarations

• ContinuousLinearMap.lyapunovPerronGraphMap: the displacement of the initial value of a Lyapunov--Perron solution away from the range of P.
• ContinuousLinearMap.apply_lyapunovPerronGraphMap: it takes values in the kernel of P.
• ContinuousLinearMap.lipschitzWith_lyapunovPerronGraphMap: it is Lipschitz, with a constant that tends to 0 with the Lipschitz constant of the nonlinearity; ContinuousLinearMap.norm_lyapunovPerronGraphMap_le is the resulting cone bound.
• ContinuousLinearMap.hasFDerivAt_lyapunovPerronGraphMap_zero: when the nonlinearity fixes the origin and has derivative zero there, so does the graph map.
• ContinuousLinearMap.setOf_lyapunovPerronSolution_zero_eq_image: the fixed-point set is the graph of the graph map over the range of P.
• ContinuousLinearMap.invOn_add_lyapunovPerronGraphMap and ContinuousLinearMap.bijOn_apply_setOf_lyapunovPerronSolution_zero: P parametrizes the fixed-point set by the range of P.
• ContinuousLinearMap.setOf_exists_isIntegralCurveOn_bounded_eq_image and ContinuousLinearMap.setOf_exists_isIntegralCurveOn_tendsto_eq_image: the initial values of the bounded forward solutions, respectively of the forward solutions tending to 0, form that graph.

References

• W. A. Coppel, Dichotomies in Stability Theory, Lecture Notes in Mathematics 629, Springer, 1978, Chapter 5.
• C. Chicone, Ordinary Differential Equations with Applications, 2nd ed., Springer, 2006, Section 4.3.
• M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.

noncomputable def ContinuousLinearMap.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 * ε < α) (ξ : X) : X

The Lyapunov--Perron graph map: the displacement of the initial value lyapunovPerronSolution ξ 0 of the Lyapunov--Perron solution with input parameter ξ away from P ξ.

When P is idempotent and commutes with A, this displacement lies in the kernel of P and depends only on P ξ, so the initial values of the bounded forward solutions of y' = A y + N y form the graph of this map over the range of P.

Equations

• A.lyapunovPerronGraphMap P N hs hu hα hN hsmall ξ = (A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) 0 - P ξ

theorem ContinuousLinearMap.lyapunovPerronSolution_zero_eq_add_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 * ε < α) (ξ : X) : (A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) 0 = P ξ + A.lyapunovPerronGraphMap P N hs hu hα hN hsmall ξ

The initial value of a Lyapunov--Perron solution splits as P ξ plus the graph displacement.

theorem ContinuousLinearMap.lyapunovPerronGraphMap_eq_lyapunovPerronIntegral {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 * ε < α) (ξ : X) : A.lyapunovPerronGraphMap P N hs hu hα hN hsmall ξ = A.lyapunovPerronIntegral P (fun (s : ℝ) => N ((A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) s.toNNReal)) 0

The graph displacement is the value at time 0 of the integral terms of the Lyapunov--Perron equation: at time 0 the homogeneous term contributes exactly P ξ.

@[simp]

theorem ContinuousLinearMap.apply_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 * ε < α) (hP : IsIdempotentElem P) (hAP : Commute A P) (ξ : X) : P (A.lyapunovPerronGraphMap P N hs hu hα hN hsmall ξ) = 0

When P is idempotent and commutes with A, the graph displacement lies in the kernel of P.

@[simp]

theorem ContinuousLinearMap.lyapunovPerronGraphMap_map {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 * ε < α) (hP : IsIdempotentElem P) (ξ : X) : A.lyapunovPerronGraphMap P N hs hu hα hN hsmall (P ξ) = A.lyapunovPerronGraphMap P N hs hu hα hN hsmall ξ

When P is idempotent, the graph displacement depends only on the P-component of the input parameter.

@[simp]

theorem ContinuousLinearMap.lyapunovPerronGraphMap_zero {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 * ε < α) (hN0 : N 0 = 0) : A.lyapunovPerronGraphMap P N hs hu hα hN hsmall 0 = 0

If the nonlinearity vanishes at the origin, so does the graph map.

theorem ContinuousLinearMap.lipschitzWith_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 * ε < α) : LipschitzWith (2 * K * ε / α * (K / (1 - 2 * K * ε / α))) (A.lyapunovPerronGraphMap P N hs hu hα hN hsmall)

The Lyapunov--Perron graph map is Lipschitz. Its constant, which equals 2 K² ε / (α - 2 K ε), tends to 0 with the Lipschitz constant ε of the nonlinearity: in the limit of a vanishing nonlinearity the graph flattens onto the range of P.

theorem ContinuousLinearMap.norm_lyapunovPerronGraphMap_le {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 * ε < α) (hN0 : N 0 = 0) (ξ : X) : ‖A.lyapunovPerronGraphMap P N hs hu hα hN hsmall ξ‖ ≤ ↑(2 * K * ε / α * (K / (1 - 2 * K * ε / α))) * ‖ξ‖

If the nonlinearity vanishes at the origin, the graph lies in a cone around the range of P whose opening tends to 0 with the Lipschitz constant of the nonlinearity.

theorem ContinuousLinearMap.hasFDerivAt_lyapunovPerronGraphMap_zero {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 * ε < α) (hN0 : N 0 = 0) (hN' : HasFDerivAt N 0 0) : HasFDerivAt (A.lyapunovPerronGraphMap P N hs hu hα hN hsmall) 0 0

The Lyapunov--Perron graph map is flat at the equilibrium. If the nonlinearity fixes the origin and has derivative zero there, then the graph map also has derivative zero at the origin.

theorem ContinuousLinearMap.invOn_add_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 * ε < α) (hP : IsIdempotentElem P) (hAP : Commute A P) : Set.InvOn (fun (v : X) => v + A.lyapunovPerronGraphMap P N hs hu hα hN hsmall v) ⇑P {x : X | (A.lyapunovPerronSolution P N hs hu hα hN hsmall x) 0 = x} (Set.range ⇑P)

The projection P and the parametrization v ↦ v + graph map v are mutually inverse between the Lyapunov--Perron fixed-point set and the range of P.

theorem ContinuousLinearMap.setOf_lyapunovPerronSolution_zero_eq_image {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 * ε < α) (hP : IsIdempotentElem P) (hAP : Commute A P) : {x : X | (A.lyapunovPerronSolution P N hs hu hα hN hsmall x) 0 = x} = (fun (v : X) => v + A.lyapunovPerronGraphMap P N hs hu hα hN hsmall v) '' Set.range ⇑P

The Lyapunov--Perron fixed-point set is a graph over the range of P. When P is idempotent and commutes with A, the fixed points of ξ ↦ lyapunovPerronSolution ξ 0 are exactly the points v + graph map v with v in the range of P. The graph map is Lipschitz by ContinuousLinearMap.lipschitzWith_lyapunovPerronGraphMap and takes values in the kernel of P by ContinuousLinearMap.apply_lyapunovPerronGraphMap.

theorem ContinuousLinearMap.bijOn_apply_setOf_lyapunovPerronSolution_zero {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 * ε < α) (hP : IsIdempotentElem P) (hAP : Commute A P) : Set.BijOn ⇑P {x : X | (A.lyapunovPerronSolution P N hs hu hα hN hsmall x) 0 = x} (Set.range ⇑P)

The projection P parametrizes the Lyapunov--Perron fixed-point set by its range.

theorem ContinuousLinearMap.setOf_exists_isIntegralCurveOn_bounded_eq_image {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 * ε < α) (hP : IsIdempotentElem P) (hAP : Commute A P) : {x : X | ∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (y : X) => A y + N y) (Set.Ici 0) ∧ y 0 = x ∧ ∃ (B : ℝ), ∀ t ∈ Set.Ici 0, ‖y t‖ ≤ B} = (fun (v : X) => v + A.lyapunovPerronGraphMap P N hs hu hα hN hsmall v) '' Set.range ⇑P

The initial values of the bounded forward solutions form a graph over the range of P.

theorem ContinuousLinearMap.setOf_exists_isIntegralCurveOn_tendsto_eq_image {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 * ε < α) (hP : IsIdempotentElem P) (hAP : Commute A P) (hN0 : N 0 = 0) : {x : X | ∃ (y : ℝ → X), IsIntegralCurveOn y (fun (x : ℝ) (y : X) => A y + N y) (Set.Ici 0) ∧ y 0 = x ∧ Filter.Tendsto y Filter.atTop (nhds 0)} = (fun (v : X) => v + A.lyapunovPerronGraphMap P N hs hu hα hN hsmall v) '' Set.range ⇑P

The stable set of the equilibrium 0 is a graph over the range of P. When the nonlinearity fixes the origin, the initial values of the solutions of y' = A y + N y on [0, ∞) that tend to 0 are exactly the points v + graph map v with v in the range of P. Thus the global stable set is a Lipschitz graph for a globally small nonlinearity.