Theorem 2.20 (proof): Gray isotopy with
ProvedGrayStability.gray_stability_conformalLet be a compact regular level and , , a smooth family of contact forms on . Then there are an isotopy of and a smooth function , positive on , such that
This is the form in which the proof of Gray's theorem produces the isotopy. It implies the theorem, since gives .
import Definitions.Def_GrayStability_Basic open scoped ContDiff
namespace GrayStability
/-- Geiges, proof of Theorem 2.20: for a smooth family of contact forms `α_t` on a
closed submanifold `M ⊂ ℝⁿ` there are an isotopy `ψ_t` of `M` and smooth positive
functions `λ_t` with `ψ_t^* α_t = λ_t α_0` on `TM`. -/
theorem gray_stability_conformal {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 := by sorry
end GrayStability
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Read-back: gray_stability_conformal
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 exist
- a map which is an isotopy of (definition below), and then
- a function , , which is on all of ,
such that
- (strictly) for every and every ; and
- for every , every and every ,
i.e. as functionals restricted to .
Positivity of and the identity are required only for and , and the identity only on tangent vectors ; elsewhere is only required to be smooth (it may vanish or be negative there). is not required, and the isotopy is required to satisfy only on .
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.