Smooth parametrizations of regular Fredholm level sets

At a point where a map between Banach spaces has surjective derivative with complemented kernel, TauCeti.levelSetChart identifies its level set locally with that kernel. This file proves that the inverse chart is, at the chart origin, as smooth as the original map, and computes its derivative there: it is the canonical inclusion of the kernel into the ambient space.

The smoothness statement is Tau Ceti's HasStrictFDerivAt.contDiffAt_implicitToOpenPartialHomeomorphOfComplemented_symm, restricted to the slice {c} × ker f' on which the chart is the implicit function. The derivative statement is Mathlib's HasStrictFDerivAt.to_implicitFunctionOfComplemented, transported along the chart. The geometric organization follows McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., Appendix A.3.

Together with ContinuousLinearMap.IsFredholm.closedComplemented_ker_coprod, which supplies the complemented kernel of a surjective linearization whose fixed-parameter part is Fredholm, these are the pointwise smoothness and derivative computation from which the smooth local input to the parameter projection and Sard--Smale arguments is assembled.

Smoothness at the origin alone does not let two charts of the same level set be compared; the final theorem removes that restriction. It is C^n at every point of the chart target whose image lies in HasStrictFDerivAt.implicitCoordSource, the neighbourhood of the base point on which the coordinate map of the implicit function theorem keeps an invertible derivative. Since that neighbourhood is open and contains the base point, the inverse chart is smooth on a whole neighbourhood of its origin, which is what smooth compatibility of charts needs.

Main results

• TauCeti.contDiffAt_coe_levelSetChart_symm: the inverse regular-level-set chart, included into the ambient Banach space, is smooth at its origin.
• TauCeti.hasStrictFDerivAt_coe_levelSetChart_symm: its derivative there is the inclusion of the derivative's kernel.
• TauCeti.contDiffAt_coe_levelSetChart_symm_of_mem: it is smooth at every point of the chart target that the coordinate map's invertibility neighbourhood covers.

theorem TauCeti.contDiffAt_coe_levelSetChart_symm {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E → F} {f' : E →L[K] F} {a : E} {c : F} {n : WithTop ℕ∞} (hf : HasStrictFDerivAt f f' a) (hcont : ContDiffAt K n f a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (ha : f a = c) : ContDiffAt K n (fun (k : ↥(↑f').ker) => ↑(↑(levelSetChart hf hf' hker ha).symm k)) 0

The inverse regular-level-set chart, followed by the inclusion into the ambient space, is as smooth as the defining equation at the chart origin.

theorem TauCeti.hasStrictFDerivAt_coe_levelSetChart_symm {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E → F} {f' : E →L[K] F} {a : E} {c : F} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (ha : f a = c) : HasStrictFDerivAt (fun (k : ↥(↑f').ker) => ↑(↑(levelSetChart hf hf' hker ha).symm k)) (↑f').ker.subtypeL 0

The derivative at the origin of the inverse regular-level-set chart, included into the ambient space, is the canonical inclusion of the derivative's kernel.

theorem TauCeti.contDiffAt_coe_levelSetChart_symm_of_mem {K : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField K] [NormedAddCommGroup E] [NormedSpace K E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace K F] [CompleteSpace F] {f : E → F} {f' : E →L[K] F} {a : E} {c : F} {n : WithTop ℕ∞} (hf : HasStrictFDerivAt f f' a) (hf' : (↑f').range = ⊤) (hker : (↑f').ker.ClosedComplemented) (ha : f a = c) {k : ↥(↑f').ker} (hk : k ∈ (levelSetChart hf hf' hker ha).target) (hmem : ↑(↑(levelSetChart hf hf' hker ha).symm k) ∈ hf.implicitCoordSource hf' hker) {A : E →L[K] F} (hA : HasFDerivAt f A ↑(↑(levelSetChart hf hf' hker ha).symm k)) (hcont : ContDiffAt K n f ↑(↑(levelSetChart hf hf' hker ha).symm k)) : ContDiffAt K n (fun (k : ↥(↑f').ker) => ↑(↑(levelSetChart hf hf' hker ha).symm k)) k

The inverse regular-level-set chart is smooth away from its centre as well. At a point k of the chart target whose image lies in the neighbourhood HasStrictFDerivAt.implicitCoordSource on which the implicit-function coordinate map keeps an invertible derivative, the inverse chart is as smooth as the equation is there.

TauCeti.contDiffAt_coe_levelSetChart_symm is the case k = 0, where the hypotheses hold automatically.