Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Theorem 2.20 (proof): Gray isotopy with ψt∗αt=λtα0\psi_t^*\alpha_t=\lambda_t\alpha_0ψt∗​αt​=λt​α0​

Proved
GrayStability.gray_stability_conformal

by Mazecto · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

contact-geometrydifferential-geometrysymplectic-geometry

Let M=F−1(0)⊂RnM=F^{-1}(0)\subset\mathbb{R}^nM=F−1(0)⊂Rn be a compact regular level and αt\alpha_tαt​, t∈[0,1]t\in[0,1]t∈[0,1], a smooth family of contact forms on MMM. Then there are an isotopy ψt\psi_tψt​ of MMM and a smooth function λ:R×Rn→R\lambda:\mathbb{R}\times\mathbb{R}^n\to\mathbb{R}λ:R×Rn→R, positive on [0,1]×M[0,1]\times M[0,1]×M, such that

ψt∗αt=λt α0on TyM,t∈[0,1], y∈M.\psi_t^*\alpha_t=\lambda_t\,\alpha_0\quad\text{on } T_yM,\qquad t\in[0,1],\ y\in M.ψt∗​αt​=λt​α0​on Ty​M,t∈[0,1], y∈M.

This is the form in which the proof of Gray's theorem produces the isotopy. It implies the theorem, since λt>0\lambda_t>0λt​>0 gives Tψt(ker⁡α0)=ker⁡αtT\psi_t(\ker\alpha_0)=\ker\alpha_tTψt​(kerα0​)=kerαt​.

Preamble
import Definitions.Def_GrayStability_Basic

open scoped ContDiff
Formal statement
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
Source
Geiges, Contact geometry, Handbook of Differential Geometry Vol. II (2006) 315-382, https://arxiv.org/abs/math/0307242, proof of Theorem 2.20, pp. 14-15
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 n,cn, cn,c, every map F:Rn→RcF : \mathbb{R}^n \to \mathbb{R}^cF:Rn→Rc, and every map t↦αtt \mapsto \alpha_tt↦αt​ from R\mathbb{R}R to one-forms on Rn\mathbb{R}^nRn: if

  • (hypothesis on FFF) FFF is a compact regular level, i.e. F∈C∞F \in C^\inftyF∈C∞, M=F−1(0)M = F^{-1}(0)M=F−1(0) is compact, and DF(y)DF(y)DF(y) is surjective for all y∈My \in My∈M; and
  • (hypothesis on α\alphaα) α\alphaα is a contact family on MMM, i.e. (t,y)↦αt(y)(t,y) \mapsto \alpha_t(y)(t,y)↦αt​(y) is C∞C^\inftyC∞ on R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn and αt\alpha_tαt​ is contact at yyy for all t∈[0,1]t \in [0,1]t∈[0,1] and all y∈My \in My∈M,

then there exist

  • a map ψ:R×Rn→Rn\psi : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^nψ:R×Rn→Rn which is an isotopy of MMM (definition below), and then
  • a function λ:R×Rn→R\lambda : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}λ:R×Rn→R, (t,y)↦λt(y)(t,y) \mapsto \lambda_t(y)(t,y)↦λt​(y), which is C∞C^\inftyC∞ on all of R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn,

such that

  1. λt(y)>0\lambda_t(y) > 0λt​(y)>0 (strictly) for every t∈[0,1]t \in [0,1]t∈[0,1] and every y∈My \in My∈M; and
  2. for every t∈[0,1]t \in [0,1]t∈[0,1], every y∈My \in My∈M and every v∈Ty=ker⁡DF(y)v \in T_y = \ker DF(y)v∈Ty​=kerDF(y),
αt(ψt(y))(Dψt(y) v)=λt(y) α0(y)(v),\alpha_t\big(\psi_t(y)\big)\big(D\psi_t(y)\,v\big) = \lambda_t(y)\,\alpha_0(y)(v),αt​(ψt​(y))(Dψt​(y)v)=λt​(y)α0​(y)(v),

i.e. (ψt∗αt)y=λt(y) α0(y)(\psi_t^*\alpha_t)_y = \lambda_t(y)\,\alpha_0(y)(ψt∗​αt​)y​=λt​(y)α0​(y) as functionals restricted to TyT_yTy​.

Positivity of λ\lambdaλ and the identity are required only for t∈[0,1]t \in [0,1]t∈[0,1] and y∈My \in My∈M, and the identity only on tangent vectors v∈Tyv \in T_yv∈Ty​; elsewhere λ\lambdaλ is only required to be smooth (it may vanish or be negative there). λ0=1\lambda_0 = 1λ0​=1 is not required, and the isotopy is required to satisfy ψ0=id\psi_0 = \mathrm{id}ψ0​=id only on MMM.

Setting and unfolded definitions. Throughout, n,c∈Nn, c \in \mathbb{N}n,c∈N are arbitrary natural numbers (both may be 000), and Rn\mathbb{R}^nRn means the space of functions {0,…,n−1}→R\{0,\dots,n-1\} \to \mathbb{R}{0,…,n−1}→R with the sup norm. A one-form α\alphaα is any map Rn→(Rn)∗\mathbb{R}^n \to (\mathbb{R}^n)^*Rn→(Rn)∗, y↦αyy \mapsto \alpha_yy↦αy​ (a continuous linear functional at each point; no regularity is built in). Derivatives DDD are Fréchet derivatives of maps on the ambient space Rn\mathbb{R}^nRn (or R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn), with the convention that a derivative is 000 at any point where the map is not differentiable. For F:Rn→RcF : \mathbb{R}^n \to \mathbb{R}^cF:Rn→Rc and a one-form α\alphaα:

  • Level set: M:=F−1(0)={y∈Rn:F(y)=0}M := F^{-1}(0) = \{ y \in \mathbb{R}^n : F(y) = 0 \}M:=F−1(0)={y∈Rn:F(y)=0}.

  • Compact regular level (hypothesis on FFF): FFF is C∞C^\inftyC∞ on all of Rn\mathbb{R}^nRn, MMM is compact, and for every y∈My \in My∈M the derivative DF(y):Rn→RcDF(y) : \mathbb{R}^n \to \mathbb{R}^cDF(y):Rn→Rc is surjective.

  • Tangent space: Ty:=ker⁡DF(y)={v∈Rn:DF(y) v=0}T_y := \ker DF(y) = \{ v \in \mathbb{R}^n : DF(y)\,v = 0 \}Ty​:=kerDF(y)={v∈Rn:DF(y)v=0} (defined for every yyy, used only for y∈My \in My∈M).

  • Exterior derivative: dαy(u,v):=(Dα(y) u)(v)−(Dα(y) v)(u)d\alpha_y(u,v) := \big(D\alpha(y)\,u\big)(v) - \big(D\alpha(y)\,v\big)(u)dαy​(u,v):=(Dα(y)u)(v)−(Dα(y)v)(u), where Dα(y):Rn→(Rn)∗D\alpha(y) : \mathbb{R}^n \to (\mathbb{R}^n)^*Dα(y):Rn→(Rn)∗ is the ambient derivative of y↦αyy \mapsto \alpha_yy↦αy​ (equal to 000 if α\alphaα is not differentiable at yyy).

  • Contact plane: ξy:={v∈Ty:αy(v)=0}\xi_y := \{ v \in T_y : \alpha_y(v) = 0 \}ξy​:={v∈Ty​:αy​(v)=0}.

  • Contact at yyy: (i) there exists v∈Tyv \in T_yv∈Ty​ with αy(v)≠0\alpha_y(v) \neq 0αy​(v)=0, and (ii) for every u∈ξyu \in \xi_yu∈ξy​ with u≠0u \neq 0u=0 there exists v∈ξyv \in \xi_yv∈ξy​ with dαy(u,v)≠0d\alpha_y(u,v) \neq 0dαy​(u,v)=0 (i.e. dαyd\alpha_ydαy​ restricted to ξy×ξy\xi_y \times \xi_yξy​×ξy​ is nondegenerate; condition (ii) is vacuous when ξy={0}\xi_y = \{0\}ξy​={0}). No orientation, sign, or dimension-parity condition is imposed explicitly.

  • Smooth family: a map t↦αtt \mapsto \alpha_tt↦αt​ from R\mathbb{R}R to one-forms such that (t,y)↦αt(y)∈(Rn)∗(t,y) \mapsto \alpha_t(y) \in (\mathbb{R}^n)^*(t,y)↦αt​(y)∈(Rn)∗ is C∞C^\inftyC∞ on all of R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn.

  • Contact family on MMM (hypothesis on α\alphaα): α\alphaα is a smooth family, and for every t∈[0,1]t \in [0,1]t∈[0,1] and every y∈My \in My∈M, αt\alpha_tαt​ is contact at yyy in the above sense. Nothing is required of αt\alpha_tαt​ for t∉[0,1]t \notin [0,1]t∈/[0,1] beyond smoothness, nor off MMM beyond smoothness.

  • Isotopy of MMM: a map ψ:R×Rn→Rn\psi : \mathbb{R} \times \mathbb{R}^n \to \mathbb{R}^nψ:R×Rn→Rn, (t,y)↦ψt(y)(t,y) \mapsto \psi_t(y)(t,y)↦ψt​(y), such that

    1. (t,y)↦ψt(y)(t,y) \mapsto \psi_t(y)(t,y)↦ψt​(y) is C∞C^\inftyC∞ on all of R×Rn\mathbb{R} \times \mathbb{R}^nR×Rn;
    2. ψ0(y)=y\psi_0(y) = yψ0​(y)=y for every y∈My \in My∈M (only on MMM, not on all of Rn\mathbb{R}^nRn);
    3. for every t∈[0,1]t \in [0,1]t∈[0,1]: ψt\psi_tψt​ maps MMM into MMM, is injective on MMM, and maps MMM onto MMM; and for every y∈My \in My∈M, the linear map Dψt(y)D\psi_t(y)Dψt​(y) is injective on TyT_yTy​.

    Nothing is required of ψt\psi_tψt​ for t∉[0,1]t \notin [0,1]t∈/[0,1] other than smoothness, and nothing off MMM other than smoothness. The definition does not state separately that Dψt(y)D\psi_t(y)Dψt​(y) maps TyT_yTy​ into Tψt(y)T_{\psi_t(y)}Tψt​(y)​.

  • Pullback: (ψt∗αt)y(v):=αt(ψt(y))(Dψt(y) v)(\psi_t^*\alpha_t)_y(v) := \alpha_t\big(\psi_t(y)\big)\big(D\psi_t(y)\,v\big)(ψt∗​αt​)y​(v):=αt​(ψt​(y))(Dψt​(y)v), where Dψt(y)D\psi_t(y)Dψt​(y) is the ambient derivative of ψt:Rn→Rn\psi_t : \mathbb{R}^n \to \mathbb{R}^nψt​:Rn→Rn at yyy. Edge cases of the hypotheses.

  • Surjectivity of DF(y)DF(y)DF(y) at points of MMM forces dim⁡Ty=n−c\dim T_y = n - cdimTy​=n−c there; if c>nc > nc>n then MMM must be empty.

  • If M=∅M = \emptysetM=∅ (e.g. c>nc > nc>n; or n=0n = 0n=0 and c≥1c \ge 1c≥1; or FFF a nonzero constant with c≥1c \ge 1c≥1), every condition quantified over MMM is vacuous: both hypotheses reduce to smoothness of FFF and of α\alphaα, and the conclusion only asks for smooth objects with no constraint coming from MMM.

  • Contact condition (i) requires Ty≠{0}T_y \neq \{0\}Ty​={0} at each y∈My \in My∈M, so a nonempty MMM needs n−c≥1n - c \ge 1n−c≥1. For c=0c = 0c=0 the target R0\mathbb{R}^0R0 is a point, so F≡0F \equiv 0F≡0 and M=RnM = \mathbb{R}^nM=Rn; compactness forces n=0n = 0n=0, and then Ty={0}T_y = \{0\}Ty​={0} violates (i). Hence for c=0c = 0c=0 the two hypotheses cannot hold simultaneously.

  • If n−c=1n - c = 1n−c=1, then ξy={0}\xi_y = \{0\}ξy​={0} and contact condition (ii) is vacuous; "contact" then only means that αt(y)\alpha_t(y)αt​(y) does not vanish identically on TyT_yTy​.

  • The contact condition and dαd\alphadα use the ambient derivative of αt\alpha_tαt​ on Rn\mathbb{R}^nRn, evaluated at points of MMM on vectors of ξy\xi_yξy​.

Human review
  • Endorsed by Shuze Chen · Oct 6, 2026

    Confirmed by the moderator at approval.

  • Endorsed by Mazecto · Oct 6, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me