A map with upper semi-Fredholm derivative is proper near the point

A continuous map between infinite-dimensional Banach spaces need not be proper: a Fredholm linear map with nonzero kernel has a noncompact fibre over zero. A map whose derivative at a point a is closed-range with finite-dimensional complemented kernel — in particular, a Fredholm operator — is nonetheless proper on a neighbourhood of a:

∃ N ∈ 𝓝 a, ∀ L compact, N ∩ f ⁻¹' L is compact.

This is Smale's local properness lemma, the geometric half of the input to the Sard--Smale theorem (Smale, An infinite dimensional version of Sard's theorem, Amer. J. Math. 87 (1965), 861–866; McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A). Its consequence recorded here is that the preimage f ⁻¹' L of a compact set — in particular a level set f ⁻¹' {c}, the shape every moduli space of the analytic Heegaard Floer roadmap takes — is a locally compact space, even though the Banach space it sits inside is not.

The proof is quantitative rather than chart-theoretic. The a priori estimate ContinuousLinearMap.exists_projection_norm_le supplies a continuous projection P of E onto ker f' and a constant C > 0 with ‖x‖ ≤ C * ‖f' x‖ + ‖P x‖. On a small enough closed ball N around a, strict differentiability turns this into the two-sided bound

‖x - y‖ ≤ 2 * (C * ‖f x - f y‖) + 2 * ‖P x - P y‖ for x, y ∈ N,

so the map x ↦ (f x, P x) is anti-Lipschitz on N. Its second component takes values in the finite-dimensional space ker f', where bounded sets have compact closure, so x ↦ (f x, P x) sends N ∩ f ⁻¹' L into a compact box; being anti-Lipschitz, it reflects total boundedness, and N ∩ f ⁻¹' L is totally bounded and closed, hence compact.

Main declarations

• TauCeti.one_sub_mul_norm_sub_le: an a priori estimate survives a nonlinear approximation, degraded by its quality — the absorption step behind Peetre's lemma.
• HasStrictFDerivAt.exists_mem_nhds_forall_isCompact_inter_preimage: local properness.
• HasStrictFDerivAt.exists_mem_nhds_isCompact_inter_preimage_singleton: an arbitrary fibre is compact near the point of differentiation.
• TauCeti.locallyCompactSpace_preimage and TauCeti.locallyCompactSpace_preimage_singleton: the preimage of a compact set, and in particular a level set, along which the derivative is Fredholm is locally compact.

Lane F0 of the analytic Heegaard Floer roadmap asks for the package "a moduli space is the zero set of a Fredholm section, and at a regular point a manifold of dimension the index", of which TauCeti.Analysis.Fredholm.LevelSet.Basic supplies the charts. Local properness is the complementary topological half, and it is what will make the critical values of a Fredholm map locally closed in the Sard--Smale argument.

theorem TauCeti.one_sub_mul_norm_sub_le {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {f' : E →L[𝕜] F} {G : Type u_4} [SeminormedAddGroup G] {P : E →+ G} {C : ℝ} {N : Set E} {ε : NNReal} (hC : 0 ≤ C) (hest : ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖ + ‖P z‖) (happ : ApproximatesLinearOn f f' N ε) {x : E} (hx : x ∈ N) {y : E} (hy : y ∈ N) : (1 - C * ↑ε) * ‖x - y‖ ≤ C * ‖f x - f y‖ + ‖P x - P y‖

An a priori estimate survives a nonlinear approximation, degraded by its quality. Suppose every vector is controlled by its image under f' together with an auxiliary additive map P, as ‖z‖ ≤ C * ‖f' z‖ + ‖P z‖, and f approximates f' on N to within ε. Then the same control holds for f on N, with the left side scaled by 1 - C * ε; it has content exactly when C * ε < 1, and taking ε ≤ (2 * C)⁻¹ gives the factor-two form properness uses.

Nothing about P beyond map_sub enters, so it need only be additive into a seminormed additive group — no scalar-linearity, no idempotence, no constraint on its target. Taking it to be the projection onto ker f' from ContinuousLinearMap.exists_projection_norm_le recovers the Peetre estimate, which characterises semi-Fredholm operators — see Wendl, Fredholm operators, Lemma 5.2.

theorem HasStrictFDerivAt.exists_mem_nhds_forall_isCompact_inter_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hclosed : IsClosed ↑(↑f').range) (hfinite : FiniteDimensional 𝕜 ↥(↑f').ker) (hcompl : (↑f').ker.ClosedComplemented) : ∃ N ∈ nhds a, ∀ (L : Set F), IsCompact L → IsCompact (N ∩ f ⁻¹' L)

Local properness of a map with upper semi-Fredholm derivative. If f is strictly differentiable at a and its derivative there has closed range and finite-dimensional complemented kernel, then f is proper on a neighbourhood N of a: the part of the preimage of any compact set lying in N is compact.

Compare ContinuousLinearMap.exists_projection_norm_le, the linear estimate this is read off from: the kernel direction, in which f' loses all control, is finite-dimensional, so the loss of compactness it causes is harmless.

theorem HasStrictFDerivAt.exists_mem_nhds_isCompact_inter_preimage_singleton {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {f' : E →L[𝕜] F} {a : E} (hf : HasStrictFDerivAt f f' a) (hclosed : IsClosed ↑(↑f').range) (hfinite : FiniteDimensional 𝕜 ↥(↑f').ker) (hcompl : (↑f').ker.ClosedComplemented) (c : F) : ∃ N ∈ nhds a, IsCompact (N ∩ f ⁻¹' {c})

An arbitrary fibre of f is compact near a point where the derivative has closed range and finite-dimensional complemented kernel. This is the case L = {c} of local properness, and it is the local finiteness statement that a moduli space of a Fredholm problem inherits before any global energy bound is imposed.

theorem TauCeti.locallyCompactSpace_preimage {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {D : E → E →L[𝕜] F} {L : Set F} (hL : IsCompact L) (hf : ∀ x ∈ f ⁻¹' L, HasStrictFDerivAt f (D x) x) (hclosed : ∀ x ∈ f ⁻¹' L, IsClosed ↑(↑(D x)).range) (hfinite : ∀ x ∈ f ⁻¹' L, FiniteDimensional 𝕜 ↥(↑(D x)).ker) (hcompl : ∀ x ∈ f ⁻¹' L, (↑(D x)).ker.ClosedComplemented) : LocallyCompactSpace ↑(f ⁻¹' L)

The preimage of a compact set under a map with upper semi-Fredholm derivative is locally compact. If f is strictly differentiable at each point of f ⁻¹' L, its derivative there has closed range and finite-dimensional complemented kernel, and L is compact, then f ⁻¹' L, with the topology induced from E, is a locally compact space.

No compactness is assumed of the ambient Banach space, and none is available: the point is that the hypotheses confine the failure of local compactness to the finite-dimensional kernel direction, which is itself locally compact and is controlled by the kernel projection.

theorem TauCeti.locallyCompactSpace_preimage_singleton {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [ProperSpace 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {D : E → E →L[𝕜] F} {c : F} (hf : ∀ x ∈ f ⁻¹' {c}, HasStrictFDerivAt f (D x) x) (hclosed : ∀ x ∈ f ⁻¹' {c}, IsClosed ↑(↑(D x)).range) (hfinite : ∀ x ∈ f ⁻¹' {c}, FiniteDimensional 𝕜 ↥(↑(D x)).ker) (hcompl : ∀ x ∈ f ⁻¹' {c}, (↑(D x)).ker.ClosedComplemented) : LocallyCompactSpace ↑(f ⁻¹' {c})

A level set of a map with upper semi-Fredholm derivative is locally compact: the case L = {c} of TauCeti.locallyCompactSpace_preimage, and the shape every moduli space of a Fredholm problem takes.