The trajectory operator with a degenerate limit is not Fredholm

Let A : ℝ → End(F) be an essentially bounded family of operators on a real Banach space F. If some nonzero vector v satisfies A(s) v → 0 as s → ∞ (or as s → -∞), for instance because A has a limit A⁺ with A⁺ v = 0, then the trajectory operator

D_A u = u' + A u : W^{1,2}(ℝ, F) → L²(ℝ, F)

is not Fredholm. Together with TauCeti.WeakDerivStep.isFredholm_trajectoryOperator_of_hasLyapunovForm, this shows that for a continuous family of operators on a finite-dimensional inner product space with symmetric limits A±, D_A is Fredholm exactly when both limits are injective, that is, invertible (TauCeti.WeakDerivStep.isFredholm_trajectoryOperator_iff, in TauCeti.Analysis.ODE.EnergyEstimate.Lyapunov).

The proof constructs an escaping approximate kernel. Fix a smooth bump ψ supported in (-1, 1), and put uₙ(s) = (n + 1)^(-1/2) ψ((s - cₙ) / (n + 1)) v up to a normalizing constant, with centres cₙ so far out that ‖A(s) v‖ ≤ 1 / (n + 1) on the support of uₙ and the supports are pairwise disjoint. Then ‖uₙ‖_{L²} = 1, ‖uₙ'‖_{L²} is of order 1 / (n + 1) and ‖D_A uₙ‖_{L²} → 0, while ‖uₙ - uₘ‖²_{L²} = 2 for n ≠ m. A Fredholm operator has closed range and a finite-dimensional complemented kernel, so a bounded sequence on which it tends to zero has a convergent subsequence (ContinuousLinearMap.tendsto_subseq_of_cauchySeq_comp). The sequence uₙ has none.

Main declarations

• TauCeti.WeakDerivStep.not_isFredholm_trajectoryOperator_of_tendsto_atTop and TauCeti.WeakDerivStep.not_isFredholm_trajectoryOperator_of_tendsto_atBot: if A(s) v → 0 at +∞ or at -∞ for some v ≠ 0, then D_A is not Fredholm.

References

• J. Robbin and D. Salamon, The spectral flow and the Maslov index, Bull. London Math. Soc. 27 (1995), 1--33, Theorem A (the operator d/ds + A(s) is Fredholm exactly when the limits are invertible).
• M. Schwarz, Morse Homology, Chapter 2 (linearized trajectory operators).

The escaping profiles

The escaping approximate kernel

theorem TauCeti.WeakDerivStep.not_isFredholm_trajectoryOperator_of_tendsto_atTop {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {A : ℝ → F →L[ℝ] F} {v : F} (hv : v ≠ 0) (hAv : Filter.Tendsto (fun (s : ℝ) => (A s) v) Filter.atTop (nhds 0)) (AL : ↥(MeasureTheory.Lp (F →L[ℝ] F) ⊤ (MeasureTheory.volume.restrict ↑⊤))) (hAL : ↑↑AL =ᵐ[MeasureTheory.volume.restrict ↑⊤] A) : ¬(trajectoryOperator AL).IsFredholm

The trajectory operator with a degenerate limit at +∞ is not Fredholm. If A(s) v → 0 as s → ∞ for some v ≠ 0, for instance because A tends to an operator A⁺ with A⁺ v = 0, then u ↦ u' + A u from W^{1,2}(ℝ, F) to L²(ℝ, F) is not Fredholm. The coefficient of the operator is any L∞ class AL of A.

theorem TauCeti.WeakDerivStep.not_isFredholm_trajectoryOperator_of_tendsto_atBot {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {A : ℝ → F →L[ℝ] F} {v : F} (hv : v ≠ 0) (hAv : Filter.Tendsto (fun (s : ℝ) => (A s) v) Filter.atBot (nhds 0)) (AL : ↥(MeasureTheory.Lp (F →L[ℝ] F) ⊤ (MeasureTheory.volume.restrict ↑⊤))) (hAL : ↑↑AL =ᵐ[MeasureTheory.volume.restrict ↑⊤] A) : ¬(trajectoryOperator AL).IsFredholm

The trajectory operator with a degenerate limit at -∞ is not Fredholm. If A(s) v → 0 as s → -∞ for some v ≠ 0, for instance because A tends to an operator A⁻ with A⁻ v = 0, then u ↦ u' + A u from W^{1,2}(ℝ, F) to L²(ℝ, F) is not Fredholm. The coefficient of the operator is any L∞ class AL of A.