Lemma 2.19: derivative of a pulled-back family of forms along a flow

Proved

GrayStability.pullback_family_hasDerivAt

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

contact-geometrydifferential-geometrysymplectic-geometry

Let $\eta_t$ be a smooth family of one-forms on $\mathbb{R}^n$ and $X_t$ a smooth time-dependent vector field. Let $\psi_t$ be a smooth family of bijections of $\mathbb{R}^n$ with $\psi_0=\mathrm{id}$ that is the flow of $X_t$ : $\partial_t\psi_t(y)=X_t(\psi_t(y))$ . Then for all $t$ , $y$ and $v$ ,

\frac{d}{dt}\big(\psi_t^*\eta_t\big)_y(v)=\big(\psi_t^*(\dot\eta_t+\mathcal{L}_{X_t}\eta_t)\big)_y(v),

where $(\psi^*\eta)_y(v)=\eta_{\psi(y)}(D\psi(y)v)$ and $(\mathcal{L}_X\eta)_y(v)=D\eta_y(X(y))(v)+\eta_y(DX(y)v)$ .

This is the identity that turns the equation $\psi_t^*\alpha_t=\lambda_t\alpha_0$ of Gray's theorem into an equation for the vector field $X_t$ (the Moser trick).

Preamble

import Definitions.Def_GrayStability_Basic

open scoped ContDiff

Formal statement

namespace GrayStability

/-- Geiges, Lemma 2.19 (one-forms on `ℝⁿ`): if `ψ_t` is an isotopy that is the flow of
the time-dependent vector field `X_t`, then
`d/dt (ψ_t^* η_t) = ψ_t^* (η̇_t + L_{X_t} η_t)`. -/
theorem pullback_family_hasDerivAt {n : ℕ} (η : ℝ → OneForm n) (hη : IsSmoothFamily η)
    (X : ℝ → E n → E n) (hX : ContDiff ℝ ∞ (fun p : ℝ × E n => X p.1 p.2))
    (ψ : ℝ → E n → E n) (hψ : ContDiff ℝ ∞ (fun p : ℝ × E n => ψ p.1 p.2))
    (h0 : ∀ y, ψ 0 y = y) (hbij : ∀ t, Function.Bijective (ψ t))
    (hflow : ∀ t y, HasDerivAt (fun s => ψ s y) (X t (ψ t y)) t)
    (t : ℝ) (y v : E n) :
    HasDerivAt (fun s => pullback (ψ s) (η s) y v)
      (formTimeDeriv η t (ψ t y) (fderiv ℝ (ψ t) y v) +
        lieDerivOneForm (X t) (η t) (ψ t y) (fderiv ℝ (ψ t) y v)) t := by sorry

end GrayStability

Source

Geiges, Contact geometry, Handbook of Differential Geometry Vol. II (2006) 315-382, https://arxiv.org/abs/math/0307242, Lemma 2.19, p. 13 (stated for

k

-forms on a manifold; here

k=1

\mathbb{R}^n

)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Data and hypotheses. Let $n \in \mathbb{N}$ be arbitrary and $\mathbb{R}^n$ carry the sup norm. Assume:

$(\eta_t)_{t \in \mathbb{R}}$ is a family of one-forms, $\eta_t : \mathbb{R}^n \to (\mathbb{R}^n)^*$ , such that $(t,z) \mapsto \eta_t(z)$ is $C^\infty$ on $\mathbb{R} \times \mathbb{R}^n$ ;
$(X_t)_{t \in \mathbb{R}}$ is a time-dependent vector field, $X_t : \mathbb{R}^n \to \mathbb{R}^n$ , with $(t,z) \mapsto X_t(z)$ $C^\infty$ on $\mathbb{R} \times \mathbb{R}^n$ ;
$(\psi_t)_{t \in \mathbb{R}}$ is a family of maps $\psi_t : \mathbb{R}^n \to \mathbb{R}^n$ with $(t,z) \mapsto \psi_t(z)$ $C^\infty$ on $\mathbb{R} \times \mathbb{R}^n$ ;
$\psi_0(z) = z$ for every $z \in \mathbb{R}^n$ ;
every $\psi_t$ ( $t \in \mathbb{R}$ ) is a bijection of $\mathbb{R}^n$ ;
for every $t \in \mathbb{R}$ and $z \in \mathbb{R}^n$ , $\displaystyle \frac{d}{ds}\Big|_{s=t} \psi_s(z) = X_t(\psi_t(z))$ (the derivative exists and has this value).

No level set, map $F$ or restriction to $[0,1]$ appears; everything is on all of $\mathbb{R}^n$ and all $t \in \mathbb{R}$ .

Conclusion. For every $t \in \mathbb{R}$ and $y, v \in \mathbb{R}^n$ , put $z = \psi_t(y)$ and $w = D\psi_t(y)\,v$ . Then the real function

s \longmapsto (\psi_s^*\eta_s)_y(v) = \eta_s\big(\psi_s(y)\big)\big(D\psi_s(y)\,v\big)

is differentiable at $s = t$ , with derivative

\frac{d}{ds}\Big|_{s=t} \eta_s(z)(w) \;+\; \big(D\eta_t(z)\,X_t(z)\big)(w) \;+\; \eta_t(z)\big(DX_t(z)\,w\big).

Here the first term is the derivative of $s \mapsto \eta_s(z)(w)$ at $s = t$ with $z, w$ frozen (the "time derivative" of the family), and the last two terms together are the Lie derivative $(\mathcal{L}_{X_t}\eta_t)_z(w)$ , where $D\eta_t(z) : \mathbb{R}^n \to (\mathbb{R}^n)^*$ and $DX_t(z)$ are Fréchet derivatives in the space variable. Under the smoothness hypotheses all derivatives appearing are genuine (no zero-by-convention values arise).

Remarks. The hypotheses $\psi_0 = \mathrm{id}$ and bijectivity of each $\psi_t$ are not referenced in the conclusion. The hypotheses are satisfiable (e.g. $X \equiv 0$ , $\psi_t = \mathrm{id}$ for all $t$ ). For $n = 0$ every quantity is $0$ .

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