theorem ι_squared_zero_on_2forms {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X : VF) (α : Ω 2) : DifferentialFormSpace.ι X (DifferentialFormSpace.ι X α) = 0

For any vector field $X$ and 2-form $\alpha$, the double contraction vanishes: $\iota_X \iota_X \alpha = 0$.

theorem ι_ι_skew_2form {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (X Y : VF) (α : Ω 2) : DifferentialFormSpace.ι Y (DifferentialFormSpace.ι X α) = -DifferentialFormSpace.ι X (DifferentialFormSpace.ι Y α)

Skew-symmetry of iterated contractions on a 2-form: $\iota_Y \iota_X \alpha = -\iota_X \iota_Y \alpha$.

structure HamiltonianVectorField {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (H : Ω 0) : Type u_2

A Hamiltonian vector field for $H$ on a symplectic manifold $(M, \omega)$: a vector field $X$ satisfying the defining equation $\iota_X \omega = dH$.

• X : VF
• defining_eq : DifferentialFormSpace.ι self.X S.ω = DifferentialFormSpace.d VF H

class HasHamiltonianVF (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type (max u_1 u_2)

Symplectic manifolds in which every smooth function $H : M \to \mathbb{R}$ admits a Hamiltonian vector field $X_H$.

• hamiltonianVF (H : Ω 0) : HamiltonianVectorField S H

theorem lie_deriv_hamiltonian_eq_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (H : Ω 0) (hv : HamiltonianVectorField S H) : DifferentialFormSpace.L hv.X S.ω = 0

A Hamiltonian vector field preserves the symplectic form: $\mathcal{L}_{X_H} \omega = 0$. By Cartan's magic formula $\mathcal{L}_{X_H}\omega = \iota_{X_H} d\omega + d(\iota_{X_H}\omega) = 0 + d(dH) = 0$.

structure HamiltonianFlow {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (H : Ω 0) (hv : HamiltonianVectorField S H) : Type u_1

The flow (isotopy) $\rho_t$ generated by a Hamiltonian vector field $X_H$, encoded as a one-parameter family of pullback morphisms together with the defining ODE $\tfrac{d}{dt}(\rho_t^*\alpha) = \rho_t^*(\mathcal{L}_{X_H}\alpha)$, the initial condition $\rho_0 = \mathrm{id}$, the constancy principle for forms with zero derivative, and inverse relations $\rho_{-t} \circ \rho_t = \mathrm{id}$.

• ρ_t : ℝ → DFSMorphism Ω VF Ω VF
• ρ_zero {p : ℕ} (α : Ω p) : (self.ρ_t 0).pullback α = α
• pullback_deriv (t : ℝ) {p : ℕ} : Ω p → Ω p
• flow_ode (t : ℝ) {p : ℕ} (α : Ω p) : self.pullback_deriv t α = (self.ρ_t t).pullback (DifferentialFormSpace.L hv.X α)
• deriv_zero_const {p : ℕ} (α : Ω p) : (∀ (t : ℝ), self.pullback_deriv t α = 0) → ∀ (t : ℝ), (self.ρ_t t).pullback α = α
• flow_inv (t : ℝ) {p : ℕ} (α : Ω p) : (self.ρ_t (-t)).pullback ((self.ρ_t t).pullback α) = α
• flow_inv' (t : ℝ) {p : ℕ} (α : Ω p) : (self.ρ_t t).pullback ((self.ρ_t (-t)).pullback α) = α

theorem HamiltonianFlow.preserves_lie_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} {H : Ω 0} {hv : HamiltonianVectorField S H} (flow : HamiltonianFlow S H hv) (t : ℝ) {p : ℕ} (α : Ω p) (hL : DifferentialFormSpace.L hv.X α = 0) : (flow.ρ_t t).pullback α = α

General invariance principle: if $\mathcal{L}_{X_H}\alpha = 0$ then the Hamiltonian flow leaves $\alpha$ invariant: $\rho_t^* \alpha = \alpha$ for all $t$.

theorem HamiltonianFlow.preserves_symplectic_form {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} {H : Ω 0} {hv : HamiltonianVectorField S H} (flow : HamiltonianFlow S H hv) (t : ℝ) : (flow.ρ_t t).pullback S.ω = S.ω

Proposition 3 (method form): the Hamiltonian flow preserves the symplectic form, $\rho_t^* \omega = \omega$ for all $t$.

theorem hamiltonian_flow_preserves_symplectic_form {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (H : Ω 0) (hv : HamiltonianVectorField S H) (flow : HamiltonianFlow S H hv) (t : ℝ) : (flow.ρ_t t).pullback S.ω = S.ω

Proposition 3 (standalone form): for $H : M \to \mathbb{R}$ smooth with Hamiltonian vector field $X_H$, every time-$t$ map of the generated isotopy $\rho_t$ is a symplectomorphism: $\rho_t^* \omega = \omega$.

def HamiltonianFlow.toSymplectomorphism {Ω : ℕ → Type u_1} {VF : Type u_2} [DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} {H : Ω 0} {hv : HamiltonianVectorField S H} (flow : HamiltonianFlow S H hv) (t : ℝ) : Symplectomorphism S S

Promote a time-$t$ map of a Hamiltonian flow to a symplectomorphism of $(M, \omega)$, using $\rho_{-t}$ as the inverse.

def IsSymplecticVectorField {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (X : VF) : Prop

Definition 1 (symplectic part): a vector field $X$ is symplectic if $\mathcal{L}_X \omega = 0$, equivalently $\iota_X \omega$ is closed.

def IsHamiltonianVectorField {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (X : VF) : Prop

Definition 1 (Hamiltonian part): a vector field $X$ is Hamiltonian if $\iota_X \omega$ is exact, i.e. there exists $H \in C^\infty(M)$ with $\iota_X \omega = dH$.

theorem isSymplecticVF_iff_ιXω_closed {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (X : VF) : IsSymplecticVectorField S X ↔ DifferentialFormSpace.IsClosed' VF (DifferentialFormSpace.ι X S.ω)

Equivalent characterisation of symplectic vector fields: $X$ is symplectic iff $\iota_X \omega$ is a closed 1-form. This follows from Cartan's formula together with $d\omega = 0$.

theorem hamiltonianVF_isHamiltonianVF {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (H : Ω 0) (hv : HamiltonianVectorField S H) : IsHamiltonianVectorField S hv.X

The underlying vector field of any HamiltonianVectorField structure satisfies the predicate IsHamiltonianVectorField.

def poissonBracket {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) {F G : Ω 0} (hvF : HamiltonianVectorField S F) (hvG : HamiltonianVectorField S G) : Ω 0

The Poisson bracket $\{F, G\} := \omega(X_F, X_G) = \iota_{X_G}\iota_{X_F}\omega$ of two smooth functions $F, G$ with chosen Hamiltonian vector fields.

theorem poissonBracket_eq_neg_lie_deriv {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) {F G : Ω 0} (hvF : HamiltonianVectorField S F) (hvG : HamiltonianVectorField S G) : poissonBracket S hvF hvG = -DifferentialFormSpace.L hvF.X G

The Poisson bracket equals minus the Lie derivative of one Hamiltonian along the other: $\{F, G\} = -\mathcal{L}_{X_F} G$.

class HasLieBracket (Ω : ℕ → Type u_1) (VF : Type u_2) [inst : DifferentialFormSpace Ω VF] : Type u_2

Interface providing a Lie bracket $[X, Y]$ of vector fields characterised by the identity $\iota_{[X, Y]} \alpha = \mathcal{L}_X (\iota_Y \alpha) - \iota_Y (\mathcal{L}_X \alpha)$ for every form $\alpha$ of positive degree.

• bracket : VF → VF → VF
• bracket_ι_eq (X Y : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (bracket Ω X Y) α = DifferentialFormSpace.L X (DifferentialFormSpace.ι Y α) - DifferentialFormSpace.ι Y (DifferentialFormSpace.L X α)

theorem lie_bracket_ι_eq {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (X Y : VF) {p : ℕ} (α : Ω (p + 1)) : DifferentialFormSpace.ι (HasLieBracket.bracket Ω X Y) α = DifferentialFormSpace.L X (DifferentialFormSpace.ι Y α) - DifferentialFormSpace.ι Y (DifferentialFormSpace.L X α)

Restatement of the defining identity for the Lie bracket: $\iota_{[X, Y]} \alpha = \mathcal{L}_X (\iota_Y \alpha) - \iota_Y (\mathcal{L}_X \alpha)$.

theorem L_bracket_eq {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (X Y : VF) {p : ℕ} (α : Ω p) : DifferentialFormSpace.L (HasLieBracket.bracket Ω X Y) α = DifferentialFormSpace.L X (DifferentialFormSpace.L Y α) - DifferentialFormSpace.L Y (DifferentialFormSpace.L X α)

Compatibility of the Lie bracket with Lie derivatives on forms: $\mathcal{L}_{[X, Y]} \alpha = \mathcal{L}_X (\mathcal{L}_Y \alpha) - \mathcal{L}_Y (\mathcal{L}_X \alpha)$ for every form $\alpha$ of arbitrary degree.

theorem ι_one_form_nondegenerate {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (α : Ω 1) (h : ∀ (X : VF), DifferentialFormSpace.ι X α = 0) : α = 0

Non-degeneracy of contraction for 1-forms: if $\iota_X \alpha = 0$ for every vector field $X$, then $\alpha = 0$.

theorem lie_bracket_hamiltonian_eq {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] [hbr : HasLieBracket Ω VF] (S : SymplecticManifold Ω VF) {F G : Ω 0} (hvF : HamiltonianVectorField S F) (hvG : HamiltonianVectorField S G) : DifferentialFormSpace.ι (HasLieBracket.bracket Ω hvF.X hvG.X) S.ω = DifferentialFormSpace.d VF (DifferentialFormSpace.L hvF.X G)

For Hamiltonian vector fields $X_F$ and $X_G$, the bracket $[X_F, X_G]$ is itself Hamiltonian with Hamiltonian $\mathcal{L}_{X_F} G = \{F, G\}$ (up to sign): explicitly, $\iota_{[X_F, X_G]} \omega = d(\mathcal{L}_{X_F} G)$.

structure SymplecticIsotopy {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type (max u_1 u_2)

A symplectic isotopy of $(M, \omega)$: a one-parameter family $\varphi_t$ of pullback morphisms starting at the identity, generated by a time-dependent symplectic vector field $X_t$ (i.e. $\mathcal{L}_{X_t} \omega = 0$), and preserving $\omega$ at each time.

• φ_t : ℝ → DFSMorphism Ω VF Ω VF
• X_t : ℝ → VF
• symplectic (t : ℝ) : IsSymplecticVectorField S (self.X_t t)
• φ_zero {p : ℕ} (α : Ω p) : (self.φ_t 0).pullback α = α
• preserves_ω (t : ℝ) : (self.φ_t t).pullback S.ω = S.ω

structure TimeDependentHamiltonianFlow {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) : Type (max u_1 u_2)

The flow generated by a time-dependent Hamiltonian $H_t : M \to \mathbb{R}$ with chosen Hamiltonian vector fields $X_{H_t}$: the analogue of HamiltonianFlow with $H$ and $X_H$ allowed to vary smoothly in $t$.

• H_t : ℝ → Ω 0
• hv_t (t : ℝ) : HamiltonianVectorField S (self.H_t t)
• φ_t : ℝ → DFSMorphism Ω VF Ω VF
• φ_zero {p : ℕ} (α : Ω p) : (self.φ_t 0).pullback α = α
• pullback_deriv (t : ℝ) {p : ℕ} : Ω p → Ω p
• flow_ode (t : ℝ) {p : ℕ} (α : Ω p) : self.pullback_deriv t α = (self.φ_t t).pullback (DifferentialFormSpace.L (self.hv_t t).X α)
• deriv_zero_const {p : ℕ} (α : Ω p) : (∀ (t : ℝ), self.pullback_deriv t α = 0) → ∀ (t : ℝ), (self.φ_t t).pullback α = α

theorem TimeDependentHamiltonianFlow.preserves_lie_zero {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (flow : TimeDependentHamiltonianFlow S) (t : ℝ) {p : ℕ} (α : Ω p) (hL : ∀ (s : ℝ), DifferentialFormSpace.L (flow.hv_t s).X α = 0) : (flow.φ_t t).pullback α = α

General invariance principle for time-dependent Hamiltonian flows: if $\mathcal{L}_{X_{H_s}}\alpha = 0$ for all $s$, then $\varphi_t^*\alpha = \alpha$ for all $t$.

theorem TimeDependentHamiltonianFlow.preserves_symplectic_form {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (flow : TimeDependentHamiltonianFlow S) (t : ℝ) : (flow.φ_t t).pullback S.ω = S.ω

Time-dependent version of Proposition 3: a flow generated by a time-dependent Hamiltonian preserves the symplectic form, $\varphi_t^* \omega = \omega$.

def SymplecticIsotopy.ofHamiltonian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (flow : TimeDependentHamiltonianFlow S) : SymplecticIsotopy S

A time-dependent Hamiltonian flow is automatically a symplectic isotopy, with generating vector field $X_t := X_{H_t}$.

structure FluxData {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] (S : SymplecticManifold Ω VF) (iso : SymplecticIsotopy S) : Type u_1

Flux data of a symplectic isotopy $\varphi_t$: a closed 1-form $\sigma$ representing the class $[\iota_{X_t}\omega] \in H^1(M; \mathbb{R})$ uniformly in $t$, i.e. each $\sigma - \iota_{X_t}\omega$ is exact. The flux of $\varphi$ is the cohomology class $[\sigma]$.

• representative : Ω 1
• is_closed : DifferentialFormSpace.d VF self.representative = 0
• cohomologous_to_ιXω (t : ℝ) : DifferentialFormSpace.IsExact' VF (self.representative - DifferentialFormSpace.ι (iso.X_t t) S.ω)

def SymplecticIsotopy.IsHamiltonian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (iso : SymplecticIsotopy S) : Prop

A symplectic isotopy $\varphi_t$ is Hamiltonian if its generating vector field $X_t$ is a Hamiltonian vector field for every $t$.

theorem SymplecticIsotopy.ofHamiltonian_isHamiltonian {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {S : SymplecticManifold Ω VF} (flow : TimeDependentHamiltonianFlow S) : (ofHamiltonian flow).IsHamiltonian

The symplectic isotopy associated to a time-dependent Hamiltonian flow is Hamiltonian.

theorem exact_add {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α β : Ω (p + 1)) (hα : DifferentialFormSpace.IsExact' VF α) (hβ : DifferentialFormSpace.IsExact' VF β) : DifferentialFormSpace.IsExact' VF (α + β)

The sum of two exact forms is exact: $d a + d b = d(a + b)$.

theorem exact_neg {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α : Ω (p + 1)) (hα : DifferentialFormSpace.IsExact' VF α) : DifferentialFormSpace.IsExact' VF (-α)

The negation of an exact form is exact: if $\alpha = da$ then $-\alpha = d(-a)$.

theorem exact_sub {Ω : ℕ → Type u_1} {VF : Type u_2} [inst : DifferentialFormSpace Ω VF] {p : ℕ} (α β : Ω (p + 1)) (hα : DifferentialFormSpace.IsExact' VF α) (hβ : DifferentialFormSpace.IsExact' VF β) : DifferentialFormSpace.IsExact' VF (α - β)

The difference of two exact forms is exact.