Documentation

BSeries.Numerics.Enumeration

Enumeration of trees by order and existence of high-order methods #

We enumerate the planar trees and forests of each order, deduce that the rooted trees of order at most p form a finite set, and combine this with the density theorem 317A to obtain Butcher's existence theorem: for every p there is a Runge–Kutta method of order p (Butcher, Numerical Methods for ODEs, Subsection 324 via Theorem 317A).

source
@[irreducible]
def BSeries.PTree.treesOfOrder :
ℕ → List HopfAlgebras.PTree

All planar trees of order exactly n.

Equations
Instances For
    source
    @[irreducible]
    def BSeries.PTree.forestsOfOrder :
    ℕ → List (List HopfAlgebras.PTree)

    All planar forests of total order exactly m.

    Equations
    Instances For
      source
      theorem BSeries.PTree.mem_treesOfOrder (t : HopfAlgebras.PTree) :
      t ∈ treesOfOrder t.order

      Completeness of the tree enumeration.

      source
      theorem BSeries.PTree.mem_forestsOfOrder (ts : List HopfAlgebras.PTree) :
      ts ∈ forestsOfOrder (HopfAlgebras.PTree.orderList ts)

      Completeness of the forest enumeration.

      source
      noncomputable def BSeries.RootedTree.treesUpToOrder (p : ℕ) :
      Finset HopfAlgebras.RootedTree

      The finite set of rooted trees of order at most p.

      Equations
      Instances For
        source
        theorem BSeries.RootedTree.mem_treesUpToOrder {p : ℕ} {τ : HopfAlgebras.RootedTree} (h : τ.order ≤ p) :
        τ ∈ treesUpToOrder p
        source
        theorem BSeries.RungeKutta.exists_rk_hasOrder (R : Type u_1) [Field R] [CharZero R] (p : ℕ) :
        ∃ (ι : Type) (x : Fintype ι) (rk : RungeKutta ι R), rk.HasOrder p

        Existence of Runge–Kutta methods of arbitrary order (Butcher, Numerical Methods for ODEs, Subsection 324, via Theorem 317A): for every p there is a Runge–Kutta method of order p.