The Lyapunov--Perron fixed point

Let A be a bounded operator on a real Banach space X and let P be a bounded operator 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:

‖exp (t A) (P v)‖ ≤ K exp (-α t) ‖v‖ for t ≥ 0, and ‖exp (t A) (v - P v)‖ ≤ K exp (α t) ‖v‖ for t ≤ 0.

These are the two estimates carried by an exponential dichotomy of y' = A y, but nothing below needs P to be idempotent or to commute with A: they are used here purely as a forward and a backward exponential estimate, and P v and v - P v are not assumed to be the components of a splitting. For a globally ε-Lipschitz nonlinearity N, the Lyapunov--Perron integral equation

`y t = exp (t A) (P ξ) + ∫₀ᵗ exp ((t - s) A) (P (N (y s))) ds

• ∫ₜ^∞ exp ((t - s) A) (N (y s) - P (N (y s))) ds`

builds a bounded forward solution of y' = A y + N y from the input parameter ξ.

This file shows that when 2 K ε < α the right-hand side is a contraction of the complete space of bounded continuous functions on [0, ∞). Its unique fixed point ContinuousLinearMap.lyapunovPerronSolution depends Lipschitz-continuously on ξ and solves y' = A y + N y on [0, ∞). Conversely, once P is idempotent and commutes with A, every solution that stays bounded on [0, ∞) is the fixed point whose input parameter is its initial value. The initial values of the bounded forward solutions are therefore exactly the points x with lyapunovPerronSolution x 0 = x; their P-component is free and determines the rest Lipschitz-continuously.

The fixed points also satisfy weighted bounds: for every β ≥ 0 with 2 K ε < α - β, the difference of two Lyapunov--Perron solutions is bounded by a constant times exp (-β t). For β > 0, they therefore approach each other exponentially. When N 0 = 0 every Lyapunov--Perron solution tends to the equilibrium 0, and the bounded forward solutions are exactly the forward solutions tending to 0: the initial values above form the stable set of the equilibrium. This is the analytic core of the Lyapunov--Perron proof of the stable-manifold theorem at a hyperbolic equilibrium, where the local stable manifold is read off from the initial values of these fixed points after the nonlinearity has been cut off.

Main declarations

• ContinuousLinearMap.lyapunovPerronIntegral: the two integral terms of the equation, for an arbitrary forcing term g.
• ContinuousLinearMap.hasDerivAt_lyapunovPerronIntegral: the integral terms solve the forced linear equation y' = A y + g.
• ContinuousLinearMap.norm_lyapunovPerronIntegral_le_mul_exp: under the forward and backward exponential estimates, a forcing term bounded by M exp (-β s), for 0 ≤ β < α, produces integral terms bounded by 2 K M exp (-β t) / (α - β) in forward time; ContinuousLinearMap.norm_lyapunovPerronIntegral_le is the case β = 0.
• ContinuousLinearMap.lyapunovPerronMap: the Lyapunov--Perron operator on bounded continuous functions on [0, ∞).
• ContinuousLinearMap.contractingWith_lyapunovPerronMap: it is a contraction when 2 K ε < α.
• ContinuousLinearMap.lyapunovPerronSolution: its unique fixed point.
• ContinuousLinearMap.lipschitzWith_lyapunovPerronSolution: the fixed point is Lipschitz in ξ.
• ContinuousLinearMap.isIntegralCurveOn_lyapunovPerronSolution: the fixed point solves y' = A y + N y on [0, ∞).
• ContinuousLinearMap.eqOn_lyapunovPerronSolution_of_isIntegralCurveOn: when P is idempotent and commutes with A, every bounded forward solution is a Lyapunov--Perron solution.
• ContinuousLinearMap.exists_isIntegralCurveOn_bounded_iff: the initial values of bounded forward solutions are the fixed points of ξ ↦ lyapunovPerronSolution ξ 0.
• ContinuousLinearMap.apply_lyapunovPerronSolution_zero: the P-component of that initial value is P ξ.
• ContinuousLinearMap.lyapunovPerronSolution_lyapunovPerronSolution_zero: restarting a Lyapunov--Perron solution from its initial value reproduces it.
• ContinuousLinearMap.norm_lyapunovPerronSolution_sub_le: the difference of two Lyapunov--Perron solutions has a weighted bound for every β ≥ 0 with 2 K ε < α - β, giving exponential approach when β > 0.
• ContinuousLinearMap.norm_lyapunovPerronSolution_le, ContinuousLinearMap.tendsto_lyapunovPerronSolution: when N 0 = 0, Lyapunov--Perron solutions satisfy the corresponding weighted bounds and tend to 0.
• ContinuousLinearMap.norm_le_of_isIntegralCurveOn_of_bounded: bounded forward solutions satisfy the corresponding weighted bounds, which give exponential decay when β > 0.
• ContinuousLinearMap.exists_isIntegralCurveOn_tendsto_iff: the initial values of forward solutions tending to 0 are the fixed points of ξ ↦ lyapunovPerronSolution ξ 0.

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.

noncomputable def ContinuousLinearMap.lyapunovPerronIntegral {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (A P : X →L[ℝ] X) (g : ℝ → X) (t : ℝ) : X

The integral terms of the Lyapunov--Perron equation with forcing term g:

∫₀ᵗ exp ((t - s) A) (P (g s)) ds - ∫ₜ^∞ exp ((t - s) A) (g s - P (g s)) ds.

The first integral propagates the part P (g s) of the forcing forward from time 0; the second propagates the remaining part g s - P (g s) backward from time ∞.

Equations

• A.lyapunovPerronIntegral P g t = (∫ (s : ℝ) in 0..t, (NormedSpace.exp ((t - s) • A)) (P (g s))) - ∫ (s : ℝ) in Set.Ioi t, (NormedSpace.exp ((t - s) • A)) (g s - P (g s))

theorem ContinuousLinearMap.integrableOn_lyapunovPerron_unstable {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (t : ℝ) (hg : ContinuousOn g (Set.Ioi t)) (hgM : ∀ s ∈ Set.Ioi t, ‖g s‖ ≤ M) : MeasureTheory.IntegrableOn (fun (s : ℝ) => (NormedSpace.exp ((t - s) • A)) (g s - P (g s))) (Set.Ioi t) MeasureTheory.volume

Under the backward exponential estimate, a forcing term that is continuous and bounded by M on (t, ∞) makes the unstable integrand of the Lyapunov--Perron equation integrable there.

theorem ContinuousLinearMap.norm_setIntegral_lyapunovPerron_unstable_le_mul_exp {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) {β : ℝ} (hαβ : 0 < ↑α + β) (t : ℝ) (hgM : ∀ s ∈ Set.Ioi t, ‖g s‖ ≤ M * Real.exp (-β * s)) : ‖∫ (s : ℝ) in Set.Ioi t, (NormedSpace.exp ((t - s) • A)) (g s - P (g s))‖ ≤ ↑K * M / (↑α + β) * Real.exp (-β * t)

Under the backward exponential estimate, the unstable integral of a forcing term bounded by M exp (-β s) on (t, ∞) is bounded by K M exp (-β t) / (α + β), provided α + β > 0.

theorem ContinuousLinearMap.norm_setIntegral_lyapunovPerron_unstable_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (t : ℝ) (hgM : ∀ s ∈ Set.Ioi t, ‖g s‖ ≤ M) : ‖∫ (s : ℝ) in Set.Ioi t, (NormedSpace.exp ((t - s) • A)) (g s - P (g s))‖ ≤ ↑K * M / ↑α

Under the backward exponential estimate, the unstable integral of a forcing term bounded by M on (t, ∞) is bounded by K M / α.

theorem ContinuousLinearMap.norm_intervalIntegral_lyapunovPerron_stable_le_mul_exp {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} {t : ℝ} (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) {β : ℝ} (hβα : β < ↑α) (ht : 0 ≤ t) (hgM : ∀ s ∈ Set.Icc 0 t, ‖g s‖ ≤ M * Real.exp (-β * s)) : ‖∫ (s : ℝ) in 0..t, (NormedSpace.exp ((t - s) • A)) (P (g s))‖ ≤ ↑K * M / (↑α - β) * Real.exp (-β * t)

Under the forward exponential estimate, the stable integral of a forcing term bounded by M exp (-β s) on [0, t] is bounded by K M exp (-β t) / (α - β) in forward time, provided β < α.

theorem ContinuousLinearMap.norm_intervalIntegral_lyapunovPerron_stable_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} {t : ℝ} (hs : ∀ (t : ℝ), 0 ≤ t → ∀ (v : X), ‖(NormedSpace.exp (t • A)) (P v)‖ ≤ ↑K * Real.exp (-↑α * t) * ‖v‖) (hα : 0 < α) (ht : 0 ≤ t) (hgM : ∀ s ∈ Set.Icc 0 t, ‖g s‖ ≤ M) : ‖∫ (s : ℝ) in 0..t, (NormedSpace.exp ((t - s) • A)) (P (g s))‖ ≤ ↑K * M / ↑α

Under the forward exponential estimate, the stable integral of a forcing term bounded by M on [0, t] is bounded by K M / α in forward time.

theorem ContinuousLinearMap.norm_lyapunovPerronIntegral_le_mul_exp {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} {t : ℝ} (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 ≤ β) (hβα : β < ↑α) (hgM : ∀ (s : ℝ), 0 ≤ s → ‖g s‖ ≤ M * Real.exp (-β * s)) (ht : 0 ≤ t) : ‖A.lyapunovPerronIntegral P g t‖ ≤ 2 * ↑K * M / (↑α - β) * Real.exp (-β * t)

Under the forward and backward exponential estimates, the integral terms of the Lyapunov--Perron equation with a forcing term bounded by M exp (-β s) in forward time are bounded by 2 K M exp (-β t) / (α - β) in forward time, for a rate 0 ≤ β < α.

theorem ContinuousLinearMap.norm_lyapunovPerronIntegral_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} {t : ℝ} (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 < α) (hgM : ∀ (s : ℝ), ‖g s‖ ≤ M) (ht : 0 ≤ t) : ‖A.lyapunovPerronIntegral P g t‖ ≤ 2 * ↑K * M / ↑α

Under the forward and backward exponential estimates, the integral terms of the Lyapunov--Perron equation with a forcing term bounded by M are bounded by 2 K M / α in forward time.

theorem ContinuousLinearMap.lyapunovPerronIntegral_sub {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g₁ g₂ : ℝ → X} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (hg₁ : Continuous g₁) (hg₁M : ∀ (s : ℝ), ‖g₁ s‖ ≤ M) (hg₂ : Continuous g₂) {M₂ : ℝ} (hg₂M : ∀ (s : ℝ), ‖g₂ s‖ ≤ M₂) (t : ℝ) : A.lyapunovPerronIntegral P g₁ t - A.lyapunovPerronIntegral P g₂ t = A.lyapunovPerronIntegral P (g₁ - g₂) t

The integral terms of the Lyapunov--Perron equation are linear in the forcing term.

@[simp]

theorem ContinuousLinearMap.lyapunovPerronIntegral_smul {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A P : X →L[ℝ] X} (c : ℝ) (g : ℝ → X) (t : ℝ) : A.lyapunovPerronIntegral P (c • g) t = c • A.lyapunovPerronIntegral P g t

The Lyapunov--Perron integral is homogeneous in its forcing term.

theorem ContinuousLinearMap.hasDerivAt_lyapunovPerronIntegral {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (hg : Continuous g) (hgM : ∀ (s : ℝ), ‖g s‖ ≤ M) (t : ℝ) : HasDerivAt (A.lyapunovPerronIntegral P g) (A (A.lyapunovPerronIntegral P g t) + g t) t

Under the backward exponential estimate, the integral terms of the Lyapunov--Perron equation solve the forced linear equation y' = A y + g.

theorem ContinuousLinearMap.continuous_lyapunovPerronIntegral {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (hg : Continuous g) (hgM : ∀ (s : ℝ), ‖g s‖ ≤ M) : Continuous (A.lyapunovPerronIntegral P g)

Under the backward exponential estimate, the integral terms of the Lyapunov--Perron equation are continuous in time.

theorem ContinuousLinearMap.apply_lyapunovPerronIntegral_zero {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} {M : ℝ} {g : ℝ → X} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (hP : IsIdempotentElem P) (hAP : Commute A P) (hg : ContinuousOn g (Set.Ioi 0)) (hgM : ∀ s ∈ Set.Ioi 0, ‖g s‖ ≤ M) : P (A.lyapunovPerronIntegral P g 0) = 0

When P is idempotent and commutes with A, the integral terms of the Lyapunov--Perron equation have vanishing P-component at time 0: there only the backward integral of the parts g s - P (g s) survives.

theorem ContinuousLinearMap.eq_zero_of_norm_exp_smul_apply_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] {A P : X →L[ℝ] X} {K α : NNReal} (hu : ∀ t ≤ 0, ∀ (v : X), ‖(NormedSpace.exp (t • A)) (v - P v)‖ ≤ ↑K * Real.exp (↑α * t) * ‖v‖) (hα : 0 < α) (hAP : Commute A P) {v : X} (hv : P v = 0) {C : ℝ} (hC : ∀ (t : ℝ), 0 ≤ t → ‖(NormedSpace.exp (t • A)) v‖ ≤ C) : v = 0

Under the backward exponential estimate, a vector v with P v = 0 whose forward orbit t ↦ exp (t A) v stays bounded is zero, provided P commutes with A.

This is the linear uniqueness statement behind the converse of the Lyapunov--Perron construction: the component of a forward solution not seen by P cannot stay bounded unless it vanishes.

noncomputable def ContinuousLinearMap.lyapunovPerronMap {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) (ξ : X) (γ : BoundedContinuousFunction NNReal X) : BoundedContinuousFunction NNReal X

The Lyapunov--Perron operator of y' = A y + N y with input parameter ξ, acting on bounded continuous functions on [0, ∞):

γ ↦ (t ↦ exp (t A) (P ξ) + lyapunovPerronIntegral A P (N ∘ γ) t).

Here P ξ is only the parameter in the homogeneous term. Without projection and commutation hypotheses on P, it is not identified with P (y 0).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ContinuousLinearMap.lyapunovPerronMap_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) (ξ : X) (γ : BoundedContinuousFunction NNReal X) (t : NNReal) : (A.lyapunovPerronMap P N hs hu hα hN ξ γ) t = (NormedSpace.exp (↑t • A)) (P ξ) + A.lyapunovPerronIntegral P (fun (s : ℝ) => N (γ s.toNNReal)) ↑t

theorem ContinuousLinearMap.dist_lyapunovPerronMap_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) (ξ : X) (γ η : BoundedContinuousFunction NNReal X) : dist (A.lyapunovPerronMap P N hs hu hα hN ξ γ) (A.lyapunovPerronMap P N hs hu hα hN ξ η) ≤ 2 * ↑K * ↑ε / ↑α * dist γ η

The Lyapunov--Perron operator is 2 K ε / α-Lipschitz.

theorem ContinuousLinearMap.contractingWith_lyapunovPerronMap {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) : ContractingWith (2 * K * ε / α) (A.lyapunovPerronMap P N hs hu hα hN ξ)

When 2 K ε < α, the Lyapunov--Perron operator is a contraction.

theorem ContinuousLinearMap.dist_lyapunovPerronMap_lyapunovPerronMap_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) (ξ ζ : X) (γ : BoundedContinuousFunction NNReal X) : dist (A.lyapunovPerronMap P N hs hu hα hN ξ γ) (A.lyapunovPerronMap P N hs hu hα hN ζ γ) ≤ ↑K * dist ξ ζ

Changing the input parameter moves the Lyapunov--Perron operator by at most K ‖ξ - ζ‖.

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

The Lyapunov--Perron solution with input parameter ξ: the unique fixed point of the Lyapunov--Perron operator, when 2 K ε < α.

Equations

• A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ = ContractingWith.fixedPoint (A.lyapunovPerronMap P N hs hu hα hN ξ) ⋯

theorem ContinuousLinearMap.isFixedPt_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 * ε < α) (ξ : X) : Function.IsFixedPt (A.lyapunovPerronMap P N hs hu hα hN ξ) (A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ)

theorem ContinuousLinearMap.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 * ε < α) (ξ : X) (t : NNReal) : (A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) t = (NormedSpace.exp (↑t • A)) (P ξ) + A.lyapunovPerronIntegral P (fun (s : ℝ) => N ((A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) s.toNNReal)) ↑t

The Lyapunov--Perron solution satisfies the Lyapunov--Perron integral equation.

theorem ContinuousLinearMap.eq_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 * ε < α) {ξ : X} {γ : BoundedContinuousFunction NNReal X} (hγ : ∀ (t : NNReal), γ t = (NormedSpace.exp (↑t • A)) (P ξ) + A.lyapunovPerronIntegral P (fun (s : ℝ) => N (γ s.toNNReal)) ↑t) : γ = A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ

The Lyapunov--Perron solution is the only bounded continuous solution of the Lyapunov--Perron integral equation.

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

The Lyapunov--Perron solution depends Lipschitz-continuously on the input parameter.

@[simp]

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

If the nonlinearity vanishes at the origin, the Lyapunov--Perron solution with zero input parameter is the zero solution.

theorem ContinuousLinearMap.isIntegralCurveOn_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 * ε < α) (ξ : X) : IsIntegralCurveOn (fun (t : ℝ) => (A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) t.toNNReal) (fun (x : ℝ) (y : X) => A y + N y) (Set.Ici 0)

The Lyapunov--Perron solution solves y' = A y + N y on [0, ∞).

Bounded forward solutions are Lyapunov--Perron solutions

When P is idempotent and commutes with A, every bounded forward solution of y' = A y + N y is the Lyapunov--Perron solution with input parameter its initial value. The initial values of the bounded forward solutions are therefore exactly the fixed points of ξ ↦ lyapunovPerronSolution ξ 0: the graph, over the range of P, of a Lipschitz map into the kernel of P.

@[simp]

theorem ContinuousLinearMap.lyapunovPerronSolution_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.lyapunovPerronSolution P N hs hu hα hN hsmall (P ξ) = A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ

When P is idempotent, the Lyapunov--Perron solution depends only on the P-component of its input parameter.

@[simp]

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

When P is idempotent and commutes with A, the P-component of the initial value of a Lyapunov--Perron solution is the P-component of its input parameter.

@[simp]

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

When P is idempotent and commutes with A, restarting a Lyapunov--Perron solution from its own initial value reproduces it. Hence every initial value lyapunovPerronSolution ξ 0 is a fixed point of x ↦ lyapunovPerronSolution x 0, and the P-component P ξ can be prescribed arbitrarily.

theorem ContinuousLinearMap.eqOn_lyapunovPerronSolution_of_isIntegralCurveOn {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) {y : ℝ → X} (hy : IsIntegralCurveOn y (fun (x : ℝ) (y : X) => A y + N y) (Set.Ici 0)) {B : ℝ} (hB : ∀ t ∈ Set.Ici 0, ‖y t‖ ≤ B) : Set.EqOn y (fun (t : ℝ) => (A.lyapunovPerronSolution P N hs hu hα hN hsmall (y 0)) t.toNNReal) (Set.Ici 0)

Bounded forward solutions are Lyapunov--Perron solutions. When P is idempotent and commutes with A, every solution of y' = A y + N y on [0, ∞) that stays bounded there agrees on [0, ∞) with the Lyapunov--Perron solution whose input parameter is its initial value.

theorem ContinuousLinearMap.exists_isIntegralCurveOn_bounded_iff {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) ↔ (A.lyapunovPerronSolution P N hs hu hα hN hsmall x) 0 = x

The Lyapunov--Perron description of bounded forward solutions. When P is idempotent and commutes with A, a point is the initial value of a solution of y' = A y + N y that stays bounded on [0, ∞) exactly when it is the initial value of the Lyapunov--Perron solution with itself as input parameter.

Exponential decay of Lyapunov--Perron solutions

For every β ≥ 0 in the spectral gap left by the nonlinearity, 2 K ε < α - β, the difference of two Lyapunov--Perron solutions is bounded by a constant times exp (-β t); when β > 0, this gives exponential approach. When N 0 = 0 the solution with input parameter 0 is the zero solution, so all Lyapunov--Perron solutions tend to 0, and the bounded forward solutions are exactly the forward solutions tending to the equilibrium 0.

theorem ContinuousLinearMap.norm_lyapunovPerronMap_sub_le_mul_exp {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) {β : ℝ} (hβ : 0 ≤ β) (hβα : β < ↑α) (ξ ζ : X) {γ η : BoundedContinuousFunction NNReal X} {R : ℝ} (hγη : ∀ (t : NNReal), ‖γ t - η t‖ ≤ R * Real.exp (-β * ↑t)) (t : NNReal) : ‖(A.lyapunovPerronMap P N hs hu hα hN ξ γ) t - (A.lyapunovPerronMap P N hs hu hα hN ζ η) t‖ ≤ (↑K * ‖ξ - ζ‖ + 2 * ↑K * ↑ε * R / (↑α - β)) * Real.exp (-β * ↑t)

The weighted form of dist_lyapunovPerronMap_le: if two curves stay within R exp (-β t) of each other in forward time, for a rate 0 ≤ β < α, then their images under the Lyapunov--Perron operators with input parameters ξ and ζ stay within (K ‖ξ - ζ‖ + 2 K ε R / (α - β)) exp (-β t) of each other.

theorem ContinuousLinearMap.norm_lyapunovPerronSolution_sub_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 * ε < α) {β : ℝ} (hβ : 0 ≤ β) (hβα : 2 * ↑K * ↑ε < ↑α - β) (ξ ζ : X) (t : NNReal) : ‖(A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) t - (A.lyapunovPerronSolution P N hs hu hα hN hsmall ζ) t‖ ≤ ↑K / (1 - 2 * ↑K * ↑ε / (↑α - β)) * Real.exp (-β * ↑t) * ‖ξ - ζ‖

Weighted bound for the difference of Lyapunov--Perron solutions. For β ≥ 0 with 2 K ε < α - β, the difference is bounded by a constant times exp (-β t), with the constant proportional to the distance between the input parameters. In particular, the solutions approach each other exponentially when β > 0.

theorem ContinuousLinearMap.norm_lyapunovPerronSolution_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) {β : ℝ} (hβ : 0 ≤ β) (hβα : 2 * ↑K * ↑ε < ↑α - β) (ξ : X) (t : NNReal) : ‖(A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) t‖ ≤ ↑K / (1 - 2 * ↑K * ↑ε / (↑α - β)) * Real.exp (-β * ↑t) * ‖ξ‖

Weighted bound for Lyapunov--Perron solutions. If the nonlinearity vanishes at the origin, then for β ≥ 0 with 2 K ε < α - β every Lyapunov--Perron solution is bounded by a constant times exp (-β t). In particular, it decays exponentially to 0 when β > 0.

theorem ContinuousLinearMap.norm_lyapunovPerronSolution_le_mul_norm {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) (t : NNReal) : ‖(A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) t‖ ≤ ↑K / (1 - 2 * ↑K * ↑ε / ↑α) * ‖ξ‖

The unweighted bound for a Lyapunov--Perron solution whose nonlinearity vanishes at the origin.

theorem ContinuousLinearMap.tendsto_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 * ε < α) (hN0 : N 0 = 0) (ξ : X) : Filter.Tendsto (fun (t : ℝ) => (A.lyapunovPerronSolution P N hs hu hα hN hsmall ξ) t.toNNReal) Filter.atTop (nhds 0)

If the nonlinearity vanishes at the origin, every Lyapunov--Perron solution tends to 0 in forward time.

theorem ContinuousLinearMap.norm_le_of_isIntegralCurveOn_of_bounded {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) (hP : IsIdempotentElem P) (hAP : Commute A P) {β : ℝ} (hβ : 0 ≤ β) (hβα : 2 * ↑K * ↑ε < ↑α - β) {y : ℝ → X} (hy : IsIntegralCurveOn y (fun (x : ℝ) (y : X) => A y + N y) (Set.Ici 0)) {B : ℝ} (hB : ∀ t ∈ Set.Ici 0, ‖y t‖ ≤ B) {t : ℝ} (ht : 0 ≤ t) : ‖y t‖ ≤ ↑K / (1 - 2 * ↑K * ↑ε / (↑α - β)) * Real.exp (-β * t) * ‖y 0‖

Weighted bounds for bounded forward solutions. When the nonlinearity vanishes at the origin and P is idempotent and commutes with A, every solution of y' = A y + N y that stays bounded on [0, ∞) is bounded by a constant times exp (-β t) for every β ≥ 0 with 2 K ε < α - β. In particular, it decays exponentially to 0 when β > 0.

theorem ContinuousLinearMap.exists_isIntegralCurveOn_tendsto_iff {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) (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 ∧ Filter.Tendsto y Filter.atTop (nhds 0)) ↔ (A.lyapunovPerronSolution P N hs hu hα hN hsmall x) 0 = x

The Lyapunov--Perron description of the stable set. When the nonlinearity vanishes at the origin and P is idempotent and commutes with A, a point is the initial value of a solution of y' = A y + N y on [0, ∞) tending to the equilibrium 0 exactly when it is the initial value of the Lyapunov--Perron solution with itself as input parameter.