FC08 — John M. Lee, Introduction to Smooth Manifolds, 2nd ed. (2013)

FC08 — Lee, Introduction to Smooth Manifolds.

This chapter contains 26 definitions, 9 theorems, 14 propositions, 1 lemma, 1 corollary, 5 examples, 6 conventions and 2 other statements.

Of the 64 statements checked against Lean, 0 are formalized somewhere and 64 are not.

Status	Statements	Share	What it means
not formalized	64	100%	A documented search found no Lean statement of it anywhere.
checked in total	64

Which versions of Lean and Mathlib were searched

Canonical block: FC08-C22-U001–FC08-C22-U064, exactly 64 unique contiguous rows.
Search order: project A=3b2239e161592472b34e02ad3b7da308f9ce7280, pinned Mathlib P=db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0; Lean 4.33.0), current H=5315eef9e4ffb98e0f89f278b765c50a149f66ca (Apache-2.0; Lean 4.34.0-rc2), current Mathlib documentation, then indexed/current/external Lean search.
Result: 0 positive routes and 64 dated unmatched rows.
Linear-algebra search found BilinForm.Nondegenerate, BilinForm.finrank_orthogonal, and Mathlib.LinearAlgebra.SymplecticGroup (the canonical matrix symplectic group), but no general symplectic-vector-space structure or checked conversion from Lee’s alternating 2-covector representation. Under strict bundle semantics U001–U011 are not silently recoded through that gap.
Project search at A found no symplectic/Hamiltonian/Poisson/contact implementation. P/H/current documentation has no manifold symplectic module; the current public Mathlib index exposes the matrix symplectic-group module but no symplectic-manifold/Hamiltonian/contact counterpart.
U012–U024 also depend on the missing smooth manifold differential-form/exterior-derivative layer identified in FC08 C14–C18. U025–U042 need Hamiltonian/Poisson geometry; U043–U052 contact/Legendrian geometry; U053–U064 the resulting characteristic-flow treatment of nonlinear first-order PDEs. No complete checked owners were found for those layers.
N=2026-09-07 marks all negative decisions; strict whole-row semantics apply uniformly.

Definition/convention — nondegenerate

FC08-C22-U001 · Ch. 22, § Symplectic Tensors; source L16845 · not formalized

We begin with linear algebra. A 2-covector ! on a finite-dimensional vector space V is said to be nondegenerate if the linear map ! $V \to V ^ { * }$ defined by $\widehat { \omega } ( v ) = v \lrcorner \omega$ is invert element of the group.

Not formalized. none; no complete checked declaration under strict bundle semantics — Mathlib has BilinForm.Nondegenerate, bilinear orthogonals and finrank_orthogonal, and a matrix symplecticGroup, but no checked conversion/bridge from Lee’s alternating 2-covector representation to a general symplectic-vector-space object owning this whole row. The matrix symplectic group is only a fixed-coordinate special model. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Definition/convention — symplectic tensor

FC08-C22-U002 · Ch. 22, § Symplectic Tensors; source L16855 · not formalized

A nondegenerate 2-covector is called a symplectic tensor. A vector space V endowed with a specific symplectic tensor is called a symplectic vector space. (A symplectic tensor is also often called a “symplectic form,” because it is in particular a bilinear form. But to avoid confusion, we reserve that name for something slightly different, to be defined below.)

Example 22.2

FC08-C22-U003 · Ch. 22, § Symplectic Tensors; source L16857 · not formalized

Let $V$ be a vector space of dimension $2n$ with basis $(A_{1},B_{1},\dots,A_{n},B_{n})$, let $(\alpha^{1},\beta^{1},\dots,\alpha^{n},\beta^{n})$ be the dual basis for $V^{*}$, and let $\omega \in \Lambda^{2}(V^{*})$ be \[ \omega = \sum_{i=1}^{n} \alpha^{i} \wedge \beta^{i}. \tag{22.1} \] On basis vectors, \[ \omega(A_{i},A_{j}) = \omega(B_{i},B_{j}) = 0, \qquad \omega(A_{i},B_{j}) = -\omega(B_{j},A_{i}) = \delta_{ij}. \tag{22.2} \] If $v = a^{i}A_{i} + b^{i}B_{i} \in V$ satisfies $\omega(v,w) = 0$ for all $w \in V$, then $v = 0$; so $\omega$ is nondegenerate and hence a symplectic tensor. In the special case $\dim V = 2$, every nonzero 2-covector is symplectic.

Definition/convention — symplectic complement

FC08-C22-U004 · Ch. 22, § Symplectic Tensors; source L16873 · not formalized

If $(V,\omega)$ is a symplectic vector space and $S \subseteq V$ is a linear subspace, the symplectic complement of $S$ is \[ S^{\perp} = \{v \in V : \omega(v,w) = 0 \text{ for all } w \in S\}, \] analogous to the orthogonal complement in an inner product space.

Lemma 22.3

FC08-C22-U005 · Ch. 22, § Symplectic Tensors; source L16881 · not formalized

Let $(V,\omega)$ be a symplectic vector space. For any linear subspace $S \subseteq V$, $\dim S + \dim S^{\perp} = \dim V$.

Definition/convention — symplectic

FC08-C22-U006 · Ch. 22, § Symplectic Tensors; source L16893 · not formalized

Show that $( S ^ { \bot } ) ^ { \bot } = S$ Symplectic complements differ from orthogonal complements in one important respect: although it is always true that $S \cap S ^ { \perp } = \{ 0 \}$ in an inner product space, this need not be true in a symplectic vector space. Indeed, if S is 1-dimensional, the fact that ! is alternating forces $\omega ( v , v ) = 0$ for every $v \in S$ , so $S \subseteq S ^ { \bot }$ . Carrying this idea a little further, a linear subspace $S \subseteq V$ is said to be symplectic if $S \cap S ^ { \perp } = \{ 0 \} ;$ isotropic if $S \subseteq S ^ { \bot } ;$ coisotropic if $S \supseteq S ^ { \bot } ;$ Lagrangian if $S = S ^ { \perp } .$ Proposition 22.5. Let $( V , \omega )$

Proposition 22.5

FC08-C22-U007 · Ch. 22, § Symplectic Tensors; source L16903 · not formalized

Let $(V,\omega)$ be a symplectic vector space and $S \subseteq V$ a linear subspace. (a) $S$ is symplectic if and only if $S^{\perp}$ is symplectic. (b) $S$ is symplectic if and only if $\omega|_{S}$ is nondegenerate. (c) $S$ is isotropic if and only if $\omega|_{S} = 0$. (d) $S$ is coisotropic if and only if $S^{\perp}$ is isotropic. (e) $S$ is Lagrangian if and only if $\omega|_{S} = 0$ and $\dim S = \tfrac{1}{2}\dim V$.

Proposition 22.7

FC08-C22-U008 · Ch. 22, § Symplectic Tensors; source L16931 · not formalized

Proposition 22.7 (Canonical Form for a Symplectic Tensor). Let ! be a symplectic tensor on an m-dimensional vector space V . Then V has even dimension $m = 2 n$ , and there exists a basis for V in which ! has the form (22.1)

Definition/convention — symplectic basis

FC08-C22-U009 · Ch. 22, § Symplectic Tensors; source L16939 · not formalized

If $(V,\omega)$ is a symplectic vector space, a basis $(A_{1},B_{1},\dots,A_{n},B_{n})$ for $V$ is a symplectic basis if (22.2) holds, equivalently if $\omega$ is given by (22.1) in terms of the dual basis. The proposition says every symplectic vector space has a symplectic basis.

Convention/notation — source terminology/construction

FC08-C22-U010 · Ch. 22, § Symplectic Tensors; source L16941 · not formalized

This leads to another useful criterion for 2-covector to be nondegenerate. For an alternating tensor $\omega$ , the notation $\omega ^ { k }$ denotes the k-fold wedge the set of orbits forms a foliation of M whose leaves are embedded submanifolds diffeomorphic to $G$ .

Proposition 22.8

FC08-C22-U011 · Ch. 22, § Symplectic Tensors; source L16943 · not formalized

Suppose $V$ is a $2n$-dimensional vector space and $\omega \in \Lambda^{2}(V^{*})$. Then $\omega$ is a symplectic tensor if and only if $\omega^{n} \neq 0$.

Definition/convention — symplectic manifold

FC08-C22-U012 · Ch. 22, § Symplectic Structures on Manifolds; source L16955 · not formalized

A nondegenerate 2-form on M is a 2- form ! such that $\omega _ { p }$ is a nondegenerate 2-covector for each $p \in M$ . A symplectic form on M is a closed nondegenerate 2-form. A smooth manifold endowed with a specific choice of symplectic form is called a symplectic manifold. A choice of symplectic form is also sometimes called a symplectic structure.

Not formalized. none; no complete checked declaration under strict bundle semantics — P/H/current Mathlib has no manifold symplectic-form structure, no smooth differential-form exterior derivative, no tautological cotangent 1-form/canonical symplectic form, and no symplectic Darboux theorem. Adjacent manifold/tensor infrastructure cannot state the complete row. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Definition/convention — symplectomorphism

FC08-C22-U013 · Ch. 22, § Symplectic Structures on Manifolds; source L16959 · not formalized

If $( M _ { 1 } , \omega _ { 1 } )$ and $( M _ { 2 } , \omega _ { 2 } )$ are symplectic manifolds, a diffeomorphism F $M _ { 1 } $ $M _ { 2 }$ satisfying $F ^ { * } \omega _ { 2 } = \omega _ { 1 }$ is called a symplectomorphism. The study of properties of symplectic manifolds that are invariant under symplectomorphisms is known as symplectic geometry or symplectic topology.

Example 22.9

FC08-C22-U014 · Ch. 22, § Symplectic Structures on Manifolds; source L16961 · after FC08-C22-U003 · not formalized

Example 22.9 (Symplectic Manifolds). (a) With standard coordinates on $\mathbb { R } ^ { 2 n }$ denoted by { 1 } , , x ^ { n } )$ , the $2 \AA ^ { - }$ form \[ \omega = \sum_ {i = 1} ^ {n} d x ^ {i} \wedge d y ^ {i} \] is symplectic: it is obviously closed, and it is nondegenerate because its value at each point is the symplectic tensor of Example 22.2. This is called the standard symplectic form on $ } ^ { 2 n }$ . (In formulas involving the standard symplectic form, like those involving the Euclidean inner product, it is usually necessary to insert explicit summation signs, because the summation index i appears twice in the upper position.) (b) Suppose ˙ is any orientable smooth 2-manifold and ! is a nonvanishing smooth 2-form on ˙. Then ! is closed because d! is a 3-form on a 2-manifold. Moreover, as we observed just after Example 22.2, in two dimensions every nonvanishing 2-form is nondegenerate, so .˙; !/ is a symplectic manifold. Suppose $

Convention/notation — standard symplectic form

FC08-C22-U015 · Ch. 22, § Symplectic Structures on Manifolds; source L16969 · after FC08-C22-U003 · not formalized

is symplectic: it is obviously closed, and it is nondegenerate because its value at each point is the symplectic tensor of Example 22.2. This is called the standard symplectic form on $\bar { \mathbb { R } } ^ { 2 n }$ . (In formulas involving the standard symplectic form, like those involving the Euclidean inner product, it is usually necessary to insert explicit summation signs, because the summation index i appears twice in the upper positio To complete the proof of the claim, we need to show that we can find a cubical subset $U _ { 0 } \subseteq U$ centered at $p$ that intersects each G-orbit in at most a single slice.

Definition/convention — a symplectic

FC08-C22-U016 · Ch. 22, § Symplectic Structures on Manifolds; source L16973 · not formalized

Suppose $( M , \omega )$ is a symplectic manifold. An (immersed or embedded) submanifold $S \subseteq M$ is said to be a symplectic, isotropic, coisotropic, or Lagrangian submanifold if $T _ { p } S$ (thought of as a subspace of $T _ { p } M )$ has the corresponding property at each point $p \in S$ . More generally, a smooth immersion (or embedding) $F \colon N \to M$ is said to have one of these properties if the subspace $d F _ { p } ( T _ { p } N ) \subseteq$ $T _ { F ( p ) } M$ has the corresponding property for every $p \in N$ . Thus a submanifold is symplectic (isotropic, etc.) if and only if its inclusion map has the same property.

Convention/notation — tautological 1-form

FC08-C22-U017 · Ch. 22, § The Canonical Symplectic Form on the Cotangent Bundle; source L16982 · not formalized

The most important symplectic manifolds are total spaces of cotangent bundles, which carry canonical symplectic structures that we now define. First, there is a natural 1-form $\tau$ on the total space of $T ^ { * } M$ ; called the tautological 1-form, defined as follows. A point in $T ^ { * } M$ is a covector $\varphi \in T _ { q } ^ { * } M$ for some $q \in M$ ; we denote such a point by the notation $( q , \varphi )$ . The natural projection $\pi \colon T ^ { * } M \to M$ is then just $\left( q , \varphi \right) = q$ , and its pointwise pullback at $q$ is a linear map $d \pi _ { ( q , \varphi ) } ^ { * } \colon T _ { q } ^ { * } M \to$ $T _ { ( q , \varphi ) } ^ { * } ( T ^ { * } M )$ . We define $\tau \in \Omega ^ { 1 } ( T ^ { * } M )$ (a 1-form on the total space of $T ^ { * } M )$ ) by \[ \tau_ {(q, \varphi)} = d \pi_ {(q, \varphi)} ^ {*} \varphi .\tag{22.3} \] (See Fig. 22.1.) In other words, the value of $\tau$ at $( q , \varphi ) \in T ^ { * } M$ is the pullback with respect to $\pi$ of the covector $\varphi$ itself. If v is a tangent vector in $T _ { ( q , \varphi ) } ( T ^ { * } M )$ , then \[ \tau_ {(q, \varphi)} (v) = \varphi \big (d \pi_ {(q, \varphi)} (v) \big). \]

Proposition 22.11

FC08-C22-U018 · Ch. 22, § The Canonical Symplectic Form on the Cotangent Bundle; source L16994 · not formalized

Proposition 22.11. Let M be a smooth manifold. The tautological 1-form is smooth, and $\omega = - d \tau$ is a symplectic form on the total space of $T ^ { * } M$

Definition/convention — canonical symplectic form

FC08-C22-U019 · Ch. 22, § The Canonical Symplectic Form on the Cotangent Bundle; source L17012 · not formalized

symplectic. The symplectic form defined in this proposition is called the canonical symplectic form on ${ \pmb T } ^ { * } { \pmb M }$ . One of its many uses is in giving the following somewhat more “geometric” interpretation of what it means for a 1-form to be clo ending the equivalence class of a point $( x , y )$ to $y ;$ this is well defined by the definition of an adapted chart.

Proposition 22.12

FC08-C22-U020 · Ch. 22, § The Canonical Symplectic Form on the Cotangent Bundle; source L17014 · not formalized

Proposition 22.12. Let M be a smooth manifold, and let be a smooth 1-form on M . Thought of as a smooth map from M to T M; is a smooth embedding, and is closed if and only if its image .M / is a Lagrangian submanifold of T M . P

Theorem 22.13

FC08-C22-U021 · Ch. 22, § The Darboux Theorem; source L17050 · not formalized

Theorem 22.13 (Darboux). Let .M; !/ be a 2n-dimensional symplectic manifold. For any $p \in M$ ; there are smooth coordinates $\left( x ^ { 1 } , \ldots , x ^ { n } , y ^ { 1 } , \ldots , y ^ { n } \right)$ centered at $p$ in which ! has the coordinate representation \[ \omega = \sum_ {i = 1} ^ {n} d x ^ {i} \wedge d y ^ {i}.\tag{22.5} \]

Definition/convention — Darboux coordinates

FC08-C22-U022 · Ch. 22, § The Darboux Theorem; source L17056 · after FC08-C22-U018 · not formalized

Coordinates satisfying (22.5) are called Darboux coordinates, symplectic coordinates or canonical coordinates. The standard coordinates $(x^{1},\dots,x^{n},y^{1},\dots,y^{n})$ on $\mathbb{R}^{2n}$ are Darboux coordinates, and the proof of Proposition 22.11 showed that the natural coordinates $(x^{i},\xi_{i})$ are Darboux coordinates for $T^{*}M$ with its canonical symplectic structure.

Proposition 22.14

FC08-C22-U023 · Ch. 22, § The Darboux Theorem; source L17064 · not formalized

Let $M$ be a smooth manifold, $V \colon J \times M \to TM$ a smooth time-dependent vector field and $\psi \colon \mathcal{E} \to M$ its time-dependent flow. For any smooth covariant tensor field $A \in \mathcal{T}^{k}(M)$ and any $(t_{1},t_{0},p) \in \mathcal{E}$, \[ \left.\frac{d}{dt}\right|_{t=t_{1}} \left(\psi_{t,t_{0}}^{*}A\right)_{p} = \left(\psi_{t_{1},t_{0}}^{*}\left(\mathcal{L}_{V_{t_{1}}}A\right)\right)_{p}. \tag{22.6} \]

Proposition 22.15

FC08-C22-U024 · Ch. 22, § The Darboux Theorem; source L17116 · not formalized

Proposition 22.15. Let M be a smooth manifold and $J \subseteq \mathbb { R }$ be an open interval. Suppose V $J \times M$ is a smooth time-dependent vector field on M; $\psi \colon \mathcal { E } \to M$ is its time-dependent flow, and $A \colon J \times M \to T ^ { k } T ^ { * } M$ is a smooth time-dependent tensor field on M . Then for any $( t _ { 1 } , t _ { 0 } , p ) \in \mathcal { E }$ \[ \left. \frac {d}{d t} \right| _ {t = t _ {1}} \left(\theta_ {t, t _ {0}} ^ {*} A _ {t}\right) _ {p} = \left( \right.\theta_ {t _ {1}, t _ {0}} ^ {*} \left( \right.\mathscr {L} _ {V _ {t _ {1}}} A _ {t _ {1}} + \frac {d}{d t} \left. \right| _ {t = t _ {1}} A _ {t}\left. \right)\left. \right) _ {p}.\tag{22.8} \]

Definition/convention — Hamiltonian vector field of f to be the smooth vector field X

FC08-C22-U025 · Ch. 22, § Hamiltonian Vector Fields; source L17166 · not formalized

Suppose $(M,\omega)$ is a symplectic manifold. For any smooth function $f \in C^{\infty}(M)$, the Hamiltonian vector field of $f$ is the smooth vector field $X_{f}$ defined by \[ X_{f} = \widehat{\omega}^{-1}(df), \] where $\widehat{\omega} \colon TM \to T^{*}M$ is the bundle isomorphism determined by $\omega$; equivalently, $X_{f} \lrcorner\, \omega = df$.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H/current/external search finds no Hamiltonian vector field/system, Poisson bracket on smooth functions, Noether theorem, or Hamiltonian flowout theory for symplectic manifolds. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Proposition 22.16

FC08-C22-U026 · Ch. 22, § Hamiltonian Vector Fields; source L17212 · not formalized

Proposition 22.16 (Properties of Hamiltonian Vector Fields). Let $( M , \omega )$ be a symplectic manifold and let $f \in C ^ { \infty } ( M )$ (a) f is constant along each integral curve of X . (b) At each regular point of f , the Hamiltonian vector field Xf is tangent to the level set of f .

Definition/convention — symplectic

FC08-C22-U027 · Ch. 22, § Hamiltonian Vector Fields; source L17226 · not formalized

A smooth vector field X on M is said to be symplectic if ! is invariant under the flow of X . It is said to be Hamiltonian (or globally Hamiltonian) if there exists a function $f \in C ^ { \infty } ( M )$ such that $X = X _ { f }$ and locally Hamiltonian if each point p has a neighborhood on which X is Hamiltonian. Clearly, every globally Hamiltonian vector field is locally Hamiltonian.

Proposition 22.17

FC08-C22-U028 · Ch. 22, § Hamiltonian Vector Fields; source L17228 · not formalized

Proposition 22.17 (Hamiltonian and Symplectic Vector Fields). Let $( M , \omega )$ be a symplectic manifold. A smooth vector field on M is symplectic if and only if it is locally Hamiltonian. Every locally Hamiltonian vector field on M is globally Hamiltonian if and only group of G.

Definition/convention — Hamiltonian system

FC08-C22-U029 · Ch. 22, § Hamiltonian Vector Fields; source L17240 · not formalized

A symplectic manifold ( M , ω ) together with a smooth function H ∈ C ^∞ ( M ) is called a Hamiltonian system. The function H is called the Hamiltonian of the system; the flow of the Hamiltonian vector field X _H is called its Hamiltonian flow, and the integral curves of X _H are called the trajectories or orbits of the system. In Darboux coordinates, formula (22.9) implies that the orbits are those curves γ ( t ) = ( x ^i ( t ) , y ^i ( t ) ) that satisfy \[ \dot{x}^{i}(t) = \frac{\partial H}{\partial y^{i}}\big(x(t),y(t)\big), \qquad \dot{y}^{i}(t) = -\frac{\partial H}{\partial x^{i}}\big(x(t),y(t)\big). \tag{22.11} \]

Definition/convention — Hamilton

FC08-C22-U030 · Ch. 22, § Hamiltonian Vector Fields; source L17250 · not formalized

(with dots denoting ordinary derivatives of component functions with respect to t). These are called Hamilton’s equations.

Example 22.18

FC08-C22-U031 · Ch. 22, § Hamiltonian Vector Fields; source L17254 · not formalized

(The $n$-Body Problem). Consider $n$ particles of masses $m_{1},\dots,m_{n}$ moving in space, idealized as points $\mathbf{q}_{1},\dots,\mathbf{q}_{n} \in \mathbb{R}^{3}$, with conservative forces, so that $F = -dV$ for a potential energy $V \in C^{\infty}(Q)$. Newton’s second law gives $m_{k}\ddot{\mathbf{q}}_{k}(t) = \mathbf{F}_{k}(\mathbf{q}(t))$ for each $k$, a system of $3n$ second-order ODEs with no implied summation. Relabelling the positions as $q(t) = (q^{1}(t),\dots,q^{3n}(t))$ and the forces as $F(q) = (F_{1}(q),\dots,F_{3n}(q))$, and letting $M = (M_{ij})$ be the diagonal $3n \times 3n$ matrix with entries $(m_{1},m_{1},m_{1},\dots,m_{n},m_{n},m_{n})$, positivity of the masses makes $M$ a constant-coefficient Riemannian metric on $Q$ and hence a smooth bundle isomorphism $\widehat{M} \colon TQ \to T^{*}Q$, with \[ (q^{i},p_{i}) = \widehat{M}(q^{i},v^{i}) = (q^{i},\ M_{ij}v^{j}). \] The total energy $E \in C^{\infty}(T^{*}Q)$ is $E(q,p) = V(q) + K(p)$ with kinetic energy $K(p) = \tfrac{1}{2}M^{ij}p_{i}p_{j}$. Since $(q^{i},p_{i})$ are Darboux coordinates, (22.14) is exactly Hamilton’s equations for the Hamiltonian flow of $E$; that $E$ is constant along its own trajectories is the law of conservation of energy.

Convention/notation — potential energy of the system)

FC08-C22-U032 · Ch. 22, § Hamiltonian Vector Fields; source L17284 · not formalized

(Here the summation convention is in force.) We assume that the forces depend smoothly on $q ,$ so we can interpret $F ( q ) = ( F _ { 1 } ( q ) , \dots , F _ { 3 n } ( q ) )$ / as the components of a smooth covector field on Q. We assume further that the forces are conservative, which by the results of Chapter 11 is equivalent to the existence of a smooth function $V \in C ^ { \infty } ( Q )$ (called the potential energy of the system) such that $F = - d V$

Convention/notation — source terminology/construction

FC08-C22-U033 · Ch. 22, § Hamiltonian Vector Fields; source L17286 · not formalized

Under the physically reasonable assumption that all of the masses are positive, the matrix M is positive definite, and thus can be interpreted as a (constantcoefficient) Riemannian metric on Q . It therefore defines a smooth bundle isomorphism hat(M) : T Q → T * Q . If we denote the natural coordinates on T Q by ( q ^i , v ^i ) and those on T * Q by ( q ^i , p _i ) , then M ( v , w ) = M _i j v ^i w ^j , and hat(M) has the coordinate representation \[ (q^{i},p_{i}) = \widehat{M}(q^{i},v^{i}) = (q^{i}, M_{ij}v^{j}). \]

Definition/convention — total energy of the system

FC08-C22-U034 · Ch. 22, § Hamiltonian Vector Fields; source L17318 · not formalized

With $(M^{ij})$ the inverse of the matrix $(M_{ij})$, the total energy of the system is the function $E \in C^{\infty}(T^{*}Q)$ given by \[ E(q,p) = V(q) + K(p), \] where $V$ is the potential energy and $K$ the kinetic energy, \[ K(p) = \tfrac{1}{2}M^{ij}p_{i}p_{j}. \]

Definition/convention — their Poisson bracket f

FC08-C22-U035 · Ch. 22, § Poisson Brackets; source L17336 · not formalized

Brackets Hamiltonian vector fields allow us to define an operation on real-valued functions on a symplectic manifold M similar to the Lie bracket of vector fields. Given $f , g \in$ $C ^ { \infty } ( M )$ , we define their Poisson bracket $\{ f , g \} \in C ^ { \infty } ( M )$ by any of the following equivalent formulas: \[ \{f, g \} = \omega (X _ {f}, X _ {g}) = d f (X _ {g}) = X _ {g} f.\tag{22.15} \]

Proposition 22.19

FC08-C22-U036 · Ch. 22, § Poisson Brackets; source L17352 · not formalized

Proposition 22.19 (Properties of the Poisson Bracket). Suppose $( M , \omega )$ is a symplectic manifold, and $f , g , h \in C ^ { \infty } ( M )$ (a) BILINEARITY: $\{ f , g \}$ is linear over R in f and in $g$ . (b) ANTISYMMETRY: $\{ f , g \} = - \{ g , f \}$ (c) JACOBI IDENTITY: $\{ \{ f , g \} , h \} + \{ \{ g , h \} , f \} + \{ \{ h , f \} , g \} = 0 .$ (d) $X _ { \{ f , g \} } = - [ X _ { f } , X _ { g } ] .$

Corollary 22.20

FC08-C22-U037 · Ch. 22, § Poisson Brackets; source L17390 · not formalized

If $(M,\omega)$ is a symplectic manifold, the vector space $C^{\infty}(M)$ is a Lie algebra under the Poisson bracket.

Definition/convention — conserved quantity of the system

FC08-C22-U038 · Ch. 22, § Poisson Brackets; source L17392 · not formalized

If $( M , \omega , H )$ is a Hamiltonian system, any function $f \in C ^ { \infty } ( M )$ that is constant on every integral curve of $X _ { H }$ is called a conserved quantity of the system. Conserved quantities turn out to be deeply related to symmetries, as we now show.

Definition/convention — infinitesimal symmetry of ( M

FC08-C22-U039 · Ch. 22, § Poisson Brackets; source L17394 · not formalized

A smooth vector field V on M is called an infinitesimal symmetry of $( M , \omega , H )$ if both ! and H are invariant under the flow of $V$

Proposition 22.21

FC08-C22-U040 · Ch. 22, § Poisson Brackets; source L17396 · not formalized

Proposition 22.21. Let $( M , \omega , H )$ be a Hamiltonian system. (a) A function $f \in C ^ { \infty } ( M )$ is a conserved quantity if and only $i f \left\{ f , H \right\} = 0$ (b) The infinitesimal symmetries of $( M , \omega , H )$ are precisely the symplectic vector fields V that satisfy $V H = 0$ (c) If is the flow of an infinitesimal symmetry and is a trajectory of the system, then for each $s \in \mathbb { R } , \theta _ { s } \circ \gamma$ is also a trajectory on its domain nd the projection $\pi \colon G \to G / K$ sending each element of G to its coset is a surjective homomorphism whose kernel is K.

Theorem 22.22

FC08-C22-U041 · Ch. 22, § Poisson Brackets; source L17408 · not formalized

Theorem 22.22 (Noether’s Theorem). $L e t \left( { \cal M } , \omega , { \cal H } \right)$ be a Hamiltonian system. If f is any conserved quantity, then its Hamiltonian vector field is an infinitesimal symmetry. Conversely, if $H _ { \mathrm { d R } } ^ { 1 } ( M ) = 0$ , then each infinitesimal symmetry is the Hamiltonian vector field of a conserved quantity, which is unique up to addition of a function that is constant on each com ).

Theorem 22.23

FC08-C22-U042 · Ch. 22, § Hamiltonian Flowouts; source L17420 · not formalized

Theorem 22.23 (Hamiltonian Flowout Theorem). Suppose $( M , \omega )$ is a symplectic manifold, $H \in C ^ { \infty } ( M )$ , is an embedded isotropic submanifold of M that is contained in a single level set of H , and the Hamiltonian vector field $X _ { H }$ is nowhere tangent to . If is a flowout from along $X _ { H }$ , then is also isotropic and contained in the same level set of H .

Definition/convention — contact form for H

FC08-C22-U043 · Ch. 22, § Contact Structures; source L17442 · not formalized

Suppose M is a smooth manifold of odd dimension $2 n + 1$ . A contact form on M is a nonvanishing smooth 1-form $\theta$ with the property that for each $p \in M$ the restriction of $d \theta _ { p }$ to the subspace Ker $\theta _ { p } \subseteq T _ { p } M$ is nondegenerate, which is to say it is a symplectic tensor. A contact structure on M is a smooth distribution $H \subseteq T M$ of rank 2n with the property that any smooth local defining form for H is a contact form. A contact manifold is a smooth manifold M together with a contact structure on M . If .M; H / is a contact manifold, any (local or global) defining form for H is called a contact form for H . It was proved in 1971 by Jean Martinet [Mar71] that every oriented compact smooth 3-manifold admits a contact structure; but the question of which higher-dimensional manifolds admit contact structures is still unresolved.

Not formalized. none; no complete checked declaration under strict bundle semantics — Targeted P/H/current/external search finds no contact-form/contact-structure object, Reeb field, contact Darboux theorem, contact Hamiltonian vector field, or Legendrian/contact-flowout theory; the differential-form and smooth-distribution prerequisites are also absent. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Proposition 22.24

FC08-C22-U044 · Ch. 22, § Contact Structures; source L17444 · not formalized

A smooth 1-form $\theta$ on a $(2n+1)$-manifold $M$ is a contact form if and only if $\theta \wedge (d\theta)^{n}$ is nowhere zero on $M$, where $(d\theta)^{n}$ is the $n$-fold wedge product $d\theta \wedge \cdots \wedge d\theta$.

Example 22.27

FC08-C22-U045 · Ch. 22, § Contact Structures; source L17452 · after FC08-C22-U003, FC08-C22-U007 · not formalized

(Contact Forms). (a) On $\mathbb{R}^{2n+1}$ with coordinates $(x^{1},\dots,x^{n},y^{1},\dots,y^{n},z)$, the 1-form \[ \theta = dz - \sum_{i=1}^{n} y^{i}\,dx^{i} \tag{22.19} \] annihilates a rank-$2n$ distribution $H \subseteq T\mathbb{R}^{2n+1}$ on which $d\theta$ is nondegenerate, so $\theta$ is a contact form. (b) For a smooth $n$-manifold $M$, the 1-form $\theta = dz - \tau$ on $\mathbb{R} \times T^{*}M$, where $z$ is the standard coordinate on $\mathbb{R}$ and $\tau$ the tautological 1-form, has the coordinate representation $\theta = dz - \sum_{i=1}^{n} \xi_{i}\,dx^{i}$ and is a contact form by the same argument. (c) On $\mathbb{R}^{2n+2}$ with coordinates $(x^{1},\dots,x^{n+1},y^{1},\dots,y^{n+1})$, consider $\Theta = \sum_{i=1}^{n+1}(x^{i}\,dy^{i} - y^{i}\,dx^{i})$. Then \[ N \lrcorner\, d\Theta = 2\Theta, \qquad T \lrcorner\, d\Theta = d\left(|x|^{2}+|y|^{2}\right), \] so $S_{p}^{\perp}$ is the common kernel of $\Theta_{p}$ and $d(|x|^{2}+|y|^{2})_{p}$, which is $\operatorname{Ker}\Theta_{p} \cap T_{p}\mathbb{S}^{2n+1} = \operatorname{Ker}\theta_{p}$.

Theorem 22.28

FC08-C22-U046 · Ch. 22, § Contact Structures; source L17496 · not formalized

(The Reeb Field). Let $(M,H)$ be a contact manifold and $\theta$ a contact form for $H$. There is a unique vector field $T \in \mathfrak{X}(M)$, the Reeb field of $\theta$, satisfying \[ T \lrcorner\, d\theta = 0, \qquad \theta(T) = 1. \tag{22.20} \]

Theorem 22.31

FC08-C22-U047 · Ch. 22, § Contact Structures; source L17514 · not formalized

Theorem 22.31 (Contact Darboux Theorem). Suppose $\theta$ is a contact form on a $( 2 n + 1 )$ -dimensional manifold M . For each $p \in M$ ; there are smooth coordinates $\left( x ^ { 1 } , \ldots , x ^ { n } , y ^ { 1 } , \ldots , y ^ { n } , z \right)$ centered at p in which has the form (22.19).

Proposition 22.32

FC08-C22-U048 · Ch. 22, § Contact Structures; source L17520 · not formalized

Proposition 22.32. Suppose $( M , H )$ is a contact manifold and $\theta$ is a contact form for H . For any function $f \in C ^ { \infty } ( M )$ , there is a unique vector field $X _ { f }$ called the contact Hamiltonian vector field of $f$ , that satisfies $\theta ( X _ { f } ) = f$ and $( X _ { f } \lrcorner d \theta ) | _ { H } = - d f | _ { H }$

Definition/convention — contact vector field

FC08-C22-U049 · Ch. 22, § Contact Structures; source L17524 · not formalized

Suppose $(M,H)$ is a contact manifold. A smooth vector field $X \in \mathfrak{X}(M)$ is a contact vector field if its flow $\theta$ preserves the contact structure: $d(\theta_{t})_{p}(H_{p}) = H_{\theta_{t}(p)}$ for all $(t,p)$ in the domain of $\theta$.

Theorem 22.33

FC08-C22-U050 · Ch. 22, § Contact Structures; source L17526 · not formalized

Theorem 22.33 (Characterization of Contact Vector Fields). $H ( M , H )$ is a contact manifold and is a contact form for H , then a smooth vector field on M is a contact vector field if and only if it is a contact Hamiltonian vector freely on a smooth manifold M; and the orbit space $M / G$ has a smooth manifold structure such that the quotient map $M \to M / G$ is a smooth submersion, then G acts properly.

Definition/convention — Legendrian submanifold

FC08-C22-U051 · Ch. 22, § Contact Structures; source L17530 · not formalized

If $(M,H)$ is a contact manifold, a smooth submanifold $S \subseteq M$ is isotropic if $TS \subseteq H$, equivalently if $\iota^{*}\theta = 0$ for any contact form $\theta$, where $\iota \colon S \hookrightarrow M$ is the inclusion. Then $\iota^{*}d\theta = d(\iota^{*}\theta) = 0$, so each $T_{p}S$ is an isotropic subspace of the symplectic vector space $H_{p}$ and has dimension at most $n$, where $\dim M = 2n+1$. An isotropic submanifold of the maximal dimension $n$ is a Legendrian submanifold.

Theorem 22.34

FC08-C22-U052 · Ch. 22, § Contact Structures; source L17534 · not formalized

Theorem 22.34 (Contact Flowout Theorem). Suppose .M; H / is a contact manifold, $F \in C ^ { \infty } ( M )$ , is an embedded isotropic submanifold of M that is contained in the zero set of F , and the contact Hamiltonian vector field $X _ { F }$ is nowhere tangent to . If is a flowout from along $X _ { F }$ , then is also isotropic and contained in the zero set of H .

Definition/convention — Hamilton

FC08-C22-U053 · Ch. 22, § Nonlinear First-Order PDEs; source L17542 · not formalized

begin with a somewhat special case. A first-order partial differential equation that involves only the first derivatives of the unknown function but not the values of the function itself is called a Hamilton–Jacobi equation. Such an equation for an unknown function $u ( x ^ { 1 } , \ldots , x ^ { n } )$ can be written in the form \[ F \left(x ^ {1}, \dots , x ^ {n}, \frac {\partial u}{\partial x ^ {1}} (x), \dots , \frac {\partial u}{\partial x ^ {n}} (x)\right) = 0,\tag{22.21} \] where $F$ is a smooth function defined on an open subset of $\mathbb { R } ^ { 2 n }$ . (The terminology regarding Hamilton–Jacobi equations is not universally agreed upon. Some authors reserve the term Hamilton–Jacobi equation for the special case of an equation of the form \[ \frac {\partial u}{\partial x ^ {1}} + H \left(x ^ {1}, \dots , x ^ {n}, \frac {\partial u}{\partial x ^ {2}} (x), \dots , \frac {\partial u}{\partial x ^ {n}} (x)\right) = 0.\tag{22.22} \] The implicit function theorem shows that an equation of the general form (22.21) can be locally rewritten in this special form if and only if the partial derivative of F with respect to its $( n + 1 )$ st variable is nonzero. On the other hand, other authors use the term eikonal equation to refer to any equation of the form (22.21). We reserve that term for another special case to which it was originally applied; see Problem

Not formalized. none; no complete checked declaration under strict bundle semantics — The row requires Lee’s symplectic/contact geometry and first-order PDE characteristic-flow construction (cotangent/1-jet bundles, Hamiltonian/contact Hamiltonian fields, Legendrian flowouts). P/H have generic calculus/ODE/PDE-adjacent ingredients but no checked theorem implementing this source construction. Strict whole-row semantics reject proper subsets, unbridged alternate encodings, and reconstruction.

Definition/convention — solution to the equation

FC08-C22-U054 · Ch. 22, § Nonlinear First-Order PDEs; source L17560 · not formalized

More generally, if M is a smooth manifold, a Hamilton–Jacobi equation on M is given by a smooth real-valued function $F$ defined on an open subset $W \subseteq T ^ { * } M$ and a solution to the equation is a smooth real-valued function u defined on an open subset $U \subseteq M$ such that the image of du lies in the zero set of $F$ : \[ F (x, d u (x)) = 0 \quad \text { for all } x \in U.\tag{22.23} \]

Convention/notation — source terminology/construction

FC08-C22-U055 · Ch. 22, § Nonlinear First-Order PDEs; source L17566 · not formalized

(We write the covector d u _x ∈ T _x * M as ( x , d u ( x ) ) , in order to be more consistent with the coordinate representation (22.21) of the equation.) We are interested in solving a Cauchy problem for (22.23): given an embedded hypersurface S ⊆ M and a smooth function φ : S ℝ , we wish to find a smooth function u defined on a neighborhood of S in M and satisfying (22.23) together with the initial condition \[ u\big|_{S} = \varphi. \tag{22.24} \] As in Chapter 9, solutions require the problem to be noncharacteristic.

Definition/convention — noncharacteristic

FC08-C22-U056 · Ch. 22, § Nonlinear First-Order PDEs; source L17588 · not formalized

The Cauchy problem (22.23)–(22.24) is said to be noncharacteristic if there exists a smooth section $\sigma \in \Gamma ( T ^ { * } M | _ { S } )$ satisfying (22.25)–(22.26), with the additional property that if $\left( x ^ { i } \right)$ are any local coordinates on M and $\left( x ^ { 1 } , \ldots , x ^ { n } , \xi _ { 1 } , \ldots , \xi _ { n } \right)$ are the corresponding natural coordinates on $T ^ { * } M$ ; the following vector field along S is nowhere tangent to $S$ : \[ \left. A ^ {\sigma} \right| _ {x} = \frac {\partial F}{\partial \xi_ {1}} (x, \sigma (s)) \frac {\partial}{\partial x ^ {1}} + \dots + \frac {\partial F}{\partial \xi_ {n}} (x, \sigma (s)) \frac {\partial}{\partial x ^ {n}}.\tag{22.27} \]

Theorem 22.35

FC08-C22-U057 · Ch. 22, § Nonlinear First-Order PDEs; source L17596 · not formalized

Theorem 22.35 (The Cauchy Problem for a Hamilton–Jacobi Equation). Suppose M is a smooth manifold, $W \subseteq T ^ { * } M$ is an open subset, $F \colon W \to \mathbb { R }$ is $a$ smooth function, $S \subseteq M$ is an embedded hypersurface, and ’ $S \to \mathbb { R }$ is a smooth function. If the Cauchy problem (22.23)–(22.24) is noncharacteristic, then for each $p \in S$ there is a smooth solution defined on some neighborh linear map $\mathbb { H } { \to } \mathbb { H }$ given by $v \mapsto q v q ^ { * }$ takes E to itself and preserves the inner product $\langle v , w \rangle =$ $\scriptstyle { \frac { 1 } { 7 } } ( v ^ { * } w + w ^ { * } v )$ on $E$ (b) For each $q \in \mathcal S$ , let $\rho ( q )$ be the matrix representation of the map v $q v q ^ { * }$ with respect to the basis $( \mathring { \mathbb { I } } , \mathring { \mathbb { J } } , \mathbb { k } )$ for E.

Example 22.36

FC08-C22-U058 · Ch. 22, § Nonlinear First-Order PDEs; source L17636 · not formalized

(A Hamilton–Jacobi Equation). Consider the Cauchy problem \[ \frac{\partial u}{\partial x} - \left(\frac{\partial u}{\partial y}\right)^{2} = 0, \qquad u(0,y) = y^{2}. \] Writing $\sigma = d(y^{2}) + f(y)\,dx = 2y\,dy + f(y)\,dx$ and solving $F(0,y,f(y),2y) = f(y) - (2y)^{2} = 0$ gives $f(y) = 4y^{2}$, so $\sigma(y) = 2y\,dy + 4y^{2}\,dx$. The initial curve $S$ is parametrized by $X(s) = (0,s)$ and its lift $T \subseteq T^{*}\mathbb{R}^{2}$ by $\widetilde{X}(s) = (0,\ s,\ 4s^{2},\ 2s)$. Solving $(x,y) = (t,\ s-4st)$ for $(t,s)$ and substituting into the formulas for $(\xi,\eta)$ exhibits the flowout as the image of the closed 1-form \[ \alpha = \frac{4y^{2}}{(1-4x)^{2}}\,dx + \frac{2y}{1-4x}\,dy, \] and $\alpha = du$ on $\{(x,y) : x < 1/4\}$ with $u(x,y) = \dfrac{y^{2}}{1-4x}$, which already satisfies $u(0,y) = y^{2}$ and so solves the Cauchy problem.

Comparison/convention — higher-order jet bundles that give invariant representations

FC08-C22-U059 · Ch. 22, § General Nonlinear Equations; source L17682 · not formalized

Finally, we show how the preceding method can be adapted to solve arbitrary firstorder PDEs by using contact geometry in place of symplectic geometry. For this purpose, we introduce one last geometric construction. If M is a smooth manifold, the 1-jet bundle of M is the smooth vector bundle $J ^ { 1 } M = \mathbb { R } \times T ^ { * } M \to M$ ; whose fiber at $x \in M$ is $\mathbb { R } \times T _ { x } ^ { * } M$ . (It is the Whitney sum of a trivial R-bundle with $T ^ { * } M . )$ If u M R is a smooth function, the 1-jet of u is the section $j ^ { 1 } u \colon M \to$ $J ^ { 1 } M$ defined by $j ^ { 1 } u ( x ) = \bigl ( u ( x ) , d u ( x ) \bigr )$ . A point in the fiber of $J ^ { 1 } M$ over $x \in M$ can be viewed as a first-order Taylor polynomial at x of a smooth function on M; represented invariantly as the values of the function and its differential at x. (One can also define higher-order jet bundles that give invariant representations of higherorder Taylor polynomials. They are useful for studying higher-order PDEs, but we do not pursue them here.)

Definition/convention — Legendrian

FC08-C22-U060 · Ch. 22, § General Nonlinear Equations; source L17684 · after FC08-C22-U045, FC08-C22-U020 · not formalized

do not pursue them here.) The canonical contact form on $J ^ { 1 } M$ is the 1-form $\theta = d z - \tau$ defined in Example 22.27(b). A smooth (local or global) section $M J ^ { 1 } M$ is said to be Legendrian if its image is a Legendrian submanifold of $J ^ { 1 } M .$ ; or equivalently if $\eta ^ { * } \theta = 0$ . The next proposition is a contact analogue e dimension of $S ^ { \perp }$ is the codimension of S, as the next lemma shows.

Proposition 22.37

FC08-C22-U061 · Ch. 22, § General Nonlinear Equations; source L17686 · not formalized

proposition is a contact analogue of Proposition 22.12. Proposition 22.37. Let M be a smooth manifold. A smooth local section of J M is the 1-jet of a smooth function if and only if it is Legendrian. E

Comparison/convention — solution

FC08-C22-U062 · Ch. 22, § General Nonlinear Equations; source L17690 · not formalized

The 1-jet bundle provides the most general setting in which to consider firstorder partial differential equations. If M is a smooth manifold, a first-order PDE for a function u $M \to \mathbb { R }$ can be viewed as a real-valued function F on the 1-jet bundle of M; and a solution is a function whose 1-jet takes its values in the zero set of $F$.

Definition/convention — noncharacteristic

FC08-C22-U063 · Ch. 22, § General Nonlinear Equations; source L17702 · not formalized

\[ This problem is said to be noncharacteristic if there exists a smooth section $\sigma \in$ $\Gamma ( T ^ { * } M | _ { S } )$ taking its values in W and satisfying \] | _ {T _ {x} S} = d all } x S, \[ \] F (x, (x), for all } x S, \[ and such that the following vector field along S is nowhere tangent to S: \] . A ^ {} | _ {x} = (x), (x)) + + (x), (x)) \frac {}{ternating forces $\omega ( v , v ) = 0$ for every $v \in S$ , so $S \subseteq S ^ { \bot }$ .

Theorem 22.39

FC08-C22-U064 · Ch. 22, § General Nonlinear Equations; source L17720 · not formalized

Theorem 22.39 (The General First-Order Cauchy Problem). Suppose M is a smooth manifold, $W \subseteq J ^ { 1 } M$ is an open subset, $F \colon W \to \mathbb { R }$ is a smooth function, $S \subseteq M$ is an embedded hypersurface, and ’ $S \to \mathbb { R }$ is a smooth function. If the Cauchy problem (22.29)–(22.30) is noncharacteristic, then for each $p \in S$ there is a smooth solution on some neighborhood of $p$.