Global parametric transversality for Fredholm equations

Let f : E × Λ → F be a parametrized equation. A parameter l is regular at the level c when the fixed-parameter linearization of x ↦ f (x, l) is surjective at every solution. This file proves that the regular parameters form a residual, and hence dense, subset of Λ provided the universal linearization is surjective and the fixed-parameter linearization is Fredholm at every solution.

The proof globalizes the local statement in TauCeti.Analysis.Fredholm.LevelSet.Parametric. Around each solution, a level-set chart turns the projection to Λ into TauCeti.levelSetParameterMap; local Sard--Smale puts its non-regular values in a nowhere dense set. Second countability of the universal level set supplies a countable subcover, so all non-regular parameters form a meagre set. Completeness of Λ then makes the residual set of regular parameters dense by the Baire category theorem.

This is the parametric transversality theorem for maps between Banach spaces. Fredholm sections of Banach bundles require a separate bundle-level extension.

Main results

• TauCeti.IsRegularParameter: every solution at a parameter has surjective fixed-parameter linearization.
• TauCeti.isMeagre_setOf_not_isRegularParameter: the non-regular parameters of a universal Fredholm equation form a meagre set.
• TauCeti.mem_residual_setOf_isRegularParameter: the regular parameters form a residual set.
• TauCeti.dense_setOf_isRegularParameter: the regular parameters are dense.

References

• D. McDuff, D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix A.3.
• S. Smale, An infinite dimensional version of Sard's theorem, Amer. J. Math. 87 (1965), 861--866.

def TauCeti.IsRegularParameter {E : Type u_1} {Λ : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [NormedAddCommGroup F] [NormedSpace ℝ F] (f : E × Λ → F) (c : F) (l : Λ) : Prop

A parameter l is regular for the level equation f (x, l) = c when its fixed-parameter linearization is surjective at every solution x.

This is deliberately a condition only on the E direction. Surjectivity of the total derivative on E × Λ, used by the parametric transversality theorem, is a separate hypothesis.

Equations

• TauCeti.IsRegularParameter f c l = ∀ (x : E), f (x, l) = c → Function.Surjective ⇑(fderiv ℝ f (x, l) ∘SL ContinuousLinearMap.inl ℝ E Λ)

theorem TauCeti.isRegularParameter_iff {E : Type u_1} {Λ : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : E × Λ → F} {c : F} {l : Λ} : IsRegularParameter f c l ↔ ∀ (x : E), f (x, l) = c → Function.Surjective ⇑(fderiv ℝ f (x, l) ∘SL ContinuousLinearMap.inl ℝ E Λ)

A parameter is regular exactly when the fixed-parameter derivatives are surjective at all solutions of the level equation.

theorem TauCeti.isMeagre_setOf_not_isRegularParameter {E : Type u_1} {Λ : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace Λ] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SecondCountableTopology (E × Λ)] {f : E × Λ → F} {c : F} {n : WithTop ℕ∞} (hcont : ∀ (z : E × Λ), f z = c → ContDiffAt ℝ n f z) (hFred : ∀ (z : E × Λ), f z = c → (fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ).IsFredholm) (htotal : ∀ (z : E × Λ), f z = c → Function.Surjective ⇑(fderiv ℝ f z)) (hn : ∀ (z : E × Λ), f z = c → ↑(Module.finrank ℝ ↥(↑(fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ)).ker * Module.finrank ℝ ↥(↑(fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ)).ker + 1) ≤ n) : IsMeagre {l : Λ | ¬IsRegularParameter f c l}

Global parametric transversality. The non-regular parameters of a sufficiently smooth universal Fredholm equation form a meagre set.

The hypotheses are imposed only along the level set f⁻¹(c). There the fixed-parameter linearization must be Fredholm, the total linearization must be surjective, and the smoothness order must meet the current Sard--Smale threshold (dim ker)² + 1. Second countability of the universal source makes the level set second countable and hence allows the local nowhere dense exceptional sets to be reduced to a countable family.

theorem TauCeti.mem_residual_setOf_isRegularParameter {E : Type u_1} {Λ : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace Λ] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SecondCountableTopology (E × Λ)] {f : E × Λ → F} {c : F} {n : WithTop ℕ∞} (hcont : ∀ (z : E × Λ), f z = c → ContDiffAt ℝ n f z) (hFred : ∀ (z : E × Λ), f z = c → (fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ).IsFredholm) (htotal : ∀ (z : E × Λ), f z = c → Function.Surjective ⇑(fderiv ℝ f z)) (hn : ∀ (z : E × Λ), f z = c → ↑(Module.finrank ℝ ↥(↑(fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ)).ker * Module.finrank ℝ ↥(↑(fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ)).ker + 1) ≤ n) : {l : Λ | IsRegularParameter f c l} ∈ residual Λ

The regular parameters of a sufficiently smooth universal Fredholm equation form a residual set.

This is the complement formulation of TauCeti.isMeagre_setOf_not_isRegularParameter.

theorem TauCeti.dense_setOf_isRegularParameter {E : Type u_1} {Λ : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup Λ] [NormedSpace ℝ Λ] [CompleteSpace Λ] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] [SecondCountableTopology (E × Λ)] {f : E × Λ → F} {c : F} {n : WithTop ℕ∞} (hcont : ∀ (z : E × Λ), f z = c → ContDiffAt ℝ n f z) (hFred : ∀ (z : E × Λ), f z = c → (fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ).IsFredholm) (htotal : ∀ (z : E × Λ), f z = c → Function.Surjective ⇑(fderiv ℝ f z)) (hn : ∀ (z : E × Λ), f z = c → ↑(Module.finrank ℝ ↥(↑(fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ)).ker * Module.finrank ℝ ↥(↑(fderiv ℝ f z ∘SL ContinuousLinearMap.inl ℝ E Λ)).ker + 1) ≤ n) : Dense {l : Λ | IsRegularParameter f c l}

The regular parameters of a sufficiently smooth universal Fredholm equation are dense.

This is the Baire-category consequence of TauCeti.mem_residual_setOf_isRegularParameter.