structure SymplecticForm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] : Type (max u_1 u_3)

A symplectic form on $M$: a smoothly varying nondegenerate skew-symmetric bilinear form $\omega_x : E \times E \to \mathbb{R}$ at each point.

• form : M → E → E → ℝ
• bilinear_left (x : M) (a b : ℝ) (v₁ v₂ w : E) : self.form x (a • v₁ + b • v₂) w = a * self.form x v₁ w + b * self.form x v₂ w
• skewSymm (x : M) (v w : E) : self.form x v w = -self.form x w v
• nondegenerate (x : M) (v : E) : (∀ (w : E), self.form x v w = 0) → v = 0

def IsSymplectomorphism {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (ω : SymplecticForm I M) (φ : M → M) : Prop

$\varphi : M \to M$ is a symplectomorphism if $\varphi^* \omega = \omega$, i.e. $\omega_{\varphi(x)}(d\varphi_x v, d\varphi_x w) = \omega_x(v, w)$.

def IsCriticalPt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (f : M → ℝ) (x : M) : Prop

$x$ is a critical point of $f : M \to \mathbb{R}$ if $df_x = 0$.

def IsClosed1Form {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (μ : M → E →L[ℝ] ℝ) : Prop

A $1$-form $\mu : M \to E^*$ is closed if its derivative is symmetric: $D\mu_x(v)(w) = D\mu_x(w)(v)$.

def DeRhamH1Vanishes {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_3) [TopologicalSpace M] [ChartedSpace H M] : Prop

$H^1(M, \mathbb{R}) = 0$: every smooth closed $1$-form on $M$ is exact, i.e. $\mu = dh$ for some smooth $h$.

def IsC1CloseToId {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (φ : M → M) : Prop

$\varphi$ is $C^1$-close to the identity: smooth, with $\|d\varphi_x - \mathrm{id}\| < 1$ at every point.

theorem weinstein_identification_bridge {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [CompactSpace M] (ω : SymplecticForm I M) (φ : M → M) (hφ_sympl : IsSymplectomorphism I ω φ) (hφ_close : IsC1CloseToId I φ) : ∃ (μ : M → E →L[ℝ] ℝ), ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] ℝ)) ⊤ μ ∧ IsClosed1Form I μ ∧ ∀ (x : M), φ x = x ↔ μ x = 0

Via the Weinstein tubular neighborhood theorem, a $C^1$-close symplectomorphism produces a closed $1$-form whose zeros are exactly the fixed points of $\varphi$.

theorem weinstein_closed_one_form {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [CompactSpace M] (ω : SymplecticForm I M) (φ : M → M) (hφ_sympl : IsSymplectomorphism I ω φ) (hφ_close : IsC1CloseToId I φ) : ∃ (μ : M → E →L[ℝ] ℝ), ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] ℝ)) ⊤ μ ∧ IsClosed1Form I μ ∧ ∀ (x : M), φ x = x ↔ μ x = 0

Alias for the Weinstein identification bridge: produces a smooth closed $1$-form whose zero set coincides with the fixed-point set of $\varphi$.

theorem closed_form_exact_zeros_eq_crit {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (μ : M → E →L[ℝ] ℝ) (hμ_smooth : ContMDiff I (modelWithCornersSelf ℝ (E →L[ℝ] ℝ)) ⊤ μ) (hμ_closed : IsClosed1Form I μ) (hH1 : DeRhamH1Vanishes I M) : ∃ (h : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) ⊤ h ∧ ∀ (x : M), μ x = 0 ↔ IsCriticalPt I h x

When $H^1(M, \mathbb{R}) = 0$, a closed $1$-form $\mu$ is exact ($\mu = dh$), and its zeros are precisely the critical points of $h$.

theorem fixed_points_eq_critical_points {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [CompactSpace M] (ω : SymplecticForm I M) (φ : M → M) (hφ_sympl : IsSymplectomorphism I ω φ) (hφ_close : IsC1CloseToId I φ) (hH1 : DeRhamH1Vanishes I M) : ∃ (h : M → ℝ), ContMDiff I (modelWithCornersSelf ℝ ℝ) ⊤ h ∧ ∀ (x : M), φ x = x ↔ IsCriticalPt I h x

For a compact $M$ with $H^1(M, \mathbb{R}) = 0$, a $C^1$-close symplectomorphism $\varphi$ produces a smooth function $h$ whose critical points are precisely the fixed points of $\varphi$.

theorem mfderiv_eq_zero_of_isLocalMin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ⊤ M] {f : M → ℝ} {x : M} (hf : MDiffAt f x) (hlmin : IsLocalMin f x) : mfderiv% f x = 0

Fermat's lemma on manifolds: the manifold derivative of $f$ vanishes at any local minimum.

theorem mfderiv_eq_zero_of_isLocalMax {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ⊤ M] {f : M → ℝ} {x : M} (hf : MDiffAt f x) (hlmax : IsLocalMax f x) : mfderiv% f x = 0

Fermat's lemma on manifolds: the manifold derivative of $f$ vanishes at any local maximum.

theorem compact_manifold_two_critical_points {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ⊤ M] [CompactSpace M] [Nontrivial M] (f : M → ℝ) (hf : ContMDiff I (modelWithCornersSelf ℝ ℝ) ⊤ f) : ∃ (x : M) (y : M), x ≠ y ∧ IsCriticalPt I f x ∧ IsCriticalPt I f y

Any smooth function on a nontrivial compact manifold has at least two distinct critical points (its global minimum and maximum).

theorem symplectomorphism_fixed_points {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) [I.Boundaryless] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ⊤ M] [CompactSpace M] [Nontrivial M] (ω : SymplecticForm I M) (φ : M → M) (hφ_sympl : IsSymplectomorphism I ω φ) (hφ_close : IsC1CloseToId I φ) (hH1 : DeRhamH1Vanishes I M) : ∃ (x : M) (y : M), x ≠ y ∧ φ x = x ∧ φ y = y

Symplectomorphism fixed-point theorem (Theorem 1): for compact $(M, \omega)$ with $H^1(M, \mathbb{R}) = 0$, every symplectomorphism $C^1$-close to the identity has at least two distinct fixed points.