Tableau constructions for the independence of elementary weights

The three constructions underlying Butcher's Theorem 317A (independence of the elementary weights / density of Runge–Kutta methods):

• dirSum — the block-diagonal tableau, whose elementary weights are the sums of the constituents' weights;
• smulScheme — scaling every coefficient by c, which scales the weight of a tree t by c^{|t|};
• extendScheme — appending a single quadrature stage whose row is bᵀ and moving all quadrature weight onto it, whose elementary weights are the products of the full weights of the children of the root.

(Butcher, Numerical Methods for ODEs, Section 317.)

def BSeries.RungeKutta.dirSum {ι : Type u} {κ : Type v} {R : Type w} [Zero R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) : RungeKutta (ι ⊕ κ) R

The block-diagonal sum of two tableaux.

Equations

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

def BSeries.RungeKutta.smulScheme {ι : Type u} {R : Type w} [Mul R] (c : R) (rk : RungeKutta ι R) : RungeKutta ι R

The tableau with every coefficient scaled by c.

Equations

• BSeries.RungeKutta.smulScheme c rk = { A := fun (i j : ι) => c * rk.A i j, b := fun (j : ι) => c * rk.b j }

def BSeries.RungeKutta.extendScheme {ι : Type u} {R : Type w} [Zero R] [One R] (rk : RungeKutta ι R) : RungeKutta (ι ⊕ PUnit.{u_1 + 1}) R

The tableau extended by one stage whose row is bᵀ, with all quadrature weight moved onto the new stage.

Equations

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

theorem BSeries.RungeKutta.stageWeight_dirSum_inl {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (t : HopfAlgebras.PTree) (i : ι) : (rk₁.dirSum rk₂).stageWeight t (Sum.inl i) = rk₁.stageWeight t i

theorem BSeries.RungeKutta.stageWeightList_dirSum_inl {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (ts : List HopfAlgebras.PTree) (i : ι) : (rk₁.dirSum rk₂).stageWeightList ts (Sum.inl i) = rk₁.stageWeightList ts i

theorem BSeries.RungeKutta.stageWeight_dirSum_inr {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (t : HopfAlgebras.PTree) (i : κ) : (rk₁.dirSum rk₂).stageWeight t (Sum.inr i) = rk₂.stageWeight t i

theorem BSeries.RungeKutta.stageWeightList_dirSum_inr {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (ts : List HopfAlgebras.PTree) (i : κ) : (rk₁.dirSum rk₂).stageWeightList ts (Sum.inr i) = rk₂.stageWeightList ts i

theorem BSeries.RungeKutta.weight_dirSum {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (t : HopfAlgebras.PTree) : (rk₁.dirSum rk₂).weight t = rk₁.weight t + rk₂.weight t

The elementary weights of a block-diagonal sum are the sums of the elementary weights (Butcher, Section 317, eq. (317a)).

theorem BSeries.RungeKutta.stageWeight_smulScheme {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) (i : ι) : (smulScheme c rk).stageWeight t i = c ^ (t.order - 1) * rk.stageWeight t i

theorem BSeries.RungeKutta.stageWeightList_smulScheme {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) (i : ι) : (smulScheme c rk).stageWeightList ts i = c ^ HopfAlgebras.PTree.orderList ts * rk.stageWeightList ts i

theorem BSeries.RungeKutta.weight_smulScheme {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) : (smulScheme c rk).weight t = c ^ t.order * rk.weight t

Scaling the tableau scales the weight of t by c^{|t|} (Butcher, Section 317).

theorem BSeries.RungeKutta.stageWeight_extendScheme_inl {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) (i : ι) : rk.extendScheme.stageWeight t (Sum.inl i) = rk.stageWeight t i

theorem BSeries.RungeKutta.stageWeightList_extendScheme_inl {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) (i : ι) : rk.extendScheme.stageWeightList ts (Sum.inl i) = rk.stageWeightList ts i

theorem BSeries.RungeKutta.stageWeightList_extendScheme_inr {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) (u : PUnit.{u_1 + 1}) : rk.extendScheme.stageWeightList ts (Sum.inr u) = (List.map (fun (t : HopfAlgebras.PTree) => rk.weight t) ts).prod

The added stage of extendScheme evaluates the product of the full weights of a forest.

theorem BSeries.RungeKutta.weight_extendScheme {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) : rk.extendScheme.weight (HopfAlgebras.PTree.node ts) = (List.map (fun (t : HopfAlgebras.PTree) => rk.weight t) ts).prod

The extended scheme's elementary weight is the product of the full weights of the root's children (Butcher, Section 317: the one-stage extension realizing Φ'(t) = Π_j Φ(t_j)).

def BSeries.RungeKutta.zeroScheme (R : Type w) [Zero R] : RungeKutta PUnit.{u_1 + 1} R

The scheme with all coefficients zero.

Equations

• BSeries.RungeKutta.zeroScheme R = { A := fun (x x_1 : PUnit.{?u.1 + 1}) => 0, b := fun (x : PUnit.{?u.1 + 1}) => 0 }

theorem BSeries.RungeKutta.treeWeight_zeroScheme {R : Type w} [CommSemiring R] (τ : HopfAlgebras.RootedTree) : (zeroScheme R).treeWeight τ = 0

def BSeries.RungeKutta.scaleWeights {ι : Type u} {R : Type w} [Mul R] (c : R) (rk : RungeKutta ι R) : RungeKutta ι R

Scaling only the quadrature weights b. Since b enters each elementary weight exactly once, this scales all weights linearly.

Equations

• BSeries.RungeKutta.scaleWeights c rk = { A := rk.A, b := fun (j : ι) => c * rk.b j }

theorem BSeries.RungeKutta.stageWeight_scaleWeights {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) (i : ι) : (scaleWeights c rk).stageWeight t i = rk.stageWeight t i

theorem BSeries.RungeKutta.stageWeightList_scaleWeights {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) (i : ι) : (scaleWeights c rk).stageWeightList ts i = rk.stageWeightList ts i

theorem BSeries.RungeKutta.weight_scaleWeights {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) : (scaleWeights c rk).weight t = c * rk.weight t

theorem BSeries.RungeKutta.treeWeight_scaleWeights {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : (scaleWeights c rk).treeWeight τ = c * rk.treeWeight τ

theorem BSeries.RungeKutta.treeWeight_dirSum {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (τ : HopfAlgebras.RootedTree) : (rk₁.dirSum rk₂).treeWeight τ = rk₁.treeWeight τ + rk₂.treeWeight τ

theorem BSeries.RungeKutta.treeWeight_smulScheme {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (c : R) (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : (smulScheme c rk).treeWeight τ = c ^ τ.order * rk.treeWeight τ

theorem BSeries.RungeKutta.treeWeight_extendScheme {ι : Type u} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : rk.extendScheme.treeWeight τ = rk.forestWeight τ.branches

The extended scheme evaluates the product of the children's full weights: Φ'(τ) = forestWeight(branches τ) (Butcher, Section 317).

def BSeries.RungeKutta.AchievableWeights {R : Type w} [CommSemiring R] (T₀ : Finset HopfAlgebras.RootedTree) (w : ↥T₀ → R) : Prop

A vector of prescribed elementary weights on a finite set of trees is achievable if some Runge–Kutta method realizes it.

Equations

• BSeries.RungeKutta.AchievableWeights T₀ w = ∃ (ι : Type) (x : Fintype ι) (rk : BSeries.RungeKutta ι R), ∀ (t : ↥T₀), rk.treeWeight ↑t = w t

theorem BSeries.RungeKutta.achievableWeights_zero {R : Type w} [CommSemiring R] (T₀ : Finset HopfAlgebras.RootedTree) : AchievableWeights T₀ 0

theorem BSeries.RungeKutta.AchievableWeights.add {R : Type w} [CommSemiring R] {T₀ : Finset HopfAlgebras.RootedTree} {w₁ w₂ : ↥T₀ → R} (h₁ : AchievableWeights T₀ w₁) (h₂ : AchievableWeights T₀ w₂) : AchievableWeights T₀ (w₁ + w₂)

theorem BSeries.RungeKutta.AchievableWeights.smul {R : Type w} [CommSemiring R] {T₀ : Finset HopfAlgebras.RootedTree} {w : ↥T₀ → R} (c : R) (h : AchievableWeights T₀ w) : AchievableWeights T₀ (c • w)

theorem BSeries.RungeKutta.AchievableWeights.graded {R : Type w} [CommSemiring R] {T₀ : Finset HopfAlgebras.RootedTree} {w : ↥T₀ → R} (c : R) (h : AchievableWeights T₀ w) : AchievableWeights T₀ fun (t : ↥T₀) => c ^ (↑t).order * w t

The graded scaling: c^{|t|}-weighted vectors are achievable.

def BSeries.RungeKutta.achievableSubmodule (R : Type w) [CommSemiring R] (T₀ : Finset HopfAlgebras.RootedTree) : Submodule R (↥T₀ → R)

The achievable weight vectors form a submodule (Butcher, Section 317: "the set of possible values ... is a vector space").

Equations

• BSeries.RungeKutta.achievableSubmodule R T₀ = { carrier := {w : ↥T₀ → R | BSeries.RungeKutta.AchievableWeights T₀ w}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem BSeries.RungeKutta.annihilator_graded {R : Type w} [Field R] [Infinite R] {T₀ : Finset HopfAlgebras.RootedTree} (ξ : ↥T₀ → R) (h : ∀ (w : ↥T₀ → R), AchievableWeights T₀ w → ∑ t : ↥T₀, ξ t * w t = 0) (d : ℕ) {w : ↥T₀ → R} (hw : AchievableWeights T₀ w) : ∑ t : ↥T₀ with (↑t).order = d, ξ t * w t = 0

Graded annihilation: a linear relation among the elementary weights valid for all Runge–Kutta methods splits into relations among trees of equal order (Butcher, Section 317, via the scaling c^{|t|} and a polynomial identity).

theorem BSeries.RungeKutta.exists_rk_treeWeight {R : Type w} [Field R] [Infinite R] (n : ℕ) (T₀ : Finset HopfAlgebras.RootedTree) : T₀.sup HopfAlgebras.RootedTree.order ≤ n → ∀ (β : HopfAlgebras.RootedTree → R), AchievableWeights T₀ fun (t : ↥T₀) => β ↑t

Butcher's Theorem 317A (independence of the elementary weights / density of Runge–Kutta methods): for any finite set of trees T₀ and any prescription β of values, there is a Runge–Kutta method whose elementary weights realize β on T₀ (Butcher, Numerical Methods for ODEs, Theorem 317A).

theorem BSeries.RungeKutta.exists_rk_forall_treeWeight {R : Type w} [Field R] [Infinite R] (T₀ : Finset HopfAlgebras.RootedTree) (β : HopfAlgebras.RootedTree → R) : ∃ (ι : Type) (x : Fintype ι) (rk : RungeKutta ι R), ∀ t ∈ T₀, rk.treeWeight t = β t

Butcher's Theorem 317A, packaged: any finite prescription of elementary weights is realized by some Runge–Kutta method.