Documentation

BSeries.Numerics.Composition

Composition of Runge–Kutta schemes #

Butcher's composition theorem: running one Runge–Kutta scheme for a step and then another corresponds, at the level of B-series, to the convolution (Butcher group) product of their characters. The composed scheme is the block tableau

A = [A₁ 0; 𝟙b₁ᵀ A₂], b = (b₁, b₂),

and its elementary weights satisfy ψ_{comp} = ψ₁ ⋆ ψ₂ (Butcher, Numerical Methods for ODEs, Section 383; Hairer–Lubich–Wanner III.1.4). The proof follows the stage-weight recursion: first-block stages see only rk₁, while a second-block stage weight expands as a sum over root-preserving cuts, pruned subtrees receiving the full rk₁ weight and the trunk evaluated by the rk₂ stage recursion.

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

The block tableau composing two Runge–Kutta schemes: one step of rk₁ followed by one step of rk₂.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem BSeries.RungeKutta.compose_A_inl_inl {ι : Type u} {κ : Type v} {R : Type w} [Zero R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (i j : ι) :
    (rk₁.compose rk₂).A (Sum.inl i) (Sum.inl j) = rk₁.A i j
    source
    @[simp]
    theorem BSeries.RungeKutta.compose_A_inl_inr {ι : Type u} {κ : Type v} {R : Type w} [Zero R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (i : ι) (j : κ) :
    (rk₁.compose rk₂).A (Sum.inl i) (Sum.inr j) = 0
    source
    @[simp]
    theorem BSeries.RungeKutta.compose_A_inr_inl {ι : Type u} {κ : Type v} {R : Type w} [Zero R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (i : κ) (j : ι) :
    (rk₁.compose rk₂).A (Sum.inr i) (Sum.inl j) = rk₁.b j
    source
    @[simp]
    theorem BSeries.RungeKutta.compose_A_inr_inr {ι : Type u} {κ : Type v} {R : Type w} [Zero R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (i j : κ) :
    (rk₁.compose rk₂).A (Sum.inr i) (Sum.inr j) = rk₂.A i j
    source
    @[simp]
    theorem BSeries.RungeKutta.compose_b_inl {ι : Type u} {κ : Type v} {R : Type w} [Zero R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (j : ι) :
    (rk₁.compose rk₂).b (Sum.inl j) = rk₁.b j
    source
    @[simp]
    theorem BSeries.RungeKutta.compose_b_inr {ι : Type u} {κ : Type v} {R : Type w} [Zero R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (j : κ) :
    (rk₁.compose rk₂).b (Sum.inr j) = rk₂.b j
    source
    theorem BSeries.RungeKutta.stageWeight_compose_inl {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (t : HopfAlgebras.PTree) (i : ι) :
    (rk₁.compose rk₂).stageWeight t (Sum.inl i) = rk₁.stageWeight t i

    First-block stages of the composed scheme reproduce rk₁.

    source
    theorem BSeries.RungeKutta.stageWeightList_compose_inl {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (ts : List HopfAlgebras.PTree) (i : ι) :
    (rk₁.compose rk₂).stageWeightList ts (Sum.inl i) = rk₁.stageWeightList ts i
    source
    theorem BSeries.RungeKutta.stageWeight_compose_inr {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (t : HopfAlgebras.PTree) (i : κ) :
    (rk₁.compose rk₂).stageWeight t (Sum.inr i) = (List.map (fun (c : HopfAlgebras.PTree.RootCut) => rk₁.weightList c.pruned * rk₂.stageWeight c.trunk i) t.rootCuts).sum

    The key composition identity: the stage weight of the composed scheme at a second-block stage expands as a sum over root-preserving cuts, with pruned subtrees receiving the full rk₁ weight and the trunk evaluated by rk₂.

    source
    theorem BSeries.RungeKutta.stageWeightList_compose_inr {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (ts : List HopfAlgebras.PTree) (i : κ) :
    (rk₁.compose rk₂).stageWeightList ts (Sum.inr i) = (List.map (fun (c : HopfAlgebras.PTree.RootCutList) => rk₁.weightList c.pruned * rk₂.stageWeightList c.trunks i) (HopfAlgebras.PTree.rootCutsList ts)).sum
    source
    theorem BSeries.RungeKutta.weight_compose {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (t : HopfAlgebras.PTree) :
    (rk₁.compose rk₂).weight t = (List.map (fun (c : HopfAlgebras.PTree.ChildCut) => rk₁.weightList c.pruned * c.trunk?.elim 1 rk₂.weight) t.childCuts).sum

    The elementary weight of the composed scheme as a sum over child cuts: pruned subtrees carry the full rk₁ weight, the trunk carries the rk₂ weight (empty trunk contributing 1).

    source
    theorem BSeries.RungeKutta.weight_compose_eq_convolutionCoeff {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) (t : HopfAlgebras.PTree) :
    (rk₁.compose rk₂).weight t = HopfAlgebras.PTree.convolutionCoeff rk₁.series.toCharacter rk₂.series.toCharacter t

    Butcher's composition theorem at the level of tree coefficients: the elementary weight of the composed scheme is the convolution of the two elementary weight characters.

    source
    theorem BSeries.RungeKutta.toCharacter_series_compose {ι : Type u} {κ : Type v} {R : Type w} [Fintype ι] [Fintype κ] [CommSemiring R] (rk₁ : RungeKutta ι R) (rk₂ : RungeKutta κ R) :
    (rk₁.compose rk₂).series.toCharacter = rk₁.series.toCharacter.convolution rk₂.series.toCharacter

    Butcher's composition theorem: the B-series character of a composed Runge–Kutta scheme is the convolution (Butcher group) product of the two schemes' characters (Butcher, Numerical Methods for ODEs, Theorem 383A; Hairer–Lubich–Wanner III.1.4).