19.27. Finiteness.SchwartzFiniteness🔗

Jacobians.Finiteness.SchwartzFiniteness — source

surjective_of_approx

Successive-approximation surjectivity. If a continuous linear map g : E →L[ℂ] G between Banach spaces admits, for every target y, an *approximate* preimage x within distance (1/2)‖y‖ and with norm ≤ C‖y‖, then g is (exactly) surjective. This is the iterative second half of the Banach open mapping theorem (ContinuousLinearMap.exists_preimage_norm_le), abstracted so it can be applied to a small perturbation of a surjection.

theorem surjective_of_approx [CompleteSpace E] {G : Type*} [NormedAddCommGroup G]
    [NormedSpace ℂ G] (g : E →L[ℂ] G) {C : ℝ}
    (h : ∀ y : G, ∃ x : E, dist (g x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖) :
    Function.Surjective g

exists_finiteDim_approx

Finite-dimensional δ-net for a compact operator. A compact operator K admits a finite-dimensional subspace S ≤ F that δ-approximates the image of the unit ball: every K x with ‖x‖ ≤ 1 lies within distance δ of S. The subspace is the span of a finite δ-net of the (relatively compact) image of the closed unit ball.

theorem exists_finiteDim_approx
    (K : E →L[ℂ] F) (hK : IsCompactOperator K) {δ : ℝ} (hδ : 0 < δ) :
    ∃ S : Submodule ℂ F, FiniteDimensional ℂ S ∧
      ∀ x : E, ‖x‖ ≤ 1 → infDist (K x) (S : Set F) ≤ δ

finiteDimensional_quotient_range_add_compact

Schwartz finiteness (Forster 14.8). A compact perturbation of a surjection between Banach spaces has finite-codimensional image: if A : E →L[ℂ] F is surjective and K : E →L[ℂ] F is a compact operator, then F ⧸ range (A + K) is finite-dimensional. (K = 0 ⟹ codim 0; A = id ⟹ Riesz–Schauder for 1 + K.) This is the functional-analysis core of Forster 14.9.

theorem finiteDimensional_quotient_range_add_compact [CompleteSpace E] [CompleteSpace F]
    (A : E →L[ℂ] F) (hA : Function.Surjective A)
    (K : E →L[ℂ] F) (hK : IsCompactOperator K) :
    FiniteDimensional ℂ (F ⧸ LinearMap.range (A + K).toLinearMap)