Remark 2.21(3): the Gray isotopy fixes points where vanishes
ProvedGrayStability.gray_stability_fixing_stationary_pointsLet be a compact regular level and , , a smooth family of contact forms on . Then there are an isotopy of and smooth functions on with on for , such that in addition every point with
satisfies for all .
This relative version is the form used to prove neighbourhood theorems for submanifolds, where the forms already agree along the submanifold (Geiges, proof of Theorem 2.27, the neighbourhood theorem for isotropic submanifolds).
import Definitions.Def_GrayStability_Basic open scoped ContDiff
namespace GrayStability
/-- Geiges, Remark 2.21 (3): the Gray isotopy can be chosen so that every point `p ∈ M`
at which `α̇_t(p)` vanishes on `T_p M` for all `t ∈ [0, 1]` stays fixed. -/
theorem gray_stability_fixing_stationary_points {n c : ℕ} (F : E n → (Fin c → ℝ))
(hF : IsCompactRegularLevel F) (α : ℝ → OneForm n) (hα : IsContactFamilyOn F α) :
∃ ψ : ℝ → E n → E n, IsIsotopyOf F ψ ∧
(∃ lam : ℝ → E n → ℝ, ContDiff ℝ ∞ (fun p : ℝ × E n => lam p.1 p.2) ∧
(∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ y ∈ levelSet F, 0 < lam t y) ∧
∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ y ∈ levelSet F, ∀ v ∈ tangentSpace F y,
pullback (ψ t) (α t) y v = lam t y * α 0 y v) ∧
∀ p ∈ levelSet F,
(∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ v ∈ tangentSpace F p, formTimeDeriv α t p v = 0) →
∀ t ∈ Set.Icc (0 : ℝ) 1, ψ t p = p := by sorry
end GrayStability
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Read-back: gray_stability_fixing_stationary_points
Statement. For all natural numbers , every map , and every map from to one-forms on : if
- (hypothesis on ) is a compact regular level, i.e. , is compact, and is surjective for all ; and
- (hypothesis on ) is a contact family on , i.e. is on and is contact at for all and all ,
then there exists a map which is an isotopy of (definition below) such that both of the following hold.
(A) Conformal relation. There exists , , which is on all of , with (strictly) for all , , and
Positivity and the identity are required only on (the identity only for ); elsewhere is only smooth. is not required.
(B) Fixed points. For every point : if
then for all .
Remarks on (B), as written:
- The same that witnesses (A) must satisfy (B), for all qualifying simultaneously ( is chosen before is quantified; plays no role in (B)).
- The hypothesis of (B) concerns only the single point (not a neighbourhood of , and not or derivatives in ), only tangent vectors , and only times . The time derivative is the ordinary two-sided derivative of the real function on at (including at and ); since is assumed smooth, the derivative exists and the "zero where not differentiable" convention does not come into play. Equivalently, the hypothesis says that restricted to does not depend on .
- The conclusion of (B) is only for ; nothing is asserted about , about , or about times outside .
- If no point of satisfies the hypothesis of (B), then (B) is vacuous.
Setting and unfolded definitions. Throughout, are arbitrary natural numbers (both may be ), and means the space of functions with the sup norm. A one-form is any map , (a continuous linear functional at each point; no regularity is built in). Derivatives are Fréchet derivatives of maps on the ambient space (or ), with the convention that a derivative is at any point where the map is not differentiable. For and a one-form :
-
Level set: .
-
Compact regular level (hypothesis on ): is on all of , is compact, and for every the derivative is surjective.
-
Tangent space: (defined for every , used only for ).
-
Exterior derivative: , where is the ambient derivative of (equal to if is not differentiable at ).
-
Contact plane: .
-
Contact at : (i) there exists with , and (ii) for every with there exists with (i.e. restricted to is nondegenerate; condition (ii) is vacuous when ). No orientation, sign, or dimension-parity condition is imposed explicitly.
-
Smooth family: a map from to one-forms such that is on all of .
-
Contact family on (hypothesis on ): is a smooth family, and for every and every , is contact at in the above sense. Nothing is required of for beyond smoothness, nor off beyond smoothness.
-
Isotopy of : a map , , such that
- is on all of ;
- for every (only on , not on all of );
- for every : maps into , is injective on , and maps onto ; and for every , the linear map is injective on .
Nothing is required of for other than smoothness, and nothing off other than smoothness. The definition does not state separately that maps into .
-
Pullback: , where is the ambient derivative of at . Edge cases of the hypotheses.
-
Surjectivity of at points of forces there; if then must be empty.
-
If (e.g. ; or and ; or a nonzero constant with ), every condition quantified over is vacuous: both hypotheses reduce to smoothness of and of , and the conclusion only asks for smooth objects with no constraint coming from .
-
Contact condition (i) requires at each , so a nonempty needs . For the target is a point, so and ; compactness forces , and then violates (i). Hence for the two hypotheses cannot hold simultaneously.
-
If , then and contact condition (ii) is vacuous; "contact" then only means that does not vanish identically on .
-
The contact condition and use the ambient derivative of on , evaluated at points of on vectors of .
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.