The a priori estimate of a closed-range operator

A continuous linear map T : E →L[𝕜] F between Banach spaces with closed range fails to be bounded below only in the direction of its kernel. When that kernel is complemented, this file makes the failure quantitative, in the classical form

‖x‖ ≤ C * ‖T x‖ + ‖P x‖,

where P is a continuous projection of E onto ker T. When ker T is finite-dimensional, as for a Fredholm operator, P x lies in a finite-dimensional space, and over a proper normed field, such as ℝ or ℂ, the finite-rank projection P is a compact operator.

Main declarations

• ContinuousLinearMap.exists_norm_le_mul_norm_of_mem: a closed-range operator is bounded below on any topological complement of its kernel.
• ContinuousLinearMap.exists_norm_le_mul_norm_add_norm_projectionL: the a priori estimate against the projection onto the kernel determined by a chosen complement.
• ContinuousLinearMap.exists_projection_norm_le: the same estimate with the complement discharged, so that the only data left is a continuous projection with range the kernel.

TauCeti.Analysis.Fredholm.Proper uses the estimate below to prove that a map with Fredholm derivative is proper near a point (Smale, An infinite dimensional version of Sard's theorem, Amer. J. Math. 87 (1965)); local properness is in turn what makes the critical values of such a map locally closed, and hence what upgrades Sard--Smale from a density statement to a residuality statement.

theorem ContinuousLinearMap.exists_norm_le_mul_norm_of_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {X₁ : Submodule 𝕜 E} [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (hclosed : IsClosed ↑(↑T).range) (h : Submodule.IsTopCompl (↑T).ker X₁) : ∃ C > 0, ∀ x ∈ X₁, ‖x‖ ≤ C * ‖T x‖

A closed-range operator is bounded below off its kernel. On any topological complement X₁ of ker T there is a constant C > 0 with ‖x‖ ≤ C * ‖T x‖ for every x ∈ X₁.

theorem ContinuousLinearMap.exists_norm_le_mul_norm_add_norm_projectionL {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {X₁ : Submodule 𝕜 E} [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (hclosed : IsClosed ↑(↑T).range) (h : Submodule.IsTopCompl (↑T).ker X₁) : ∃ C > 0, ∀ (x : E), ‖x‖ ≤ C * ‖T x‖ + ‖((↑T).ker.projectionL X₁ h) x‖

The a priori estimate of a closed-range operator, stated against the projection onto the kernel along a chosen topological complement: there is a C > 0 with ‖x‖ ≤ C * ‖T x‖ + ‖P x‖ for all x, where P is that projection.

theorem ContinuousLinearMap.exists_projection_norm_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace E] [CompleteSpace F] (T : E →L[𝕜] F) (hclosed : IsClosed ↑(↑T).range) (hcompl : (↑T).ker.ClosedComplemented) : ∃ (P : E →L[𝕜] E) (C : ℝ), 0 < C ∧ IsIdempotentElem P ∧ (↑P).range = (↑T).ker ∧ ∀ (x : E), ‖x‖ ≤ C * ‖T x‖ + ‖P x‖

The a priori estimate of a closed-range operator with complemented kernel, with the complement discharged: there is a continuous projection P of E onto ker T and a constant C > 0 with ‖x‖ ≤ C * ‖T x‖ + ‖P x‖.

When ker T is finite-dimensional, P x lies in the finite-dimensional space ker T, and over a proper normed field the finite-rank projection P is compact. This says that a Fredholm operator is bounded below "up to a compact error".