Noninjective limits of trajectory operators

An operator limit with a nonzero kernel supplies the vanishing direction required by the canonical non-Fredholm criterion in TrajectoryOperator.Degenerate.

theorem TauCeti.WeakDerivStep.not_isFredholm_trajectoryOperator_of_not_injective_of_tendsto_atTop {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {A : ℝ → E →L[ℝ] E} (AL : ↥(MeasureTheory.Lp (E →L[ℝ] E) ⊤ (MeasureTheory.volume.restrict ↑⊤))) (hAL : ↑↑AL =ᵐ[MeasureTheory.volume.restrict ↑⊤] A) {Aplus : E →L[ℝ] E} (htop : Filter.Tendsto A Filter.atTop (nhds Aplus)) (hinj : ¬Function.Injective ⇑Aplus) : ¬(trajectoryOperator AL).IsFredholm

A noninjective limit at +∞ destroys the Fredholm property. If A converges at +∞ to an operator which is not injective, then the trajectory operator D_A u = u' + A u from W^{1,2}(ℝ, E) to L²(ℝ, E) is not Fredholm.

theorem TauCeti.WeakDerivStep.not_isFredholm_trajectoryOperator_of_not_injective_of_tendsto_atBot {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {A : ℝ → E →L[ℝ] E} (AL : ↥(MeasureTheory.Lp (E →L[ℝ] E) ⊤ (MeasureTheory.volume.restrict ↑⊤))) (hAL : ↑↑AL =ᵐ[MeasureTheory.volume.restrict ↑⊤] A) {Aminus : E →L[ℝ] E} (hbot : Filter.Tendsto A Filter.atBot (nhds Aminus)) (hinj : ¬Function.Injective ⇑Aminus) : ¬(trajectoryOperator AL).IsFredholm

A noninjective limit at -∞ destroys the Fredholm property. If A converges at -∞ to an operator which is not injective, then the trajectory operator D_A u = u' + A u from W^{1,2}(ℝ, E) to L²(ℝ, E) is not Fredholm.