Local normal form of a Fredholm map

This file gives the Lyapunov--Schmidt finite-dimensional reduction of a nonlinear map at a point where its derivative is Fredholm. A Fredholm package splits the domain and codomain into essential parts, on which the derivative is invertible, and finite-dimensional inessential parts. Projecting the nonlinear map to the essential codomain and retaining the inessential domain coordinate gives a local homeomorphism. When the original map is C^k, the inverse coordinates and the finite-dimensional obstruction are C^k as germs at the base point. In these coordinates the original map has the form

(r, k) ↦ r + q(r, k),

where q takes values in the finite-dimensional codomain complement. Thus all failure of surjectivity is confined to the finite-dimensional codomain complement; after fixing r, the remaining variable k also ranges over a finite-dimensional space. This is the normal-form ingredient of the Sard--Smale argument.

The construction follows S. Smale, An infinite dimensional version of Sard's theorem, Amer. J. Math. 87 (1965), 861--866, and McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A. The local chart is Mathlib's HasStrictFDerivAt.toOpenPartialHomeomorph; the linear splittings are Mathlib's ContinuousLinearMap.FredholmPackage.

Main declarations

• ContinuousLinearMap.FredholmPackage.normalFormEquivL: the linear coordinate change determined by a Fredholm package.
• ContinuousLinearMap.FredholmPackage.normalFormMap: the nonlinear coordinate map.
• ContinuousLinearMap.FredholmPackage.normalFormOpenPartialHomeomorph: the local homeomorphism defined by that map.
• ContinuousLinearMap.FredholmPackage.obstructionMap: the remainder valued in the finite-dimensional complementary codomain direction.
• ContinuousLinearMap.FredholmPackage.obstructionSlice: the finite-dimensional obstruction obtained by fixing the essential coordinate.
• ContinuousLinearMap.FredholmPackage.apply_normalFormOpenPartialHomeomorph_symm: reconstruction of the original map from its essential coordinate and obstruction map.
• ContinuousLinearMap.FredholmPackage.hasStrictFDerivAt_obstructionMap_self: the obstruction has zero derivative at the base point.
• ContinuousLinearMap.FredholmPackage.hasStrictFDerivAt_obstructionSlice_self: the same for the finite-dimensional slice of the obstruction through the base point.
• ContinuousLinearMap.FredholmPackage.hasFDerivAt_obstructionSlice: at any point where the obstruction is differentiable, its slice derivative is the restriction to the kernel direction.
• ContinuousLinearMap.FredholmPackage.contDiffAt_normalFormOpenPartialHomeomorph_symm_self: the inverse normal-form coordinates have the same C^k regularity as the original map, at the normal-form coordinate of the base point.
• ContinuousLinearMap.FredholmPackage.contDiffAt_obstructionMap_self: the obstruction has the same C^k regularity as the original map, at the normal-form coordinate of the base point.
• ContinuousLinearMap.FredholmPackage.contDiffAt_obstructionSlice_self: the finite-dimensional obstruction slice through the base point has that same C^k regularity; this is the input finite-dimensional Sard needs.

Linear and nonlinear coordinates

noncomputable def ContinuousLinearMap.FredholmPackage.normalFormEquivL {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) : E ≃L[𝕜] ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀

The linear coordinate change associated to a Fredholm package. It first splits the domain as the essential summand and the finite-dimensional kernel summand, then uses the package's equivalence on the essential coordinate.

Equations

• pkg.normalFormEquivL = (pkg.decDom.X₁.prodEquivOfIsTopCompl pkg.decDom.X₀ ⋯).symm.trans (pkg.equiv.prodCongr (ContinuousLinearEquiv.refl 𝕜 ↥pkg.decDom.X₀))

@[simp]

theorem ContinuousLinearMap.FredholmPackage.normalFormEquivL_fst {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) (x : E) : (pkg.normalFormEquivL x).1 = pkg.decCodom.proj (T x)

The essential coordinate of the linear normal form is the projection of T x to the essential codomain summand.

@[simp]

theorem ContinuousLinearMap.FredholmPackage.normalFormEquivL_snd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) (x : E) : (pkg.normalFormEquivL x).2 = (pkg.decDom.X₀.projectionOntoL pkg.decDom.X₁ ⋯) x

The inessential coordinate of the linear normal form is the projection of x to the finite-dimensional kernel summand.

@[simp]

theorem ContinuousLinearMap.FredholmPackage.normalFormEquivL_symm_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) (y : ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀) : pkg.normalFormEquivL.symm y = ↑(pkg.equiv.symm y.1) + ↑y.2

The inverse linear normal-form coordinates reassemble the essential and inessential domain components.

noncomputable def ContinuousLinearMap.FredholmPackage.normalFormMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) (f : E → F) (a x : E) : ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀

The nonlinear normal-form coordinate map at a. Its first coordinate is the projection of f x to the essential codomain summand; its second remembers the finite-dimensional kernel coordinate of x - a.

Equations

• pkg.normalFormMap f a x = (pkg.decCodom.proj (f x), (pkg.decDom.X₀.projectionOntoL pkg.decDom.X₁ ⋯) (x - a))

@[simp]

theorem ContinuousLinearMap.FredholmPackage.normalFormMap_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) (f : E → F) (a x : E) : pkg.normalFormMap f a x = (pkg.decCodom.proj (f x), (pkg.decDom.X₀.projectionOntoL pkg.decDom.X₁ ⋯) (x - a))

The two components of the nonlinear normal-form coordinate map.

theorem ContinuousLinearMap.FredholmPackage.normalFormMap_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) (f : E → F) (a : E) : pkg.normalFormMap f a a = (pkg.decCodom.proj (f a), 0)

The normal-form coordinate map evaluated at its base point. Not a simp lemma: the general normalFormMap_apply already rewrites the left-hand side.

theorem ContinuousLinearMap.FredholmPackage.hasStrictFDerivAt_normalFormMap_of_hasStrictFDerivAt {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) {f : E → F} {a x : E} {T' : E →L[𝕜] F} (hf : HasStrictFDerivAt f T' x) : HasStrictFDerivAt (pkg.normalFormMap f a) ((pkg.decCodom.proj ∘SL T').prod (pkg.decDom.X₀.projectionOntoL pkg.decDom.X₁ ⋯)) x

The derivative of the nonlinear normal-form coordinate map at any point is the product of the projected derivative of f and the fixed projection onto the inessential domain summand.

theorem ContinuousLinearMap.FredholmPackage.hasStrictFDerivAt_normalFormMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : HasStrictFDerivAt (pkg.normalFormMap f a) (↑pkg.normalFormEquivL) a

The derivative of the nonlinear normal-form coordinate map at its base point is precisely the linear coordinate equivalence associated to the Fredholm package.

theorem ContinuousLinearMap.FredholmPackage.contDiffAt_normalFormMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) {f : E → F} {a x : E} {n : WithTop ℕ∞} (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (pkg.normalFormMap f a) x

The nonlinear normal-form coordinate map has the same C^k regularity as the original map, at every point where the latter is C^k.

The normal-form chart

noncomputable def ContinuousLinearMap.FredholmPackage.normalFormOpenPartialHomeomorph {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : OpenPartialHomeomorph E (↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀)

The local homeomorphism putting a map into Fredholm normal-form coordinates near a point where its derivative is represented by pkg.

Equations

• pkg.normalFormOpenPartialHomeomorph hf = HasStrictFDerivAt.toOpenPartialHomeomorph (pkg.normalFormMap f a) ⋯

@[simp]

theorem ContinuousLinearMap.FredholmPackage.normalFormOpenPartialHomeomorph_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) (x : E) : ↑(pkg.normalFormOpenPartialHomeomorph hf) x = pkg.normalFormMap f a x

The Fredholm normal-form homeomorphism agrees with the normal-form coordinate map everywhere; its source only controls where the inverse laws apply.

theorem ContinuousLinearMap.FredholmPackage.mem_normalFormOpenPartialHomeomorph_source {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : a ∈ (pkg.normalFormOpenPartialHomeomorph hf).source

The base point belongs to the source of the Fredholm normal-form homeomorphism.

theorem ContinuousLinearMap.FredholmPackage.normalFormOpenPartialHomeomorph_self_mem_target {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : (pkg.decCodom.proj (f a), 0) ∈ (pkg.normalFormOpenPartialHomeomorph hf).target

The normal-form coordinate of the base point belongs to the target of the local homeomorphism.

@[simp]

theorem ContinuousLinearMap.FredholmPackage.normalFormOpenPartialHomeomorph_symm_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : ↑(pkg.normalFormOpenPartialHomeomorph hf).symm ((pkg.decCodom.X₁.projectionOnto pkg.decCodom.X₀ ⋯) (f a), 0) = a

Applying the inverse normal-form coordinate map to the coordinate of the base point returns the base point.

The finite-dimensional obstruction map

noncomputable def ContinuousLinearMap.FredholmPackage.obstructionMap {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) (y : ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀) : ↥pkg.decCodom.X₀

The inessential-codomain component of f in Fredholm normal-form coordinates. Its codomain is finite dimensional by pkg.decCodom.finite_X₀; fixing the first coordinate gives pkg.obstructionSlice, a map between the finite-dimensional spaces pkg.decDom.X₀ and pkg.decCodom.X₀, whose neighborhood regularity at the base coordinate — the remaining input for Sard — is pkg.contDiffAt_obstructionSlice_self. Values outside the target of pkg.normalFormOpenPartialHomeomorph hf are irrelevant, as for any OpenPartialHomeomorph inverse.

Equations

• pkg.obstructionMap hf y = (pkg.decCodom.X₀.projectionOntoL pkg.decCodom.X₁ ⋯) (f (↑(pkg.normalFormOpenPartialHomeomorph hf).symm y))

noncomputable def ContinuousLinearMap.FredholmPackage.obstructionSlice {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) (y : ↥pkg.decCodom.X₁) (z : ↥pkg.decDom.X₀) : ↥pkg.decCodom.X₀

The finite-dimensional obstruction map obtained by fixing the essential codomain coordinate. Both its domain and codomain are finite dimensional. This is the map to which finite-dimensional Sard is applied in the Lyapunov--Schmidt proof of Sard--Smale.

Equations

• pkg.obstructionSlice hf y z = pkg.obstructionMap hf (y, z)

@[simp]

theorem ContinuousLinearMap.FredholmPackage.obstructionMap_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) (y : ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀) : pkg.obstructionMap hf y = (pkg.decCodom.X₀.projectionOntoL pkg.decCodom.X₁ ⋯) (f (↑(pkg.normalFormOpenPartialHomeomorph hf).symm y))

The obstruction map is the complementary-codomain projection of f after applying the inverse normal-form coordinates.

@[simp]

theorem ContinuousLinearMap.FredholmPackage.obstructionSlice_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) (y : ↥pkg.decCodom.X₁) (z : ↥pkg.decDom.X₀) : pkg.obstructionSlice hf y z = pkg.obstructionMap hf (y, z)

The obstruction slice is the obstruction map with its essential coordinate fixed.

theorem ContinuousLinearMap.FredholmPackage.hasFDerivAt_obstructionSlice {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) {y : ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀} (hq : DifferentiableAt 𝕜 (pkg.obstructionMap hf) y) : HasFDerivAt (pkg.obstructionSlice hf y.1) (fderiv 𝕜 (pkg.obstructionMap hf) y ∘SL inr 𝕜 ↥pkg.decCodom.X₁ ↥pkg.decDom.X₀) y.2

Fixing the essential coordinate differentiates the obstruction along the inclusion of the inessential domain summand as the second normal-form factor: the derivative of the obstruction slice is the derivative of the obstruction map precomposed with ContinuousLinearMap.inr.

theorem ContinuousLinearMap.FredholmPackage.obstructionMap_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : pkg.obstructionMap hf (pkg.decCodom.proj (f a), 0) = (pkg.decCodom.X₀.projectionOntoL pkg.decCodom.X₁ ⋯) (f a)

At the coordinate of the base point the obstruction is the inessential-codomain component of f a. Not a simp lemma: obstructionMap_apply and normalFormOpenPartialHomeomorph_symm_self already rewrite the left-hand side.

theorem ContinuousLinearMap.FredholmPackage.proj_apply_normalFormOpenPartialHomeomorph_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) {y : ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀} (hy : y ∈ (pkg.normalFormOpenPartialHomeomorph hf).target) : pkg.decCodom.proj (f (↑(pkg.normalFormOpenPartialHomeomorph hf).symm y)) = y.1

In normal-form coordinates, the essential component of f is the first coordinate.

theorem ContinuousLinearMap.FredholmPackage.apply_normalFormOpenPartialHomeomorph_symm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) {y : ↥pkg.decCodom.X₁ × ↥pkg.decDom.X₀} (hy : y ∈ (pkg.normalFormOpenPartialHomeomorph hf).target) : f (↑(pkg.normalFormOpenPartialHomeomorph hf).symm y) = ↑y.1 + ↑(pkg.obstructionMap hf y)

Fredholm local normal form. On the target of the normal-form chart, the original map is the sum of its essential coordinate and the finite-dimensional obstruction.

theorem ContinuousLinearMap.FredholmPackage.hasStrictFDerivAt_normalFormOpenPartialHomeomorph_symm_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : HasStrictFDerivAt ↑(pkg.normalFormOpenPartialHomeomorph hf).symm ↑pkg.normalFormEquivL.symm (pkg.decCodom.proj (f a), 0)

The inverse normal-form coordinates have derivative inverse to the linear normal-form equivalence at the coordinate of the base point.

theorem ContinuousLinearMap.FredholmPackage.hasStrictFDerivAt_obstructionMap_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : HasStrictFDerivAt (pkg.obstructionMap hf) 0 (pkg.decCodom.proj (f a), 0)

The finite-dimensional obstruction has zero derivative at the coordinate of the base point. This is the differential statement that the chosen essential coordinate absorbs the entire linear part of f.

theorem ContinuousLinearMap.FredholmPackage.hasStrictFDerivAt_obstructionSlice_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} (hf : HasStrictFDerivAt f T a) : HasStrictFDerivAt (pkg.obstructionSlice hf (pkg.decCodom.proj (f a))) 0 0

The finite-dimensional obstruction slice through the base point has zero derivative at the base coordinate: this is the statement hasStrictFDerivAt_obstructionMap_self reduced to the finite-dimensional kernel direction, which is where Sard is applied.

Smoothness of the finite-dimensional reduction

theorem ContinuousLinearMap.FredholmPackage.contDiffAt_normalFormOpenPartialHomeomorph {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a x : E} {n : WithTop ℕ∞} (hfd : HasStrictFDerivAt f T a) (hf : ContDiffAt 𝕜 n f x) : ContDiffAt 𝕜 n (↑(pkg.normalFormOpenPartialHomeomorph hfd)) x

The normal-form chart has the same C^k regularity as the original map, at every point where the latter is C^k.

theorem ContinuousLinearMap.FredholmPackage.contDiffAt_normalFormOpenPartialHomeomorph_symm_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} {n : WithTop ℕ∞} (hfd : HasStrictFDerivAt f T a) (hf : ContDiffAt 𝕜 n f a) : ContDiffAt 𝕜 n ↑(pkg.normalFormOpenPartialHomeomorph hfd).symm (pkg.decCodom.proj (f a), 0)

If f is C^k at the base point, then the inverse normal-form coordinates are C^k at the coordinate of that point. Here n may be any value in ℕ∞ω, including 0 and ω.

theorem ContinuousLinearMap.FredholmPackage.contDiffAt_obstructionMap_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} {n : WithTop ℕ∞} (hfd : HasStrictFDerivAt f T a) (hf : ContDiffAt 𝕜 n f a) : ContDiffAt 𝕜 n (pkg.obstructionMap hfd) (pkg.decCodom.proj (f a), 0)

If f is C^k at a point with Fredholm derivative, then its finite-dimensional obstruction in Lyapunov--Schmidt coordinates is C^k at the corresponding normal-form coordinate.

theorem ContinuousLinearMap.FredholmPackage.contDiffAt_obstructionSlice_self {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {T : E →L[𝕜] F} (pkg : T.FredholmPackage) [CompleteSpace E] {f : E → F} {a : E} {n : WithTop ℕ∞} (hfd : HasStrictFDerivAt f T a) (hf : ContDiffAt 𝕜 n f a) : ContDiffAt 𝕜 n (pkg.obstructionSlice hfd (pkg.decCodom.proj (f a))) 0

The finite-dimensional obstruction slice through the base point inherits the C^k regularity of the original map. This is the regularity input for finite-dimensional Sard.