An estimate modulo a compact operator gives finite-dimensional kernel and closed range

Proved

CauchyRiemannIndex.finiteDimensional_ker_isClosed_range_of_estimate

by Mazecto · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

cauchy-riemannconley-zehnder-indexfredholm-indexsobolev-spacessymplectic-geometry

Let $X$ , $Y$ , $Z$ be real Banach spaces, $T:X\to Y$ a bounded linear operator, $K:X\to Z$ a compact linear operator, and $c$ a constant such that

\|x\|_X\le c\,\|Tx\|_Y+c\,\|Kx\|_Z\qquad\text{for all }x\in X .

Then $\ker T$ is finite-dimensional and the range of $T$ is closed.

Formalization Note $T$ and $K$ are continuous linear maps X →L[ℝ] Y, X →L[ℝ] Z; compactness is IsCompactOperator K.

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic
import Mathlib.Analysis.Normed.Operator.Compact.Basic

Formal statement

namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- Wendl, Lemma 4.12 (p. 73): let `X`, `Y`, `Z` be Banach spaces, `T : X → Y` bounded,
`K : X → Z` compact, and `‖x‖ ≤ c ‖T x‖ + c ‖K x‖` for all `x`. Then `ker T` is
finite-dimensional and `im T` is closed. -/
theorem finiteDimensional_ker_isClosed_range_of_estimate {X Y Z : Type*}
    [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X]
    [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y]
    [NormedAddCommGroup Z] [NormedSpace ℝ Z] [CompleteSpace Z]
    (T : X →L[ℝ] Y) (K : X →L[ℝ] Z) (hK : IsCompactOperator K) (c : ℝ)
    (hc : ∀ x, ‖x‖ ≤ c * ‖T x‖ + c * ‖K x‖) :
    FiniteDimensional ℝ (LinearMap.ker (T : X →ₗ[ℝ] Y)) ∧ IsClosed (Set.range T) := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 4, Lemma 4.12, p. 73

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `CauchyRiemannIndex.finiteDimensional_ker_isClosed_range_of_estimate`

Setting. Real Banach spaces $X,Y,Z$ ; $T\in\mathcal L(X,Y)$ ; $K\in\mathcal L(X,Z)$ ; $c\in\mathbb R$ .

Hypotheses. $K$ is compact (IsCompactOperator K), and $\forall x\in X:\ \|x\|\le c\|Tx\|+c\|Kx\|$ .

Definitions used. Mathlib IsCompactOperator: $K$ maps a neighbourhood of $0$ into a relatively compact set. LinearMap.ker, Set.range.

Conclusion.

\dim_{\mathbb R}\ker T<\infty\quad\text{and}\quad T(X)\text{ is closed in }Y.

Degenerate cases. If $c<0$ , the hypothesis forces $\|x\|\le0$ , so $X=0$ and the conclusion holds trivially. The same happens for $c=0$ . $X=0$ is trivial.

Remarks. Completeness of $Y$ and $Z$ is assumed but not needed. Completeness of $X$ is needed for the closed-range part.

Soundness checks.

Real-valued norms only, with no junk. $c$ is a fixed constant quantified before $x$ , so the estimate is uniform. IsClosed (Set.range T) uses the coercion of $T$ to a function, which is the right set.
Not vacuous: it applies e.g. to Fredholm operators with a compact perturbation estimate. It is true. This is the standard Peetre-type lemma: on $\ker T$ , $\|x\|\le c\|Kx\|$ , so the unit ball of $\ker T$ is compact. For closed range, one splits off the finite-dimensional kernel, using a closed complement, and argues by contradiction with compactness of $K$ .

Verdict: no mis-formalization observed

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

An estimate modulo a compact operator gives finite-dimensional kernel and closed range

Read-back: CauchyRiemannIndex.finiteDimensional_ker_isClosed_range_of_estimate

Read-back: `CauchyRiemannIndex.finiteDimensional_ker_isClosed_range_of_estimate`