Peetre's compact-error estimate

An estimate ‖x‖ ≤ C * ‖T x‖ + ‖K x‖, with K compact, forces the kernel of T to be finite dimensional. If the domain is complete, the estimate also makes T bounded below on any closed subspace disjoint from its kernel. If the kernel is complemented, the range of T is closed. In real or complex Banach spaces the finite-dimensional kernel is automatically complemented.

This is the functional-analytic step that turns an elliptic estimate with a compact interior error into finite-dimensional kernel and closed range. It does not assert finite-dimensional cokernel: that requires a corresponding estimate for the adjoint or another argument.

The sequential form says that a bounded sequence whose T-images converge has a convergent subsequence. Its limit solves the limiting equation. No completeness of either target space is needed; the compact-error target may even be seminormed.

The argument uses Mathlib's Riesz lemma and uniform-inducing maps, and the compact-operator subsequence API in TauCeti.Analysis.Normed.Operator.Compact.Basic. The normalization argument extends the one for 1 - K in IsCompactOperator.exists_pos_mul_norm_le_of_disjoint_ker to operators with distinct targets for the principal term and the compact error.

References

• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.1: estimates with a compact error in the Fredholm criterion.

theorem ContinuousLinearMap.finiteDimensional_ker_of_compact_estimate {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {C : ℝ} [CompleteSpace 𝕜] [SeminormedAddCommGroup F] [Module 𝕜 F] (T : E →L[𝕜] F) {K : E →L[𝕜] G} (hK : IsCompactOperator ⇑K) (hbound : ∀ (x : E), ‖x‖ ≤ C * ‖T x‖ + ‖K x‖) : FiniteDimensional 𝕜 ↥(↑T).ker

An operator satisfying an a priori estimate with a compact error has finite-dimensional kernel. The domain and the target spaces need not be complete, and the target spaces need only be seminormed.

theorem ContinuousLinearMap.exists_subseq_tendsto_of_compact_estimate {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {C : ℝ} [CompleteSpace E] [NormedAddCommGroup F] [Module 𝕜 F] (T : E →L[𝕜] F) {K : E →L[𝕜] G} (hK : IsCompactOperator ⇑K) (hbound : ∀ (x : E), ‖x‖ ≤ C * ‖T x‖ + ‖K x‖) {R : ℝ} {v : ℕ → E} (hvbound : ∀ (n : ℕ), ‖v n‖ ≤ R) {y : F} (hTv : Filter.Tendsto (fun (n : ℕ) => T (v n)) Filter.atTop (nhds y)) : ∃ (x : E) (ψ : ℕ → ℕ), StrictMono ψ ∧ Filter.Tendsto (fun (n : ℕ) => v (ψ n)) Filter.atTop (nhds x) ∧ T x = y

Under a compact-error estimate, a bounded sequence whose operator images converge has a convergent subsequence. The subsequential limit maps to the prescribed limit of the images.

theorem ContinuousLinearMap.exists_pos_mul_norm_le_of_compact_estimate {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {C : ℝ} [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {K : E →L[𝕜] G} (hK : IsCompactOperator ⇑K) (hbound : ∀ (x : E), ‖x‖ ≤ C * ‖T x‖ + ‖K x‖) {M : Submodule 𝕜 E} (hM : IsClosed ↑M) (hdisj : Disjoint (↑T).ker M) : ∃ (c : ℝ), 0 < c ∧ ∀ x ∈ M, c * ‖x‖ ≤ ‖T x‖

A compact-error estimate makes an operator bounded below on every closed subspace disjoint from its kernel.

theorem ContinuousLinearMap.isClosed_range_of_compact_estimate_of_closedComplemented {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {C : ℝ} [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {K : E →L[𝕜] G} (hK : IsCompactOperator ⇑K) (hbound : ∀ (x : E), ‖x‖ ≤ C * ‖T x‖ + ‖K x‖) (hker : (↑T).ker.ClosedComplemented) : IsClosed ↑(↑T).range

A compact-error estimate gives closed range when the kernel is complemented. No completeness of the scalar field or either target space is required.

theorem ContinuousLinearMap.isClosed_range_of_compact_estimate {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup G] [NormedSpace 𝕜 G] {C : ℝ} [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) {K : E →L[𝕜] G} [IsRCLikeNormedField 𝕜] [CompleteSpace 𝕜] (hK : IsCompactOperator ⇑K) (hbound : ∀ (x : E), ‖x‖ ≤ C * ‖T x‖ + ‖K x‖) : IsClosed ↑(↑T).range

Peetre's lemma: a compact-error estimate gives closed range over real or complex scalars. Together with finiteDimensional_ker_of_compact_estimate, this proves the upper semi-Fredholm property. No completeness of the codomain is required.