Documentation

TauCeti.Analysis.ODE.Linear

Flows of bounded linear operators #

The operator exponential of a bounded endomorphism A gives a linear flow (t, x) ↦ exp (t A) x. For a symmetric operator on a finite-dimensional real inner-product space, its ordered orthonormal eigenbasis makes the asymptotic directions of this flow explicit.

This file proves the linear spectral model used by the stable-manifold theorem. For the flow of a symmetric operator T, a vector converges to zero in forward time exactly when it belongs to the negative spectral subspace of T, and it converges in backward time exactly when it belongs to the positive spectral subspace. No invertibility hypothesis is needed: a component in the zero eigenspace is constant and therefore belongs to neither asymptotic set unless it vanishes. The negative-gradient convention used by Morse theory is recovered by applying these to -T.

Main declarations #

References #

M. Audin and M. Damian, Morse Theory and Floer Homology, Springer Universitext, 2014, Chapter 2.

source
noncomputable def ContinuousLinearMap.flow {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) :
Flow ℝ X

The linear flow generated by a bounded endomorphism A, whose time-t map is exp (t • A).

Equations
Instances For
    source
    @[simp]
    theorem ContinuousLinearMap.flow_apply {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) (t : ℝ) (x : X) :
    A.flow.toFun t x = (NormedSpace.exp (t • A)) x

    The flow generated by A is the operator exponential exp (t • A).

    source
    @[simp]
    theorem ContinuousLinearMap.flow_neg {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (A : X →L[ℝ] X) :
    (-A).flow = A.flow.reverse

    Negating the generator reverses its linear flow.

    source
    theorem ContinuousLinearMap.norm_exp_smul_apply_le_mul_norm_of_le {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] {A : X →L[ℝ] X} {t c M K : ℝ} {w v : X} (hflow : ‖(NormedSpace.exp (t • A)) w‖ ≤ c * ‖w‖) (hop : ‖w‖ ≤ M * ‖v‖) (hc : 0 ≤ c) (hMK : M ≤ K) :
    ‖(NormedSpace.exp (t • A)) w‖ ≤ K * c * ‖v‖

    Combine an exponential-flow estimate with a comparison of the initial-vector norms, enlarging the latter estimate's constant from M to K.

    source
    theorem LinearMap.IsSymmetric.eigenvectorBasis_repr_flow_neg_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →L[ℝ] E} (hT : (↑T).IsSymmetric) (hn : Module.finrank ℝ E = n) (t : ℝ) (v : E) (i : Fin n) :
    ((hT.eigenvectorBasis hn).toBasis.repr ((-T).flow.toFun t v)) i = Real.exp (-(t * hT.eigenvalues hn i)) * ((hT.eigenvectorBasis hn).toBasis.repr v) i

    In an ordered orthonormal eigenbasis, the flow generated by -T multiplies the ith coordinate by exp (-t * λᵢ).

    source
    @[simp]
    theorem LinearMap.IsSymmetric.stableSet_flow_eq_negativeSpectralSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →L[ℝ] E} (hT : (↑T).IsSymmetric) (hn : Module.finrank ℝ E = n) :
    T.flow.stableSet 0 = ↑(hT.negativeSpectralSubspace hn)

    For a finite-dimensional symmetric operator T, the stable set of zero under the linear flow generated by T is exactly the negative spectral subspace of T.

    source
    @[simp]
    theorem LinearMap.IsSymmetric.unstableSet_flow_eq_positiveSpectralSubspace {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {n : ℕ} {T : E →L[ℝ] E} (hT : (↑T).IsSymmetric) (hn : Module.finrank ℝ E = n) :
    T.flow.unstableSet 0 = ↑(hT.positiveSpectralSubspace hn)

    For a finite-dimensional symmetric operator T, the unstable set of zero under the linear flow generated by T is exactly the positive spectral subspace of T.