The substitution law and backward error analysis

The substitution law of B-series (Chartier–Hairer–Vilmart): a coefficient system b on trees (a "vector field series") substitutes into a B-series a by summing over all partitions of each tree into subtree blocks — b evaluated on the blocks, a on the tree obtained by contracting each block to a vertex:

(b ⋆ a)(τ) = ∑_{p ∈ partitions τ} b(root block)·∏ b(blocks)·a(τ/p).

Partitions of a planar tree correspond to subsets of its edges (the kept edges span the blocks); partitionTriples enumerates them recursively as triples (root block, other blocks, skeleton), choosing for each edge whether to keep it (child block merges into the parent block) or cut it (child block separates, contributing a vertex to the skeleton).

Backward error analysis is the inversion of substitution along a fixed unital series e (in applications, the exact flow): every consistent a is b ⋆ e for a unique modified series b (modifiedCoeff, substCoeff_modifiedCoeff, modifiedCoeff_unique) — the numerical method a is the e-flow of the modified vector field b. The inversion is by strong induction on the tree order, using that every non-trivial partition has all blocks of strictly smaller order (partitionTriples_tail_order_lt).

Partitions of a planar tree

def BSeries.partitionTriples : HopfAlgebras.PTree → List (HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree)

All edge-subset partitions of a tree, as triples (root block, other blocks, skeleton). The first triple is always the trivial partition (no edge cut).

Equations

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

def BSeries.partitionCombine : List HopfAlgebras.PTree → List (List HopfAlgebras.PTree × List HopfAlgebras.PTree × List HopfAlgebras.PTree)

Process the children of a vertex: for each child and each partition of it, either keep the connecting edge (the child's root block becomes a branch of the parent's block, the child's skeleton root merges into the parent's skeleton vertex) or cut it (the child's root block becomes a separate block, its skeleton hangs off the parent's skeleton vertex). Returns (root-block branches, other blocks, skeleton branches).

Equations

• One or more equations did not get rendered due to their size.
• BSeries.partitionCombine [] = [([], [], [])]

@[simp]

theorem BSeries.partitionTriples_node (ts : List HopfAlgebras.PTree) : partitionTriples (HopfAlgebras.PTree.node ts) = List.map (fun (rbs : List HopfAlgebras.PTree × List HopfAlgebras.PTree × List HopfAlgebras.PTree) => (HopfAlgebras.PTree.node rbs.1, rbs.2.1, HopfAlgebras.PTree.node rbs.2.2)) (partitionCombine ts)

@[simp]

theorem BSeries.partitionCombine_nil : partitionCombine [] = [([], [], [])]

theorem BSeries.partitionCombine_cons (c : HopfAlgebras.PTree) (cs : List HopfAlgebras.PTree) : partitionCombine (c :: cs) = List.flatMap (fun (t : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree) => List.flatMap (fun (rest : List HopfAlgebras.PTree × List HopfAlgebras.PTree × List HopfAlgebras.PTree) => [(t.1 :: rest.1, t.2.1 ++ rest.2.1, t.2.2.children ++ rest.2.2), (rest.1, t.1 :: (t.2.1 ++ rest.2.1), t.2.2 :: rest.2.2)]) (partitionCombine cs)) (partitionTriples c)

Structural lemmas

theorem BSeries.partitionTriples_head (t : HopfAlgebras.PTree) : (partitionTriples t).head? = some (t, [], HopfAlgebras.PTree.node [])

The head of the partition list is the trivial partition.

theorem BSeries.partitionCombine_head (ts : List HopfAlgebras.PTree) : (partitionCombine ts).head? = some (ts, [], [])

theorem BSeries.partitionTriples_eq_cons (t : HopfAlgebras.PTree) : partitionTriples t = (t, [], HopfAlgebras.PTree.node []) :: (partitionTriples t).tail

Every tree's partition list is nonempty, headed by the trivial partition.

theorem BSeries.partitionTriples_order (t : HopfAlgebras.PTree) (tr : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree) : tr ∈ partitionTriples t → tr.1.order + HopfAlgebras.PTree.orderList tr.2.1 = t.order

Partitions preserve total order: the blocks partition the vertices.

theorem BSeries.partitionCombine_order (ts : List HopfAlgebras.PTree) (rbs : List HopfAlgebras.PTree × List HopfAlgebras.PTree × List HopfAlgebras.PTree) : rbs ∈ partitionCombine ts → HopfAlgebras.PTree.orderList rbs.1 + HopfAlgebras.PTree.orderList rbs.2.1 = HopfAlgebras.PTree.orderList ts

Non-trivial partitions have small blocks

theorem BSeries.obsEmptySum_partitionTriples (t : HopfAlgebras.PTree) : (List.map (fun (tr : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree) => if tr.2.1.isEmpty = true then 1 else 0) (partitionTriples t)).sum = 1

Exactly one partition — the trivial one — has no separated blocks.

theorem BSeries.obsEmptySum_partitionCombine (ts : List HopfAlgebras.PTree) : (List.map (fun (rbs : List HopfAlgebras.PTree × List HopfAlgebras.PTree × List HopfAlgebras.PTree) => if rbs.2.1.isEmpty = true then 1 else 0) (partitionCombine ts)).sum = 1

theorem BSeries.tail_obs_ne_nil {t : HopfAlgebras.PTree} {tr : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree} (htr : tr ∈ (partitionTriples t).tail) : tr.2.1 ≠ []

Every non-trivial partition separates at least one block.

theorem BSeries.tail_rootBlock_order_lt {t : HopfAlgebras.PTree} {tr : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree} (htr : tr ∈ (partitionTriples t).tail) : tr.1.order < t.order

In a non-trivial partition, the root block is strictly smaller.

theorem BSeries.tail_block_order_lt {t : HopfAlgebras.PTree} {tr : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree} (htr : tr ∈ (partitionTriples t).tail) {o : HopfAlgebras.PTree} (ho : o ∈ tr.2.1) : o.order < t.order

In a non-trivial partition, every separated block is strictly smaller.

The substitution law

def BSeries.substCoeff {R : Type v} [CommSemiring R] (b a : HopfAlgebras.PTree → R) (t : HopfAlgebras.PTree) : R

The substitution law: substitute the vector-field series b into the B-series a by summing over all partitions — b on the blocks, a on the contracted skeleton.

Equations

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

theorem BSeries.substCoeff_eq_head_add_tail {R : Type v} [CommSemiring R] (b a : HopfAlgebras.PTree → R) (t : HopfAlgebras.PTree) : substCoeff b a t = b t * a (HopfAlgebras.PTree.node []) + (List.map (fun (tr : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree) => b tr.1 * (List.map b tr.2.1).prod * a tr.2.2) (partitionTriples t).tail).sum

Backward error analysis: the modified vector field

@[irreducible]

noncomputable def BSeries.modifiedCoeff {R : Type v} [CommRing R] (a e : HopfAlgebras.PTree → R) (t : HopfAlgebras.PTree) : R

The modified vector-field series of a relative to a unital series e: the unique b with b ⋆ e = a, constructed by strong recursion on the tree order — on each tree, subtract the contributions of all non-trivial partitions, whose blocks are strictly smaller.

Equations

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

theorem BSeries.modifiedCoeff_eq {R : Type v} [CommRing R] (a e : HopfAlgebras.PTree → R) (t : HopfAlgebras.PTree) : modifiedCoeff a e t = a t - (List.map (fun (tr : HopfAlgebras.PTree × List HopfAlgebras.PTree × HopfAlgebras.PTree) => modifiedCoeff a e tr.1 * (List.map (modifiedCoeff a e) tr.2.1).prod * e tr.2.2) (partitionTriples t).tail).sum

The defining equation of the modified series, attach-free.

theorem BSeries.substCoeff_modifiedCoeff {R : Type v} [CommRing R] (a e : HopfAlgebras.PTree → R) (he : e (HopfAlgebras.PTree.node []) = 1) (t : HopfAlgebras.PTree) : substCoeff (modifiedCoeff a e) e t = a t

Backward error analysis, existence: the modified series substitutes along e to give back a — the numerical method is the e-flow of the modified vector field.

theorem BSeries.modifiedCoeff_unique {R : Type v} [CommRing R] {a e b : HopfAlgebras.PTree → R} (he : e (HopfAlgebras.PTree.node []) = 1) (hb : ∀ (t : HopfAlgebras.PTree), substCoeff b e t = a t) (t : HopfAlgebras.PTree) : b t = modifiedCoeff a e t

Backward error analysis, uniqueness: the modified series is the only solution of b ⋆ e = a.