Runge-Kutta Elementary Weights

This file defines Runge-Kutta tableaux and their elementary weights on rooted trees. The recursive stage weights are first defined for planar trees, then shown invariant under child permutations so that they descend to non-planar rooted trees.

Main definitions

• RungeKutta - a Butcher tableau without a fixed stage ordering
• RungeKutta.stageWeight - recursive stage weight of a planar tree
• RungeKutta.weight - elementary weight of a planar tree
• RungeKutta.series - the B-series coefficient family induced by a tableau

References

• John C. Butcher, Introduction to Runge-Kutta methods
• John C. Butcher, Numerical Methods for Ordinary Differential Equations

structure BSeries.RungeKutta (ι : Type u) (R : Type v) : Type (max u v)

A Runge-Kutta tableau with stage type ι and coefficients in R.

• A : ι → ι → R
• b : ι → R

def BSeries.RungeKutta.oneStage (R : Type v) [One R] (a : R) : RungeKutta PUnit.{u_1 + 1} R

A one-stage Runge-Kutta tableau with stage matrix entry a and weight 1.

Equations

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

def BSeries.RungeKutta.explicitEuler (R : Type v) [Zero R] [One R] : RungeKutta PUnit.{u_1 + 1} R

Forward Euler as a one-stage Runge-Kutta tableau.

Equations

• BSeries.RungeKutta.explicitEuler R = BSeries.RungeKutta.oneStage R 0

def BSeries.RungeKutta.implicitEuler (R : Type v) [One R] : RungeKutta PUnit.{u_1 + 1} R

Backward Euler as a one-stage Runge-Kutta tableau.

Equations

• BSeries.RungeKutta.implicitEuler R = BSeries.RungeKutta.oneStage R 1

def BSeries.RungeKutta.twoStageExplicit (R : Type v) [Zero R] (a21 b1 b2 : R) : RungeKutta (Fin 2) R

A two-stage explicit Runge-Kutta tableau.

Equations

• BSeries.RungeKutta.twoStageExplicit R a21 b1 b2 = { A := fun (i j : Fin 2) => ![![0, 0], ![a21, 0]] i j, b := fun (i : Fin 2) => ![b1, b2] i }

def BSeries.RungeKutta.threeStageExplicit (R : Type v) [Zero R] (a21 a31 a32 b1 b2 b3 : R) : RungeKutta (Fin 3) R

A three-stage explicit Runge-Kutta tableau.

Equations

• BSeries.RungeKutta.threeStageExplicit R a21 a31 a32 b1 b2 b3 = { A := fun (i j : Fin 3) => ![![0, 0, 0], ![a21, 0, 0], ![a31, a32, 0]] i j, b := fun (i : Fin 3) => ![b1, b2, b3] i }

@[simp]

theorem BSeries.RungeKutta.oneStage_A {R : Type v} [One R] (a : R) (i j : PUnit.{u_1 + 1}) : (oneStage R a).A i j = a

@[simp]

theorem BSeries.RungeKutta.oneStage_b {R : Type v} [One R] (a : R) (i : PUnit.{u_1 + 1}) : (oneStage R a).b i = 1

def BSeries.RungeKutta.abscissa {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : R

Row sum cᵢ = ∑ⱼ aᵢⱼ of the tableau.

Equations

• rk.abscissa i = ∑ j : ι, rk.A i j

@[simp]

theorem BSeries.RungeKutta.oneStage_abscissa {R : Type v} [CommSemiring R] (a : R) (i : PUnit.{u_1 + 1}) : (oneStage R a).abscissa i = a

@[simp]

theorem BSeries.RungeKutta.explicitEuler_abscissa {R : Type v} [CommSemiring R] (i : PUnit.{u_1 + 1}) : (explicitEuler R).abscissa i = 0

@[simp]

theorem BSeries.RungeKutta.implicitEuler_abscissa {R : Type v} [CommSemiring R] (i : PUnit.{u_1 + 1}) : (implicitEuler R).abscissa i = 1

@[simp]

theorem BSeries.RungeKutta.twoStageExplicit_abscissa_zero {R : Type v} [CommSemiring R] (a21 b1 b2 : R) : (twoStageExplicit R a21 b1 b2).abscissa 0 = 0

@[simp]

theorem BSeries.RungeKutta.twoStageExplicit_abscissa_one {R : Type v} [CommSemiring R] (a21 b1 b2 : R) : (twoStageExplicit R a21 b1 b2).abscissa 1 = a21

@[simp]

theorem BSeries.RungeKutta.threeStageExplicit_abscissa_zero {R : Type v} [CommSemiring R] (a21 a31 a32 b1 b2 b3 : R) : (threeStageExplicit R a21 a31 a32 b1 b2 b3).abscissa 0 = 0

@[simp]

theorem BSeries.RungeKutta.threeStageExplicit_abscissa_one {R : Type v} [CommSemiring R] (a21 a31 a32 b1 b2 b3 : R) : (threeStageExplicit R a21 a31 a32 b1 b2 b3).abscissa 1 = a21

@[simp]

theorem BSeries.RungeKutta.threeStageExplicit_abscissa_two {R : Type v} [CommSemiring R] (a21 a31 a32 b1 b2 b3 : R) : (threeStageExplicit R a21 a31 a32 b1 b2 b3).abscissa 2 = a31 + a32

def BSeries.RungeKutta.stageWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : HopfAlgebras.PTree → ι → R

Recursive stage weight of a planar tree.

Equations

• rk.stageWeight (HopfAlgebras.PTree.node ts) x✝ = rk.stageWeightList ts x✝

def BSeries.RungeKutta.stageWeightList {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : List HopfAlgebras.PTree → ι → R

Product of child contributions in the recursive stage weight.

Equations

• rk.stageWeightList [] x✝ = 1
• rk.stageWeightList (t :: ts) x✝ = (∑ j : ι, rk.A x✝ j * rk.stageWeight t j) * rk.stageWeightList ts x✝

@[simp]

theorem BSeries.RungeKutta.stageWeight_node {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) (i : ι) : rk.stageWeight (HopfAlgebras.PTree.node ts) i = rk.stageWeightList ts i

@[simp]

theorem BSeries.RungeKutta.stageWeightList_nil {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.stageWeightList [] i = 1

@[simp]

theorem BSeries.RungeKutta.stageWeightList_cons {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) (ts : List HopfAlgebras.PTree) (i : ι) : rk.stageWeightList (t :: ts) i = (∑ j : ι, rk.A i j * rk.stageWeight t j) * rk.stageWeightList ts i

@[simp]

theorem BSeries.RungeKutta.stageWeight_bullet {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.stageWeight HopfAlgebras.PTree.bullet i = 1

@[simp]

theorem BSeries.RungeKutta.stageWeight_chain2 {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.stageWeight HopfAlgebras.PTree.chain2 i = rk.abscissa i

@[simp]

theorem BSeries.RungeKutta.stageWeight_chain3 {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.stageWeight HopfAlgebras.PTree.chain3 i = ∑ j : ι, rk.A i j * rk.abscissa j

@[simp]

theorem BSeries.RungeKutta.stageWeight_cherry {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.stageWeight HopfAlgebras.PTree.cherry i = rk.abscissa i * rk.abscissa i

def BSeries.RungeKutta.weight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) : R

Elementary weight of a planar rooted tree.

Equations

• rk.weight t = ∑ i : ι, rk.b i * rk.stageWeight t i

def BSeries.RungeKutta.weightBullet {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : R

Elementary weight of the one-node tree.

Equations

• rk.weightBullet = ∑ i : ι, rk.b i

@[simp]

theorem BSeries.RungeKutta.weight_bullet {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.weight HopfAlgebras.PTree.bullet = rk.weightBullet

@[simp]

theorem BSeries.RungeKutta.oneStage_weightBullet {R : Type v} [CommSemiring R] (a : R) : (oneStage R a).weightBullet = 1

@[simp]

theorem BSeries.RungeKutta.explicitEuler_weightBullet {R : Type v} [CommSemiring R] : (explicitEuler R).weightBullet = 1

@[simp]

theorem BSeries.RungeKutta.implicitEuler_weightBullet {R : Type v} [CommSemiring R] : (implicitEuler R).weightBullet = 1

@[simp]

theorem BSeries.RungeKutta.oneStage_stageWeight {R : Type v} [CommSemiring R] (a : R) (t : HopfAlgebras.PTree) (i : PUnit.{u_1 + 1}) : (oneStage R a).stageWeight t i = a ^ (t.order - 1)

@[simp]

theorem BSeries.RungeKutta.oneStage_stageWeightList {R : Type v} [CommSemiring R] (a : R) (ts : List HopfAlgebras.PTree) (i : PUnit.{u_1 + 1}) : (oneStage R a).stageWeightList ts i = a ^ HopfAlgebras.PTree.orderList ts

@[simp]

theorem BSeries.RungeKutta.oneStage_weight {R : Type v} [CommSemiring R] (a : R) (t : HopfAlgebras.PTree) : (oneStage R a).weight t = a ^ (t.order - 1)

@[simp]

theorem BSeries.RungeKutta.oneStage_weight_chain2 {R : Type v} [CommSemiring R] (a : R) : (oneStage R a).weight HopfAlgebras.PTree.chain2 = a

@[simp]

theorem BSeries.RungeKutta.weight_chain3 {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.weight HopfAlgebras.PTree.chain3 = ∑ i : ι, rk.b i * ∑ j : ι, rk.A i j * rk.abscissa j

@[simp]

theorem BSeries.RungeKutta.weight_cherry {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.weight HopfAlgebras.PTree.cherry = ∑ i : ι, rk.b i * (rk.abscissa i * rk.abscissa i)

@[simp]

theorem BSeries.RungeKutta.twoStageExplicit_weightBullet {R : Type v} [CommSemiring R] (a21 b1 b2 : R) : (twoStageExplicit R a21 b1 b2).weightBullet = b1 + b2

@[simp]

theorem BSeries.RungeKutta.twoStageExplicit_weight_chain2 {R : Type v} [CommSemiring R] (a21 b1 b2 : R) : (twoStageExplicit R a21 b1 b2).weight HopfAlgebras.PTree.chain2 = b2 * a21

@[simp]

theorem BSeries.RungeKutta.threeStageExplicit_weightBullet {R : Type v} [CommSemiring R] (a21 a31 a32 b1 b2 b3 : R) : (threeStageExplicit R a21 a31 a32 b1 b2 b3).weightBullet = b1 + b2 + b3

@[simp]

theorem BSeries.RungeKutta.threeStageExplicit_weight_chain2 {R : Type v} [CommSemiring R] (a21 a31 a32 b1 b2 b3 : R) : (threeStageExplicit R a21 a31 a32 b1 b2 b3).weight HopfAlgebras.PTree.chain2 = b2 * a21 + b3 * (a31 + a32)

@[simp]

theorem BSeries.RungeKutta.threeStageExplicit_weight_chain3 {R : Type v} [CommSemiring R] (a21 a31 a32 b1 b2 b3 : R) : (threeStageExplicit R a21 a31 a32 b1 b2 b3).weight HopfAlgebras.PTree.chain3 = b3 * (a32 * a21)

@[simp]

theorem BSeries.RungeKutta.threeStageExplicit_weight_cherry {R : Type v} [CommSemiring R] (a21 a31 a32 b1 b2 b3 : R) : (threeStageExplicit R a21 a31 a32 b1 b2 b3).weight HopfAlgebras.PTree.cherry = b2 * (a21 * a21) + b3 * ((a31 + a32) * (a31 + a32))

def BSeries.RungeKutta.weightList {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) : R

Multiplicative elementary weight of a planar rooted forest.

Equations

• rk.weightList ts = (List.map rk.weight ts).prod

@[simp]

theorem BSeries.RungeKutta.weightList_nil {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.weightList [] = 1

@[simp]

theorem BSeries.RungeKutta.weightList_cons {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) (ts : List HopfAlgebras.PTree) : rk.weightList (t :: ts) = rk.weight t * rk.weightList ts

@[simp]

theorem BSeries.RungeKutta.weightList_append {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts us : List HopfAlgebras.PTree) : rk.weightList (ts ++ us) = rk.weightList ts * rk.weightList us

theorem BSeries.RungeKutta.weightList_perm {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) {ts us : List HopfAlgebras.PTree} (h : ts.Perm us) : rk.weightList ts = rk.weightList us

theorem BSeries.RungeKutta.stageWeightList_perm {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) {ts us : List HopfAlgebras.PTree} (h : ts.Perm us) : rk.stageWeightList ts i = rk.stageWeightList us i

@[simp]

theorem BSeries.RungeKutta.stageWeightList_append {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts us : List HopfAlgebras.PTree) (i : ι) : rk.stageWeightList (ts ++ us) i = rk.stageWeightList ts i * rk.stageWeightList us i

theorem BSeries.RungeKutta.stageWeight_perm {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) {t u : HopfAlgebras.PTree} : t.Perm u → rk.stageWeight t i = rk.stageWeight u i

Stage weights are invariant under the non-planar tree relation.

theorem BSeries.RungeKutta.stageWeightList_eq_of_forall₂ {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) {ts us : List HopfAlgebras.PTree} : List.Forall₂ HopfAlgebras.PTree.Perm ts us → rk.stageWeightList ts i = rk.stageWeightList us i

Stage-weight products are invariant under elementwise equivalent child lists.

theorem BSeries.RungeKutta.weight_perm {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) {t u : HopfAlgebras.PTree} : t.Perm u → rk.weight t = rk.weight u

Elementary weights are invariant under the non-planar tree relation.

def BSeries.RungeKutta.treeStageWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) (i : ι) : R

Recursive stage weight of a non-planar rooted tree.

Equations

• rk.treeStageWeight τ i = Quotient.lift (fun (t : HopfAlgebras.PTree) => rk.stageWeight t i) ⋯ τ

@[simp]

theorem BSeries.RungeKutta.treeStageWeight_ofPTree {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) (i : ι) : rk.treeStageWeight (HopfAlgebras.RootedTree.ofPTree t) i = rk.stageWeight t i

@[simp]

theorem BSeries.RungeKutta.treeStageWeight_bullet {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.treeStageWeight HopfAlgebras.RootedTree.bullet i = 1

def BSeries.RungeKutta.forestStageWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) (i : ι) : R

Product of child stage contributions over a non-planar rooted forest.

Equations

• rk.forestStageWeight φ i = (Multiset.map (fun (τ : HopfAlgebras.RootedTree) => ∑ j : ι, rk.A i j * rk.treeStageWeight τ j) φ).prod

@[simp]

theorem BSeries.RungeKutta.forestStageWeight_zero {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.forestStageWeight 0 i = 1

@[simp]

theorem BSeries.RungeKutta.forestStageWeight_empty {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (i : ι) : rk.forestStageWeight HopfAlgebras.RootedForest.empty i = 1

@[simp]

theorem BSeries.RungeKutta.forestStageWeight_singleton {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) (i : ι) : rk.forestStageWeight (HopfAlgebras.RootedForest.singleton τ) i = ∑ j : ι, rk.A i j * rk.treeStageWeight τ j

@[simp]

theorem BSeries.RungeKutta.forestStageWeight_add {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ ψ : HopfAlgebras.RootedForest) (i : ι) : rk.forestStageWeight (φ + ψ) i = rk.forestStageWeight φ i * rk.forestStageWeight ψ i

theorem BSeries.RungeKutta.forestStageWeight_ofPTree_list {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) (i : ι) : rk.forestStageWeight (↑(List.map HopfAlgebras.RootedTree.ofPTree ts)) i = rk.stageWeightList ts i

@[simp]

theorem BSeries.RungeKutta.treeStageWeight_graft {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) (i : ι) : rk.treeStageWeight φ.graft i = rk.forestStageWeight φ i

@[simp]

theorem BSeries.RungeKutta.treeStageWeight_branches {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) (i : ι) : rk.treeStageWeight τ i = rk.forestStageWeight τ.branches i

@[simp]

theorem BSeries.RungeKutta.treeStageWeight_butcherProduct {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree) (i : ι) : rk.treeStageWeight (φ.butcherProduct τ) i = rk.forestStageWeight φ i * rk.treeStageWeight τ i

def BSeries.RungeKutta.treeWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : HopfAlgebras.RootedTree → R

Elementary weight of a non-planar rooted tree.

Equations

• rk.treeWeight = Quotient.lift rk.weight ⋯

@[simp]

theorem BSeries.RungeKutta.treeWeight_ofPTree {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PTree) : rk.treeWeight (HopfAlgebras.RootedTree.ofPTree t) = rk.weight t

@[simp]

theorem BSeries.RungeKutta.oneStage_treeWeight {R : Type v} [CommSemiring R] (a : R) (τ : HopfAlgebras.RootedTree) : (oneStage R a).treeWeight τ = a ^ (τ.order - 1)

theorem BSeries.RungeKutta.treeWeight_eq_sum_treeStageWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : rk.treeWeight τ = ∑ i : ι, rk.b i * rk.treeStageWeight τ i

theorem BSeries.RungeKutta.treeWeight_graft {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) : rk.treeWeight φ.graft = ∑ i : ι, rk.b i * rk.forestStageWeight φ i

theorem BSeries.RungeKutta.treeWeight_branches {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : rk.treeWeight τ = ∑ i : ι, rk.b i * rk.forestStageWeight τ.branches i

theorem BSeries.RungeKutta.treeWeight_butcherProduct {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree) : rk.treeWeight (φ.butcherProduct τ) = ∑ i : ι, rk.b i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i)

@[simp]

theorem BSeries.RungeKutta.treeWeight_bullet {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.treeWeight HopfAlgebras.RootedTree.bullet = rk.weightBullet

def BSeries.RungeKutta.forestWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) : R

Multiplicative elementary weight of a non-planar rooted forest.

Equations

• rk.forestWeight φ = (Multiset.map rk.treeWeight φ).prod

@[simp]

theorem BSeries.RungeKutta.forestWeight_zero {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.forestWeight 0 = 1

@[simp]

theorem BSeries.RungeKutta.forestWeight_empty {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.forestWeight HopfAlgebras.RootedForest.empty = 1

@[simp]

theorem BSeries.RungeKutta.forestWeight_singleton {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : rk.forestWeight (HopfAlgebras.RootedForest.singleton τ) = rk.treeWeight τ

@[simp]

theorem BSeries.RungeKutta.forestWeight_add {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ ψ : HopfAlgebras.RootedForest) : rk.forestWeight (φ + ψ) = rk.forestWeight φ * rk.forestWeight ψ

@[simp]

theorem BSeries.RungeKutta.forestWeight_ofPTree_list {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List HopfAlgebras.PTree) : rk.forestWeight ↑(List.map HopfAlgebras.RootedTree.ofPTree ts) = rk.weightList ts

def BSeries.RungeKutta.series {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : Series R

B-series coefficient family induced by a Runge-Kutta tableau.

Equations

• rk.series HopfAlgebras.TreeIndex.empty = 1
• rk.series (HopfAlgebras.TreeIndex.tree τ) = rk.treeWeight τ

@[simp]

theorem BSeries.RungeKutta.series_apply_empty {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.series HopfAlgebras.TreeIndex.empty = 1

@[simp]

theorem BSeries.RungeKutta.series_apply_tree {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : rk.series (HopfAlgebras.TreeIndex.tree τ) = rk.treeWeight τ

@[simp]

theorem BSeries.RungeKutta.oneStage_series_apply_tree {R : Type v} [CommSemiring R] (a : R) (τ : HopfAlgebras.RootedTree) : (oneStage R a).series (HopfAlgebras.TreeIndex.tree τ) = a ^ (τ.order - 1)

@[simp]

theorem BSeries.RungeKutta.series_apply_bullet {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.series HopfAlgebras.TreeIndex.bullet = rk.weightBullet

@[simp]

theorem BSeries.RungeKutta.series_empty {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.series.coeff HopfAlgebras.TreeIndex.empty = 1

@[simp]

theorem BSeries.RungeKutta.series_bullet {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.series.coeff HopfAlgebras.TreeIndex.bullet = rk.weightBullet

theorem BSeries.RungeKutta.series_butcherProduct {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree) : rk.series.coeff (HopfAlgebras.TreeIndex.tree (φ.butcherProduct τ)) = ∑ i : ι, rk.b i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i)

theorem BSeries.RungeKutta.series_graft {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) : rk.series.coeff (HopfAlgebras.TreeIndex.tree φ.graft) = ∑ i : ι, rk.b i * rk.forestStageWeight φ i

theorem BSeries.RungeKutta.series_branches {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.RootedTree) : rk.series.coeff (HopfAlgebras.TreeIndex.tree τ) = ∑ i : ι, rk.b i * rk.forestStageWeight τ.branches i

@[simp]

theorem BSeries.RungeKutta.forestCoeff_series {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) : rk.series.forestCoeff φ = rk.forestWeight φ

@[simp]

theorem BSeries.RungeKutta.toCharacter_series_evalForest {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) : rk.series.toCharacter.evalForest φ = rk.forestWeight φ

@[simp]

theorem BSeries.RungeKutta.toCharacter_series_ofForest {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.RootedForest) : rk.series.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = rk.forestWeight φ

theorem BSeries.RungeKutta.series_hasUnitConstant {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : rk.series.HasUnitConstant

def BSeries.RungeKutta.AgreeUpToOrder {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : Prop

Two Runge-Kutta tableaux have matching B-series coefficients through order n.

Equations

• rk.AgreeUpToOrder rk' n = rk.series.AgreeUpToOrder rk'.series n

theorem BSeries.RungeKutta.agreeUpToOrder_refl {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (n : ℕ) : rk.AgreeUpToOrder rk n

theorem BSeries.RungeKutta.AgreeUpToOrder.symm {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) : rk'.AgreeUpToOrder rk n

theorem BSeries.RungeKutta.AgreeUpToOrder.trans {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ η : Type u} [Fintype κ] [Fintype η] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {rk'' : RungeKutta η R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) (h' : rk'.AgreeUpToOrder rk'' n) : rk.AgreeUpToOrder rk'' n

theorem BSeries.RungeKutta.AgreeUpToOrder.mono {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {m n : ℕ} (h : rk.AgreeUpToOrder rk' n) (hmn : m ≤ n) : rk.AgreeUpToOrder rk' m

theorem BSeries.RungeKutta.agreeUpToOrder_iff_treeWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : rk.AgreeUpToOrder rk' n ↔ ∀ (τ : HopfAlgebras.RootedTree), τ.order ≤ n → rk.treeWeight τ = rk'.treeWeight τ

theorem BSeries.RungeKutta.agreeUpToOrder_iff_weight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : rk.AgreeUpToOrder rk' n ↔ ∀ (t : HopfAlgebras.PTree), t.order ≤ n → rk.weight t = rk'.weight t

theorem BSeries.RungeKutta.agreeUpToOrder_iff_forestCoeff {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : rk.AgreeUpToOrder rk' n ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → rk.series.forestCoeff φ = rk'.series.forestCoeff φ

theorem BSeries.RungeKutta.agreeUpToOrder_iff_forestWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : rk.AgreeUpToOrder rk' n ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → rk.forestWeight φ = rk'.forestWeight φ

theorem BSeries.RungeKutta.agreeUpToOrder_iff_toCharacter_evalForest {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : rk.AgreeUpToOrder rk' n ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → rk.series.toCharacter.evalForest φ = rk'.series.toCharacter.evalForest φ

theorem BSeries.RungeKutta.AgreeUpToOrder.treeWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) {τ : HopfAlgebras.RootedTree} (hτ : τ.order ≤ n) : rk.treeWeight τ = rk'.treeWeight τ

theorem BSeries.RungeKutta.AgreeUpToOrder.weight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) {t : HopfAlgebras.PTree} (ht : t.order ≤ n) : rk.weight t = rk'.weight t

theorem BSeries.RungeKutta.AgreeUpToOrder.forestWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : rk.forestWeight φ = rk'.forestWeight φ

theorem BSeries.RungeKutta.AgreeUpToOrder.toCharacter_evalForest {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : rk.series.toCharacter.evalForest φ = rk'.series.toCharacter.evalForest φ

theorem BSeries.RungeKutta.agreeUpToOrder_succ_iff_treeWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : rk.AgreeUpToOrder rk' (n + 1) ↔ rk.AgreeUpToOrder rk' n ∧ ∀ (τ : HopfAlgebras.RootedTree), τ.order = n + 1 → rk.treeWeight τ = rk'.treeWeight τ

theorem BSeries.RungeKutta.agreeUpToOrder_succ_iff_weight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) : rk.AgreeUpToOrder rk' (n + 1) ↔ rk.AgreeUpToOrder rk' n ∧ ∀ (t : HopfAlgebras.PTree), t.order = n + 1 → rk.weight t = rk'.weight t

theorem BSeries.RungeKutta.agreeUpToOrder_all_iff_series_eq {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) : (∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ rk.series = rk'.series

theorem BSeries.RungeKutta.agreeUpToOrder_all_iff_treeWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) : (∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (τ : HopfAlgebras.RootedTree), rk.treeWeight τ = rk'.treeWeight τ

theorem BSeries.RungeKutta.agreeUpToOrder_all_iff_weight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) : (∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (t : HopfAlgebras.PTree), rk.weight t = rk'.weight t

theorem BSeries.RungeKutta.agreeUpToOrder_all_iff_forestWeight {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) : (∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (φ : HopfAlgebras.RootedForest), rk.forestWeight φ = rk'.forestWeight φ

theorem BSeries.RungeKutta.agreeUpToOrder_all_iff_toCharacter_evalForest {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] {κ : Type u} [Fintype κ] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) : (∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (φ : HopfAlgebras.RootedForest), rk.series.toCharacter.evalForest φ = rk'.series.toCharacter.evalForest φ

def BSeries.RungeKutta.HasOrderOne {ι : Type u} {R : Type v} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) : Prop

First order condition for a Runge-Kutta tableau.

Equations

• rk.HasOrderOne = (rk.weightBullet = 1)

theorem BSeries.RungeKutta.oneStage_hasOrderOne {R : Type v} [CommSemiring R] (a : R) : (oneStage R a).HasOrderOne

theorem BSeries.RungeKutta.explicitEuler_hasOrderOne {R : Type v} [CommSemiring R] : (explicitEuler R).HasOrderOne

theorem BSeries.RungeKutta.implicitEuler_hasOrderOne {R : Type v} [CommSemiring R] : (implicitEuler R).HasOrderOne

theorem BSeries.RungeKutta.twoStageExplicit_hasOrderOne {R : Type v} [CommSemiring R] {a21 b1 b2 : R} (hsum : b1 + b2 = 1) : (twoStageExplicit R a21 b1 b2).HasOrderOne

def BSeries.RungeKutta.explicitMidpoint (R : Type v) [Field R] : RungeKutta (Fin 2) R

The explicit midpoint tableau.

Equations

• BSeries.RungeKutta.explicitMidpoint R = BSeries.RungeKutta.twoStageExplicit R 2⁻¹ 0 1

def BSeries.RungeKutta.heun (R : Type v) [Field R] : RungeKutta (Fin 2) R

Heun's explicit trapezoidal tableau.

Equations

• BSeries.RungeKutta.heun R = BSeries.RungeKutta.twoStageExplicit R 1 2⁻¹ 2⁻¹

def BSeries.RungeKutta.kuttaThirdOrder (R : Type v) [Field R] : RungeKutta (Fin 3) R

Kutta's classical three-stage third-order tableau.

Equations

• BSeries.RungeKutta.kuttaThirdOrder R = BSeries.RungeKutta.threeStageExplicit R 2⁻¹ (-1) 2 6⁻¹ (2 * 3⁻¹) 6⁻¹

def BSeries.RungeKutta.implicitMidpoint (R : Type v) [Field R] : RungeKutta PUnit.{u_1 + 1} R

The one-stage implicit midpoint tableau.

Equations

• BSeries.RungeKutta.implicitMidpoint R = BSeries.RungeKutta.oneStage R 2⁻¹

def BSeries.RungeKutta.HasOrder {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : Prop

A Runge-Kutta tableau has order n when its induced B-series has order n.

Equations

• rk.HasOrder n = rk.series.HasOrder n

theorem BSeries.RungeKutta.hasOrder_iff_treeWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (τ : HopfAlgebras.RootedTree), τ.order ≤ n → rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_weight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (t : HopfAlgebras.PTree), t.order ≤ n → rk.weight t = (↑t.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_forestCoeff {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → rk.series.forestCoeff φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_forestWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_weightList {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (ts : List HopfAlgebras.PTree), HopfAlgebras.PTree.orderList ts ≤ n → rk.weightList ts = (↑(HopfAlgebras.PTree.treeFactorialList ts))⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_toCharacter_evalForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_toCharacter_ofForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.RootedForest), φ.order ≤ n → rk.series.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_one_iff_hasOrderOne {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : rk.HasOrder 1 ↔ rk.HasOrderOne

theorem BSeries.RungeKutta.hasOrder_two_iff_hasOrderOne_and_weight_chain2 {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : rk.HasOrder 2 ↔ rk.HasOrderOne ∧ rk.weight HopfAlgebras.PTree.chain2 = 2⁻¹

theorem BSeries.RungeKutta.hasOrder_three_iff_hasOrder_two_and_weight_chain3_and_cherry {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : rk.HasOrder 3 ↔ rk.HasOrder 2 ∧ rk.weight HopfAlgebras.PTree.chain3 = 6⁻¹ ∧ rk.weight HopfAlgebras.PTree.cherry = 3⁻¹

theorem BSeries.RungeKutta.kuttaThirdOrder_hasOrder_three {R : Type v} [Field R] [CharZero R] : (kuttaThirdOrder R).HasOrder 3

theorem BSeries.RungeKutta.oneStage_hasOrder_one {R : Type v} [Field R] (a : R) : (oneStage R a).HasOrder 1

theorem BSeries.RungeKutta.oneStage_hasOrder_two_iff {R : Type v} [Field R] (a : R) : (oneStage R a).HasOrder 2 ↔ a = 2⁻¹

theorem BSeries.RungeKutta.oneStage_not_hasOrder_three {R : Type v} [Field R] [CharZero R] (a : R) : ¬(oneStage R a).HasOrder 3

theorem BSeries.RungeKutta.explicitEuler_hasOrder_one {R : Type v} [Field R] : (explicitEuler R).HasOrder 1

theorem BSeries.RungeKutta.implicitEuler_hasOrder_one {R : Type v} [Field R] : (implicitEuler R).HasOrder 1

theorem BSeries.RungeKutta.twoStageExplicit_hasOrder_one {R : Type v} [Field R] {a21 b1 b2 : R} (hsum : b1 + b2 = 1) : (twoStageExplicit R a21 b1 b2).HasOrder 1

theorem BSeries.RungeKutta.implicitMidpoint_weight_chain2 {R : Type v} [Field R] : (implicitMidpoint R).weight HopfAlgebras.PTree.chain2 = 2⁻¹

theorem BSeries.RungeKutta.implicitMidpoint_hasOrder_two {R : Type v} [Field R] : (implicitMidpoint R).HasOrder 2

theorem BSeries.RungeKutta.twoStageExplicit_hasOrder_two {R : Type v} [Field R] {a21 b1 b2 : R} (hsum : b1 + b2 = 1) (hprod : b2 * a21 = 2⁻¹) : (twoStageExplicit R a21 b1 b2).HasOrder 2

theorem BSeries.RungeKutta.explicitMidpoint_hasOrder_two {R : Type v} [Field R] : (explicitMidpoint R).HasOrder 2

theorem BSeries.RungeKutta.heun_hasOrder_two_of_half_add_half {R : Type v} [Field R] (hhalf : 2⁻¹ + 2⁻¹ = 1) : (heun R).HasOrder 2

theorem BSeries.RungeKutta.heun_hasOrder_two {R : Type v} [Field R] [CharZero R] : (heun R).HasOrder 2

theorem BSeries.RungeKutta.HasOrder.treeWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {τ : HopfAlgebras.RootedTree} (hτ : τ.order ≤ n) : rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.weight {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {t : HopfAlgebras.PTree} (ht : t.order ≤ n) : rk.weight t = (↑t.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.weightList {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {ts : List HopfAlgebras.PTree} (hts : HopfAlgebras.PTree.orderList ts ≤ n) : rk.weightList ts = (↑(HopfAlgebras.PTree.treeFactorialList ts))⁻¹

theorem BSeries.RungeKutta.HasOrder.forestCoeff {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : rk.series.forestCoeff φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.forestWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.toCharacter_evalForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.toCharacter_ofForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : φ.order ≤ n) : rk.series.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.of_agreeUpToOrder {ι : Type u} {R : Type v} [Fintype ι] [Field R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) (hrk : rk.HasOrder n) : rk'.HasOrder n

theorem BSeries.RungeKutta.hasOrder_congr {ι : Type u} {R : Type v} [Fintype ι] [Field R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) : rk.HasOrder n ↔ rk'.HasOrder n

theorem BSeries.RungeKutta.hasOrder_all_congr {ι : Type u} {R : Type v} [Fintype ι] [Field R] {κ : Type u} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} (h : ∀ (n : ℕ), rk.AgreeUpToOrder rk' n) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (n : ℕ), rk'.HasOrder n

theorem BSeries.RungeKutta.HasOrder.treeWeight_graft {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.RootedForest} (hφ : 1 + φ.order ≤ n) : ∑ i : ι, rk.b i * rk.forestStageWeight φ i = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.treeWeight_branches {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {τ : HopfAlgebras.RootedTree} (hτ : τ.order ≤ n) : ∑ i : ι, rk.b i * rk.forestStageWeight τ.branches i = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.treeWeight_butcherProduct {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.RootedForest} {τ : HopfAlgebras.RootedTree} (horder : φ.order + τ.order ≤ n) : ∑ i : ι, rk.b i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_treeWeight_butcherProduct {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree), φ.order + τ.order ≤ n → ∑ i : ι, rk.b i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_iff_treeWeight_graft {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.RootedForest), 1 + φ.order ≤ n → ∑ i : ι, rk.b i * rk.forestStageWeight φ i = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_zero {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : rk.HasOrder 0

theorem BSeries.RungeKutta.series_eq_exact_of_hasOrder_all {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} (h : ∀ (n : ℕ), rk.HasOrder n) : rk.series = Series.exact R

theorem BSeries.RungeKutta.hasOrder_all_iff_series_eq_exact {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ rk.series = Series.exact R

theorem BSeries.RungeKutta.hasOrder_all_iff_coeff {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (ξ : HopfAlgebras.TreeIndex), rk.series.coeff ξ = (Series.exact R).coeff ξ

theorem BSeries.RungeKutta.hasOrder_all_iff_toCharacter_eq_exact {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ rk.series.toCharacter = (Series.exact R).toCharacter

theorem BSeries.RungeKutta.characterEquiv_hasOrder_all_iff_exact {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ Series.characterEquiv ⟨rk.series, ⋯⟩ = Series.characterEquiv ⟨Series.exact R, ⋯⟩

theorem BSeries.RungeKutta.hasOrder_all_iff_treeWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (τ : HopfAlgebras.RootedTree), rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_treeCoeff {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (τ : HopfAlgebras.RootedTree), rk.series.coeff (HopfAlgebras.TreeIndex.tree τ) = (↑τ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_weight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (t : HopfAlgebras.PTree), rk.weight t = (↑t.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_forestWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.RootedForest), rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_forestCoeff {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.RootedForest), rk.series.forestCoeff φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_toCharacter_evalForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.RootedForest), rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_toCharacter_ofForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.RootedForest), rk.series.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_treeWeight_graft {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.RootedForest), ∑ i : ι, rk.b i * rk.forestStageWeight φ i = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_treeWeight_branches {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (τ : HopfAlgebras.RootedTree), ∑ i : ι, rk.b i * rk.forestStageWeight τ.branches i = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_treeWeight_butcherProduct {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.RootedForest) (τ : HopfAlgebras.RootedTree), ∑ i : ι, rk.b i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_all_iff_weightList {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) : (∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (ts : List HopfAlgebras.PTree), rk.weightList ts = (↑(HopfAlgebras.PTree.treeFactorialList ts))⁻¹

theorem BSeries.RungeKutta.HasOrder.mono {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {m n : ℕ} (h : rk.HasOrder n) (hmn : m ≤ n) : rk.HasOrder m

theorem BSeries.RungeKutta.oneStage_hasOrder_iff {R : Type v} [Field R] [CharZero R] (a : R) (n : ℕ) : (oneStage R a).HasOrder n ↔ n ≤ 1 ∨ n = 2 ∧ a = 2⁻¹

theorem BSeries.RungeKutta.hasOrder_succ_iff_treeWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (τ : HopfAlgebras.RootedTree), τ.order = n + 1 → rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_succ_iff_weight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (t : HopfAlgebras.PTree), t.order = n + 1 → rk.weight t = (↑t.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_succ_iff_forestWeight {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order = n + 1 → rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_succ_iff_weightList {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (ts : List HopfAlgebras.PTree), HopfAlgebras.PTree.orderList ts = n + 1 → rk.weightList ts = (↑(HopfAlgebras.PTree.treeFactorialList ts))⁻¹

theorem BSeries.RungeKutta.hasOrder_succ_iff_toCharacter_evalForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order = n + 1 → rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.hasOrder_succ_iff_toCharacter_ofForest {ι : Type u} {R : Type v} [Fintype ι] [Field R] (rk : RungeKutta ι R) (n : ℕ) : rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (φ : HopfAlgebras.RootedForest), φ.order = n + 1 → rk.series.toCharacter (HopfAlgebras.ForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

theorem BSeries.RungeKutta.HasOrder.hasOrderOne {ι : Type u} {R : Type v} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) (hn : 1 ≤ n) : rk.HasOrderOne