Exact preimages from approximate preimages

Banach's open mapping theorem is proved in two steps. Baire's theorem first shows that every point of the target is approximately the image of a point of controlled norm; a geometric series then upgrades these approximate preimages to exact ones, using completeness of the domain. Mathlib only states the composite theorem ContinuousLinearMap.exists_preimage_norm_le, whose hypothesis is surjectivity.

This file isolates the second step, so that other sources of approximate preimages can be fed into it. The main application is the case where the closure of the image of every ball contains a ball, as happens when the adjoint is bounded below; this is how surjectivity is recovered in the closed-range theorem. The scalar actions need no compatibility with the norms; only additivity and continuity of the map enter the argument.

The file also records the form of the open mapping theorem used to invert operators pointwise: a bijective continuous linear map between Banach spaces is invertible.

Main declarations

• ContinuousLinearMap.exists_preimage_norm_le_of_approx: approximate preimages of controlled norm with relative error 1 / 2 give exact preimages of controlled norm.
• ContinuousLinearMap.exists_preimage_norm_le_of_mem_closure: if every y lies in the closure of the image of the closed ball of radius C * ‖y‖, then every y has a preimage of norm at most 2 * C * ‖y‖.
• ContinuousLinearMap.isInvertible_iff_bijective: by the open mapping theorem, a continuous linear map between Banach spaces is invertible exactly when it is bijective.

References

• W. Rudin, Functional Analysis, 2nd ed., Lemma 4.13.

The series argument follows the second half of the proof of Mathlib's ContinuousLinearMap.exists_preimage_norm_le.

theorem ContinuousLinearMap.exists_preimage_norm_le_of_approx {𝕜 : Type u_1} {𝕜' : Type u_2} [Semiring 𝕜] [Semiring 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [SeminormedAddCommGroup E] [Module 𝕜 E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [Module 𝕜' F] (f : E →SL[σ] F) {C : ℝ} (hC : ∀ (y : F), ∃ (x : E), dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖) (y : F) : ∃ (x : E), f x = y ∧ ‖x‖ ≤ 2 * C * ‖y‖

Approximate preimages give exact preimages. If every y is within ‖y‖ / 2 of the image of a point of norm at most C * ‖y‖, then every y is the image of a point of norm at most 2 * C * ‖y‖.

theorem ContinuousLinearMap.exists_preimage_norm_le_of_mem_closure {𝕜 : Type u_1} {𝕜' : Type u_2} [Semiring 𝕜] [Semiring 𝕜'] {σ : 𝕜 →+* 𝕜'} {E : Type u_3} [SeminormedAddCommGroup E] [Module 𝕜 E] [CompleteSpace E] {F : Type u_4} [NormedAddCommGroup F] [Module 𝕜' F] (f : E →SL[σ] F) {C : ℝ} (hC : ∀ (y : F), y ∈ closure (⇑f '' Metric.closedBall 0 (C * ‖y‖))) (y : F) : ∃ (x : E), f x = y ∧ ‖x‖ ≤ 2 * C * ‖y‖

Banach's lemma. If every y lies in the closure of the image of the closed ball of radius C * ‖y‖, then every y has a preimage of norm at most 2 * C * ‖y‖. In particular, the map is surjective.

theorem ContinuousLinearMap.isInvertible_iff_bijective {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E →L[𝕜] F} : f.IsInvertible ↔ Function.Bijective ⇑f

By the open mapping theorem, a continuous linear map between Banach spaces is invertible, that is, a continuous linear equivalence, exactly when it is bijective.