Symplecticity of Runge–Kutta methods

The algebraic theory of symplectic Runge–Kutta schemes (Sanz-Serna; Hairer–Lubich–Wanner VI.4, VI.7):

• RungeKutta.IsSymplectic — the tableau condition bᵢaᵢⱼ + bⱼaⱼᵢ = bᵢbⱼ;
• symplectic_defect — the Calvo–Sanz-Serna defect identity: for all rooted trees u, v, Φ(u ∘ v) + Φ(v ∘ u) − Φ(u)·Φ(v) = ∑ᵢⱼ (bᵢaᵢⱼ + bⱼaⱼᵢ − bᵢbⱼ)·Φᵢ(u)·Φⱼ(v) where u ∘ v is the Butcher product (grafting v onto the root of u) and Φᵢ are the stage weights;
• IsSymplectic.isSymplecticCharacter — a symplectic tableau therefore has a symplectic B-series: its elementary weights satisfy the pair condition a(u∘v) + a(v∘u) = a(u)·a(v) (IsSymplecticCharacter), which characterises symplectic B-series methods;
• the implicit midpoint rule is symplectic, the explicit Euler method is not.

The analytic statement — that the numerical flow of a symplectic method preserves the symplectic form for Hamiltonian systems — is outside the current scope; this file provides the complete tableau- and B-series-level theory.

def BSeries.RungeKutta.IsSymplectic {ι : Type u} {R : Type v} [Mul R] [Add R] (rk : RungeKutta ι R) : Prop

The symplecticity condition on a Runge–Kutta tableau: bᵢaᵢⱼ + bⱼaⱼᵢ = bᵢbⱼ for all stages i, j.

Equations

• rk.IsSymplectic = ∀ (i j : ι), rk.b i * rk.A i j + rk.b j * rk.A j i = rk.b i * rk.b j

def BSeries.RungeKutta.IsSymplecticCharacter {R : Type v} [Mul R] [Add R] (a : HopfAlgebras.RootedTree → R) : Prop

A coefficient system on rooted trees is a symplectic character when it satisfies the Calvo–Sanz-Serna pair condition a(u ∘ v) + a(v ∘ u) = a(u)·a(v) for the Butcher product.

Equations

• One or more equations did not get rendered due to their size.

theorem BSeries.RungeKutta.symplectic_defect {ι : Type u} {R : Type v} [Fintype ι] [CommRing R] (rk : RungeKutta ι R) (u v : HopfAlgebras.RootedTree) : rk.treeWeight ((HopfAlgebras.RootedForest.singleton v).butcherProduct u) + rk.treeWeight ((HopfAlgebras.RootedForest.singleton u).butcherProduct v) - rk.treeWeight u * rk.treeWeight v = ∑ i : ι, ∑ j : ι, (rk.b i * rk.A i j + rk.b j * rk.A j i - rk.b i * rk.b j) * (rk.treeStageWeight u i * rk.treeStageWeight v j)

The Calvo–Sanz-Serna defect identity: the failure of the elementary weights to be a symplectic character is the tableau defect bᵢaᵢⱼ + bⱼaⱼᵢ − bᵢbⱼ paired against the stage weights.

theorem BSeries.RungeKutta.IsSymplectic.isSymplecticCharacter {ι : Type u} {R : Type v} [Fintype ι] [CommRing R] {rk : RungeKutta ι R} (h : rk.IsSymplectic) : IsSymplecticCharacter rk.treeWeight

Symplectic tableaux have symplectic B-series: under the tableau condition, the elementary weights satisfy the pair condition Φ(u∘v) + Φ(v∘u) = Φ(u)·Φ(v).

Examples: the implicit midpoint rule is symplectic, the

explicit Euler method is not

theorem BSeries.RungeKutta.oneStage_half_isSymplectic : (oneStage ℚ (1 / 2)).IsSymplectic

The implicit midpoint rule oneStage ℚ (1/2) satisfies the symplecticity condition.

theorem BSeries.RungeKutta.oneStage_zero_not_isSymplectic : ¬(oneStage ℚ 0).IsSymplectic

The explicit Euler method oneStage ℚ 0 violates the symplecticity condition.