Labelled Runge-Kutta B-series #

This file defines labelled elementary weights for additive, or coloured, Runge-Kutta tableaus. The coefficients of a node are selected by its label.

Main definitions #

LabelledRungeKutta - a labelled tableau with one A and b family per label
LabelledRungeKutta.stageWeight - planar labelled stage weights
LabelledRungeKutta.treeWeight - non-planar labelled tree weights
LabelledRungeKutta.series - the induced labelled B-series

source

structure BSeries.LabelledRungeKutta (α : Type u) (ι : Type v) (R : Type w) :

Type (max (max u v) w)

A labelled Runge-Kutta tableau with stage type ι, labels α, and coefficients in R.

A : α → ι → ι → R
b : α → ι → R

Instances For

source

def BSeries.LabelledRungeKutta.comapMapLabels {α : Type u} {ι : Type v} {R : Type w} {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) :

LabelledRungeKutta α ι R

Pull a labelled Runge-Kutta tableau back along a relabelling map.

Equations

BSeries.LabelledRungeKutta.comapMapLabels f rk = { A := fun (a : α) => rk.A (f a), b := fun (a : α) => rk.b (f a) }

Instances For

source

def BSeries.LabelledRungeKutta.comapConstLabel {α : Type u} {ι : Type v} {R : Type w} (a : α) (rk : LabelledRungeKutta α ι R) :

RungeKutta ι R

Restrict a labelled Runge-Kutta tableau to one constant label.

Equations

BSeries.LabelledRungeKutta.comapConstLabel a rk = { A := rk.A a, b := rk.b a }

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.comapMapLabels_A {α : Type u} {ι : Type v} {R : Type w} {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (a : α) (i j : ι) :

(comapMapLabels f rk).A a i j = rk.A (f a) i j

source

@[simp]

theorem BSeries.LabelledRungeKutta.comapMapLabels_b {α : Type u} {ι : Type v} {R : Type w} {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (a : α) (i : ι) :

(comapMapLabels f rk).b a i = rk.b (f a) i

source

@[simp]

theorem BSeries.LabelledRungeKutta.comapConstLabel_A {α : Type u} {ι : Type v} {R : Type w} (a : α) (rk : LabelledRungeKutta α ι R) (i j : ι) :

(comapConstLabel a rk).A i j = rk.A a i j

source

@[simp]

theorem BSeries.LabelledRungeKutta.comapConstLabel_b {α : Type u} {ι : Type v} {R : Type w} (a : α) (rk : LabelledRungeKutta α ι R) (i : ι) :

(comapConstLabel a rk).b i = rk.b a i

source

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

Label-dependent row sum cᵢᵃ = ∑ⱼ Aᵃᵢⱼ.

Equations

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

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.abscissa_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (a : α) (i : ι) :

(comapMapLabels f rk).abscissa a i = rk.abscissa (f a) i

source

@[simp]

theorem BSeries.LabelledRungeKutta.abscissa_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (i : ι) :

(comapConstLabel a rk).abscissa i = rk.abscissa a i

source

def BSeries.LabelledRungeKutta.stageWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

HopfAlgebras.PLTree α → ι → R

Recursive stage weight of a planar labelled tree.

Equations

rk.stageWeight (HopfAlgebras.PLTree.node a ts) x✝ = rk.stageWeightList ts x✝

Instances For

source

def BSeries.LabelledRungeKutta.stageWeightList {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

List (HopfAlgebras.PLTree α) → ι → R

Product of child contributions in the recursive labelled stage weight.

Equations

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

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.stageWeight_node {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (a : α) (ts : List (HopfAlgebras.PLTree α)) (i : ι) :

rk.stageWeight (HopfAlgebras.PLTree.node a ts) i = rk.stageWeightList ts i

source

@[simp]

theorem BSeries.LabelledRungeKutta.stageWeightList_nil {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (i : ι) :

rk.stageWeightList [] i = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.stageWeightList_cons {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (t : HopfAlgebras.PLTree α) (ts : List (HopfAlgebras.PLTree α)) (i : ι) :

rk.stageWeightList (t :: ts) i = (∑ j : ι, rk.A t.rootLabel i j * rk.stageWeight t j) * rk.stageWeightList ts i

source

@[simp]

theorem BSeries.LabelledRungeKutta.stageWeight_singleton {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (a : α) (i : ι) :

rk.stageWeight (HopfAlgebras.PLTree.node a []) i = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.stageWeightList_singleton {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (a : α) (i : ι) :

rk.stageWeightList [HopfAlgebras.PLTree.node a []] i = rk.abscissa a i

source

@[simp]

theorem BSeries.LabelledRungeKutta.stageWeightList_append {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (ts us : List (HopfAlgebras.PLTree α)) (i : ι) :

rk.stageWeightList (ts ++ us) i = rk.stageWeightList ts i * rk.stageWeightList us i

source

theorem BSeries.LabelledRungeKutta.stageWeightList_perm {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (i : ι) {ts us : List (HopfAlgebras.PLTree α)} (h : ts.Perm us) :

rk.stageWeightList ts i = rk.stageWeightList us i

source

theorem BSeries.LabelledRungeKutta.stageWeight_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (t : HopfAlgebras.PLTree α) (i : ι) :

(comapMapLabels f rk).stageWeight t i = rk.stageWeight (HopfAlgebras.PLTree.map f t) i

source

theorem BSeries.LabelledRungeKutta.stageWeightList_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (ts : List (HopfAlgebras.PLTree α)) (i : ι) :

(comapMapLabels f rk).stageWeightList ts i = rk.stageWeightList (List.map (HopfAlgebras.PLTree.map f) ts) i

source

theorem BSeries.LabelledRungeKutta.stageWeight_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (t : HopfAlgebras.PTree) (i : ι) :

(comapConstLabel a rk).stageWeight t i = rk.stageWeight (HopfAlgebras.PLTree.constLabel a t) i

source

theorem BSeries.LabelledRungeKutta.stageWeightList_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (ts : List HopfAlgebras.PTree) (i : ι) :

(comapConstLabel a rk).stageWeightList ts i = rk.stageWeightList (List.map (HopfAlgebras.PLTree.constLabel a) ts) i

source

theorem BSeries.LabelledRungeKutta.stageWeight_perm {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (i : ι) {t u : HopfAlgebras.PLTree α} :

t.Perm u → rk.stageWeight t i = rk.stageWeight u i

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

source

theorem BSeries.LabelledRungeKutta.stageWeightList_eq_of_forall₂ {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (i : ι) {ts us : List (HopfAlgebras.PLTree α)} :

List.Forall₂ HopfAlgebras.PLTree.Perm ts us → rk.stageWeightList ts i = rk.stageWeightList us i

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

source

def BSeries.LabelledRungeKutta.weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

HopfAlgebras.PLTree α → R

Elementary weight of a planar labelled rooted tree.

Equations

rk.weight (HopfAlgebras.PLTree.node a ts) = ∑ i : ι, rk.b a i * rk.stageWeightList ts i

Instances For

source

theorem BSeries.LabelledRungeKutta.weight_perm {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) {t u : HopfAlgebras.PLTree α} :

t.Perm u → rk.weight t = rk.weight u

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

source

def BSeries.LabelledRungeKutta.weightList {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (ts : List (HopfAlgebras.PLTree α)) :

Multiplicative extension of labelled elementary weights to planar forests.

Equations

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

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.weightList_nil {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

rk.weightList [] = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.weightList_cons {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (t : HopfAlgebras.PLTree α) (ts : List (HopfAlgebras.PLTree α)) :

rk.weightList (t :: ts) = rk.weight t * rk.weightList ts

source

@[simp]

theorem BSeries.LabelledRungeKutta.weightList_append {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (ts us : List (HopfAlgebras.PLTree α)) :

rk.weightList (ts ++ us) = rk.weightList ts * rk.weightList us

source

theorem BSeries.LabelledRungeKutta.weightList_perm {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) {ts us : List (HopfAlgebras.PLTree α)} (h : ts.Perm us) :

rk.weightList ts = rk.weightList us

source

theorem BSeries.LabelledRungeKutta.weight_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (t : HopfAlgebras.PLTree α) :

(comapMapLabels f rk).weight t = rk.weight (HopfAlgebras.PLTree.map f t)

source

theorem BSeries.LabelledRungeKutta.weightList_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (ts : List (HopfAlgebras.PLTree α)) :

(comapMapLabels f rk).weightList ts = rk.weightList (List.map (HopfAlgebras.PLTree.map f) ts)

source

theorem BSeries.LabelledRungeKutta.weight_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (t : HopfAlgebras.PTree) :

(comapConstLabel a rk).weight t = rk.weight (HopfAlgebras.PLTree.constLabel a t)

source

theorem BSeries.LabelledRungeKutta.weightList_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (ts : List HopfAlgebras.PTree) :

(comapConstLabel a rk).weightList ts = rk.weightList (List.map (HopfAlgebras.PLTree.constLabel a) ts)

source

def BSeries.LabelledRungeKutta.treeStageWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) (i : ι) :

Recursive stage weight of a non-planar labelled rooted tree.

Equations

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

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.treeStageWeight_ofPLTree {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (t : HopfAlgebras.PLTree α) (i : ι) :

rk.treeStageWeight (HopfAlgebras.LRootedTree.ofPLTree t) i = rk.stageWeight t i

source

theorem BSeries.LabelledRungeKutta.treeStageWeight_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (τ : HopfAlgebras.LRootedTree α) (i : ι) :

(comapMapLabels f rk).treeStageWeight τ i = rk.treeStageWeight (HopfAlgebras.LRootedTree.map f τ) i

source

theorem BSeries.LabelledRungeKutta.treeStageWeight_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.RootedTree) (i : ι) :

(comapConstLabel a rk).treeStageWeight τ i = rk.treeStageWeight (HopfAlgebras.LRootedTree.constLabel a τ) i

source

def BSeries.LabelledRungeKutta.forestStageWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) (i : ι) :

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

Equations

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

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestStageWeight_zero {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (i : ι) :

rk.forestStageWeight 0 i = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestStageWeight_empty {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (i : ι) :

rk.forestStageWeight HopfAlgebras.LRootedForest.empty i = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestStageWeight_singleton {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) (i : ι) :

rk.forestStageWeight (HopfAlgebras.LRootedForest.singleton τ) i = ∑ j : ι, rk.A τ.rootLabel i j * rk.treeStageWeight τ j

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestStageWeight_add {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ ψ : HopfAlgebras.LRootedForest α) (i : ι) :

rk.forestStageWeight (φ + ψ) i = rk.forestStageWeight φ i * rk.forestStageWeight ψ i

source

theorem BSeries.LabelledRungeKutta.forestStageWeight_ofPLTree_list {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (ts : List (HopfAlgebras.PLTree α)) (i : ι) :

rk.forestStageWeight (↑(List.map HopfAlgebras.LRootedTree.ofPLTree ts)) i = rk.stageWeightList ts i

source

theorem BSeries.LabelledRungeKutta.forestStageWeight_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (φ : HopfAlgebras.LRootedForest α) (i : ι) :

(comapMapLabels f rk).forestStageWeight φ i = rk.forestStageWeight (HopfAlgebras.LRootedForest.mapLabels f φ) i

source

theorem BSeries.LabelledRungeKutta.forestStageWeight_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.RootedForest) (i : ι) :

(comapConstLabel a rk).forestStageWeight φ i = rk.forestStageWeight (HopfAlgebras.LRootedForest.constLabel a φ) i

source

@[simp]

theorem BSeries.LabelledRungeKutta.treeStageWeight_graft {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (a : α) (φ : HopfAlgebras.LRootedForest α) (i : ι) :

rk.treeStageWeight (HopfAlgebras.LRootedForest.graft a φ) i = rk.forestStageWeight φ i

source

@[simp]

theorem BSeries.LabelledRungeKutta.treeStageWeight_branches {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) (i : ι) :

rk.treeStageWeight τ i = rk.forestStageWeight τ.branches i

source

@[simp]

theorem BSeries.LabelledRungeKutta.treeStageWeight_butcherProduct {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α) (i : ι) :

rk.treeStageWeight (φ.butcherProduct τ) i = rk.forestStageWeight φ i * rk.treeStageWeight τ i

source

def BSeries.LabelledRungeKutta.treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) :

Elementary weight of a non-planar labelled rooted tree.

Equations

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

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.treeWeight_ofPLTree {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (t : HopfAlgebras.PLTree α) :

rk.treeWeight (HopfAlgebras.LRootedTree.ofPLTree t) = rk.weight t

source

theorem BSeries.LabelledRungeKutta.treeWeight_eq_sum_treeStageWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) :

rk.treeWeight τ = ∑ i : ι, rk.b τ.rootLabel i * rk.treeStageWeight τ i

source

theorem BSeries.LabelledRungeKutta.treeWeight_graft {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (a : α) (φ : HopfAlgebras.LRootedForest α) :

rk.treeWeight (HopfAlgebras.LRootedForest.graft a φ) = ∑ i : ι, rk.b a i * rk.forestStageWeight φ i

source

theorem BSeries.LabelledRungeKutta.treeWeight_branches {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) :

rk.treeWeight τ = ∑ i : ι, rk.b τ.rootLabel i * rk.forestStageWeight τ.branches i

source

theorem BSeries.LabelledRungeKutta.treeWeight_butcherProduct {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α) :

rk.treeWeight (φ.butcherProduct τ) = ∑ i : ι, rk.b τ.rootLabel i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i)

source

theorem BSeries.LabelledRungeKutta.treeWeight_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (τ : HopfAlgebras.LRootedTree α) :

(comapMapLabels f rk).treeWeight τ = rk.treeWeight (HopfAlgebras.LRootedTree.map f τ)

source

theorem BSeries.LabelledRungeKutta.treeWeight_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.RootedTree) :

(comapConstLabel a rk).treeWeight τ = rk.treeWeight (HopfAlgebras.LRootedTree.constLabel a τ)

source

def BSeries.LabelledRungeKutta.forestWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) :

Multiplicative extension of labelled elementary weights to non-planar labelled forests.

Equations

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

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestWeight_zero {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

rk.forestWeight 0 = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestWeight_empty {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

rk.forestWeight HopfAlgebras.LRootedForest.empty = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestWeight_singleton {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) :

rk.forestWeight (HopfAlgebras.LRootedForest.singleton τ) = rk.treeWeight τ

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestWeight_add {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ ψ : HopfAlgebras.LRootedForest α) :

rk.forestWeight (φ + ψ) = rk.forestWeight φ * rk.forestWeight ψ

source

theorem BSeries.LabelledRungeKutta.forestWeight_ofPLTree_list {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (ts : List (HopfAlgebras.PLTree α)) :

rk.forestWeight ↑(List.map HopfAlgebras.LRootedTree.ofPLTree ts) = rk.weightList ts

source

theorem BSeries.LabelledRungeKutta.forestWeight_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) (φ : HopfAlgebras.LRootedForest α) :

(comapMapLabels f rk).forestWeight φ = rk.forestWeight (HopfAlgebras.LRootedForest.mapLabels f φ)

source

theorem BSeries.LabelledRungeKutta.forestWeight_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.RootedForest) :

(comapConstLabel a rk).forestWeight φ = rk.forestWeight (HopfAlgebras.LRootedForest.constLabel a φ)

source

def BSeries.LabelledRungeKutta.series {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

LSeries α R

The labelled B-series induced by a labelled Runge-Kutta tableau.

Equations

rk.series BSeries.LTreeIndex.empty = 1
rk.series (BSeries.LTreeIndex.tree τ) = rk.treeWeight τ

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.series_apply_empty {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

rk.series LTreeIndex.empty = 1

source

@[simp]

theorem BSeries.LabelledRungeKutta.series_apply_tree {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) :

rk.series (LTreeIndex.tree τ) = rk.treeWeight τ

source

theorem BSeries.LabelledRungeKutta.series_butcherProduct {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α) :

rk.series.coeff (LTreeIndex.tree (φ.butcherProduct τ)) = ∑ i : ι, rk.b τ.rootLabel i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i)

source

theorem BSeries.LabelledRungeKutta.series_graft {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (a : α) (φ : HopfAlgebras.LRootedForest α) :

rk.series.coeff (LTreeIndex.tree (HopfAlgebras.LRootedForest.graft a φ)) = ∑ i : ι, rk.b a i * rk.forestStageWeight φ i

source

theorem BSeries.LabelledRungeKutta.series_branches {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (τ : HopfAlgebras.LRootedTree α) :

rk.series.coeff (LTreeIndex.tree τ) = ∑ i : ι, rk.b τ.rootLabel i * rk.forestStageWeight τ.branches i

source

theorem BSeries.LabelledRungeKutta.series_hasUnitConstant {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) :

rk.series.HasUnitConstant

source

theorem BSeries.LabelledRungeKutta.series_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} (f : α → β) (rk : LabelledRungeKutta β ι R) :

(comapMapLabels f rk).series = LSeries.comapMapLabels f rk.series

source

theorem BSeries.LabelledRungeKutta.series_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (a : α) (rk : LabelledRungeKutta α ι R) :

(comapConstLabel a rk).series = LSeries.comapConstLabel a rk.series

source

@[simp]

theorem BSeries.LabelledRungeKutta.forestCoeff_series {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) :

rk.series.forestCoeff φ = rk.forestWeight φ

source

@[simp]

theorem BSeries.LabelledRungeKutta.toCharacter_series_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) :

rk.series.toCharacter.evalForest φ = rk.forestWeight φ

source

@[simp]

theorem BSeries.LabelledRungeKutta.toCharacter_series_ofForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : LabelledRungeKutta α ι R) (φ : HopfAlgebras.LRootedForest α) :

rk.series.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = rk.forestWeight φ

source

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

Prop

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

Equations

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

Instances For

source

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

rk.AgreeUpToOrder rk n

source

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

rk'.AgreeUpToOrder rk n

source

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

rk.AgreeUpToOrder rk'' n

source

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

rk.AgreeUpToOrder rk' m

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_iff_treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) (n : ℕ) :

rk.AgreeUpToOrder rk' n ↔ ∀ (τ : HopfAlgebras.LRootedTree α), τ.order ≤ n → rk.treeWeight τ = rk'.treeWeight τ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_iff_weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) (n : ℕ) :

rk.AgreeUpToOrder rk' n ↔ ∀ (t : HopfAlgebras.PLTree α), t.order ≤ n → rk.weight t = rk'.weight t

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_iff_forestCoeff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) (n : ℕ) :

rk.AgreeUpToOrder rk' n ↔ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → rk.series.forestCoeff φ = rk'.series.forestCoeff φ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_iff_forestWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) (n : ℕ) :

rk.AgreeUpToOrder rk' n ↔ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → rk.forestWeight φ = rk'.forestWeight φ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_iff_toCharacter_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) (n : ℕ) :

rk.AgreeUpToOrder rk' n ↔ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → rk.series.toCharacter.evalForest φ = rk'.series.toCharacter.evalForest φ

source

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

rk.treeWeight τ = rk'.treeWeight τ

source

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

rk.weight t = rk'.weight t

source

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

rk.forestWeight φ = rk'.forestWeight φ

source

theorem BSeries.LabelledRungeKutta.AgreeUpToOrder.toCharacter_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] {rk : LabelledRungeKutta α ι R} {rk' : LabelledRungeKutta α κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) {φ : HopfAlgebras.LRootedForest α} (hφ : φ.order ≤ n) :

rk.series.toCharacter.evalForest φ = rk'.series.toCharacter.evalForest φ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_succ_iff_treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) (n : ℕ) :

rk.AgreeUpToOrder rk' (n + 1) ↔ rk.AgreeUpToOrder rk' n ∧ ∀ (τ : HopfAlgebras.LRootedTree α), τ.order = n + 1 → rk.treeWeight τ = rk'.treeWeight τ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_succ_iff_weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) (n : ℕ) :

rk.AgreeUpToOrder rk' (n + 1) ↔ rk.AgreeUpToOrder rk' n ∧ ∀ (t : HopfAlgebras.PLTree α), t.order = n + 1 → rk.weight t = rk'.weight t

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_iff_series_eq {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) :

(∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ rk.series = rk'.series

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_iff_treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) :

(∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (τ : HopfAlgebras.LRootedTree α), rk.treeWeight τ = rk'.treeWeight τ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_iff_weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) :

(∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (t : HopfAlgebras.PLTree α), rk.weight t = rk'.weight t

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_iff_forestWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) :

(∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (φ : HopfAlgebras.LRootedForest α), rk.forestWeight φ = rk'.forestWeight φ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_iff_toCharacter_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (rk : LabelledRungeKutta α ι R) (rk' : LabelledRungeKutta α κ R) :

(∀ (n : ℕ), rk.AgreeUpToOrder rk' n) ↔ ∀ (φ : HopfAlgebras.LRootedForest α), rk.series.toCharacter.evalForest φ = rk'.series.toCharacter.evalForest φ

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} {κ : Type v} [Fintype κ] (f : α → β) {rk : LabelledRungeKutta β ι R} {rk' : LabelledRungeKutta β κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) :

(comapMapLabels f rk).AgreeUpToOrder (comapMapLabels f rk') n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_comapMapLabels_iff_of_surjective {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} {κ : Type v} [Fintype κ] {f : α → β} (hf : Function.Surjective f) (rk : LabelledRungeKutta β ι R) (rk' : LabelledRungeKutta β κ R) (n : ℕ) :

(comapMapLabels f rk).AgreeUpToOrder (comapMapLabels f rk') n ↔ rk.AgreeUpToOrder rk' n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} {κ : Type v} [Fintype κ] (f : α → β) {rk : LabelledRungeKutta β ι R} {rk' : LabelledRungeKutta β κ R} (h : ∀ (n : ℕ), rk.AgreeUpToOrder rk' n) (n : ℕ) :

(comapMapLabels f rk).AgreeUpToOrder (comapMapLabels f rk') n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_comapMapLabels_iff_of_surjective {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {β : Type x} {κ : Type v} [Fintype κ] {f : α → β} (hf : Function.Surjective f) (rk : LabelledRungeKutta β ι R) (rk' : LabelledRungeKutta β κ R) :

(∀ (n : ℕ), (comapMapLabels f rk).AgreeUpToOrder (comapMapLabels f rk') n) ↔ ∀ (n : ℕ), rk.AgreeUpToOrder rk' n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (a : α) {rk : LabelledRungeKutta α ι R} {rk' : LabelledRungeKutta α κ R} {n : ℕ} (h : rk.AgreeUpToOrder rk' n) :

(comapConstLabel a rk).AgreeUpToOrder (comapConstLabel a rk') n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_all_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] (a : α) {rk : LabelledRungeKutta α ι R} {rk' : LabelledRungeKutta α κ R} (h : ∀ (n : ℕ), rk.AgreeUpToOrder rk' n) (n : ℕ) :

(comapConstLabel a rk).AgreeUpToOrder (comapConstLabel a rk') n

source

def BSeries.LabelledRungeKutta.ofRungeKutta {ι : Type v} {R : Type w} (α : Type u) (rk : RungeKutta ι R) :

LabelledRungeKutta α ι R

Promote an ordinary Runge-Kutta tableau to a label-independent labelled tableau.

Equations

BSeries.LabelledRungeKutta.ofRungeKutta α rk = { A := fun (x : α) => rk.A, b := fun (x : α) => rk.b }

Instances For

source

@[simp]

theorem BSeries.LabelledRungeKutta.ofRungeKutta_A {α : Type u} {ι : Type v} {R : Type w} (rk : RungeKutta ι R) (a : α) (i j : ι) :

(ofRungeKutta α rk).A a i j = rk.A i j

source

@[simp]

theorem BSeries.LabelledRungeKutta.ofRungeKutta_b {α : Type u} {ι : Type v} {R : Type w} (rk : RungeKutta ι R) (a : α) (i : ι) :

(ofRungeKutta α rk).b a i = rk.b i

source

theorem BSeries.LabelledRungeKutta.stageWeight_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PLTree α) (i : ι) :

(ofRungeKutta α rk).stageWeight t i = rk.stageWeight t.erase i

source

theorem BSeries.LabelledRungeKutta.stageWeightList_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (ts : List (HopfAlgebras.PLTree α)) (i : ι) :

(ofRungeKutta α rk).stageWeightList ts i = rk.stageWeightList (List.map HopfAlgebras.PLTree.erase ts) i

source

theorem BSeries.LabelledRungeKutta.weight_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (t : HopfAlgebras.PLTree α) :

(ofRungeKutta α rk).weight t = rk.weight t.erase

source

theorem BSeries.LabelledRungeKutta.treeStageWeight_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.LRootedTree α) (i : ι) :

(ofRungeKutta α rk).treeStageWeight τ i = rk.treeStageWeight τ.erase i

source

theorem BSeries.LabelledRungeKutta.treeWeight_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (τ : HopfAlgebras.LRootedTree α) :

(ofRungeKutta α rk).treeWeight τ = rk.treeWeight τ.erase

source

theorem BSeries.LabelledRungeKutta.forestStageWeight_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.LRootedForest α) (i : ι) :

(ofRungeKutta α rk).forestStageWeight φ i = rk.forestStageWeight φ.erase i

source

theorem BSeries.LabelledRungeKutta.forestWeight_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) (φ : HopfAlgebras.LRootedForest α) :

(ofRungeKutta α rk).forestWeight φ = rk.forestWeight φ.erase

source

theorem BSeries.LabelledRungeKutta.series_ofRungeKutta_erase {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) :

(ofRungeKutta α rk).series = LSeries.comapEraseLabels rk.series

source

theorem BSeries.LabelledRungeKutta.series_ofRungeKutta_labelInvariant {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] (rk : RungeKutta ι R) :

(ofRungeKutta α rk).series.LabelInvariant

source

theorem BSeries.LabelledRungeKutta.oneStage_treeStageWeight {α : Type u} {R : Type w} [CommSemiring R] (a : R) (τ : HopfAlgebras.LRootedTree α) (i : PUnit.{u_1 + 1}) :

(ofRungeKutta α (RungeKutta.oneStage R a)).treeStageWeight τ i = a ^ (τ.order - 1)

source

theorem BSeries.LabelledRungeKutta.oneStage_treeWeight {α : Type u} {R : Type w} [CommSemiring R] (a : R) (τ : HopfAlgebras.LRootedTree α) :

(ofRungeKutta α (RungeKutta.oneStage R a)).treeWeight τ = a ^ (τ.order - 1)

source

theorem BSeries.LabelledRungeKutta.oneStage_series_apply_tree {α : Type u} {R : Type w} [CommSemiring R] (a : R) (τ : HopfAlgebras.LRootedTree α) :

(ofRungeKutta α (RungeKutta.oneStage R a)).series (LTreeIndex.tree τ) = a ^ (τ.order - 1)

source

theorem BSeries.LabelledRungeKutta.oneStage_forestWeight {α : Type u} {R : Type w} [CommSemiring R] (a : R) (φ : HopfAlgebras.LRootedForest α) :

(ofRungeKutta α (RungeKutta.oneStage R a)).forestWeight φ = (Multiset.map (fun (τ : HopfAlgebras.LRootedTree α) => a ^ (τ.order - 1)) φ).prod

source

theorem BSeries.LabelledRungeKutta.oneStage_forestCoeff {α : Type u} {R : Type w} [CommSemiring R] (a : R) (φ : HopfAlgebras.LRootedForest α) :

(ofRungeKutta α (RungeKutta.oneStage R a)).series.forestCoeff φ = (Multiset.map (fun (τ : HopfAlgebras.LRootedTree α) => a ^ (τ.order - 1)) φ).prod

source

theorem BSeries.LabelledRungeKutta.oneStage_toCharacter_evalForest {α : Type u} {R : Type w} [CommSemiring R] (a : R) (φ : HopfAlgebras.LRootedForest α) :

(ofRungeKutta α (RungeKutta.oneStage R a)).series.toCharacter.evalForest φ = (Multiset.map (fun (τ : HopfAlgebras.LRootedTree α) => a ^ (τ.order - 1)) φ).prod

source

theorem BSeries.LabelledRungeKutta.toCharacter_series_ofRungeKutta_labelInvariant {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] [Nonempty α] (rk : RungeKutta ι R) :

(ofRungeKutta α rk).series.toCharacter.LabelInvariant

source

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

(ofRungeKutta α rk).AgreeUpToOrder (ofRungeKutta α rk') n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_ofRungeKutta_iff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] [Nonempty α] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) (n : ℕ) :

(ofRungeKutta α rk).AgreeUpToOrder (ofRungeKutta α rk') n ↔ rk.AgreeUpToOrder rk' n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_ofRungeKutta_all {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] {rk : RungeKutta ι R} {rk' : RungeKutta κ R} (h : ∀ (n : ℕ), rk.AgreeUpToOrder rk' n) (n : ℕ) :

(ofRungeKutta α rk).AgreeUpToOrder (ofRungeKutta α rk') n

source

theorem BSeries.LabelledRungeKutta.agreeUpToOrder_ofRungeKutta_all_iff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [CommSemiring R] {κ : Type v} [Fintype κ] [Nonempty α] (rk : RungeKutta ι R) (rk' : RungeKutta κ R) :

(∀ (n : ℕ), (ofRungeKutta α rk).AgreeUpToOrder (ofRungeKutta α rk') n) ↔ ∀ (n : ℕ), rk.AgreeUpToOrder rk' n

source

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

Prop

A labelled Runge-Kutta tableau has order n when its labelled B-series agrees with the exact labelled B-series through order n.

Equations

rk.HasOrder n = rk.series.HasOrder n

Instances For

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (τ : HopfAlgebras.LRootedTree α), τ.order ≤ n → rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (t : HopfAlgebras.PLTree α), t.order ≤ n → rk.weight t = (↑t.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_forestCoeff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → rk.series.forestCoeff φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_forestWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_weightList {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (ts : List (HopfAlgebras.PLTree α)), HopfAlgebras.PLTree.orderList ts ≤ n → rk.weightList ts = (↑(HopfAlgebras.PLTree.treeFactorialList ts))⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_toCharacter_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_toCharacter_ofForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order ≤ n → rk.series.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {τ : HopfAlgebras.LRootedTree α} (hτ : τ.order ≤ n) :

rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {t : HopfAlgebras.PLTree α} (ht : t.order ≤ n) :

rk.weight t = (↑t.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.weightList {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {ts : List (HopfAlgebras.PLTree α)} (hts : HopfAlgebras.PLTree.orderList ts ≤ n) :

rk.weightList ts = (↑(HopfAlgebras.PLTree.treeFactorialList ts))⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.forestCoeff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.LRootedForest α} (hφ : φ.order ≤ n) :

rk.series.forestCoeff φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.forestWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.LRootedForest α} (hφ : φ.order ≤ n) :

rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.toCharacter_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.LRootedForest α} (hφ : φ.order ≤ n) :

rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.toCharacter_ofForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.LRootedForest α} (hφ : φ.order ≤ n) :

rk.series.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

source

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

rk'.HasOrder n

source

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

rk.HasOrder n ↔ rk'.HasOrder n

source

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

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (n : ℕ), rk'.HasOrder n

source

theorem BSeries.LabelledRungeKutta.HasOrder.treeWeight_graft {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {x : α} {φ : HopfAlgebras.LRootedForest α} (hφ : 1 + φ.order ≤ n) :

∑ i : ι, rk.b x i * rk.forestStageWeight φ i = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.treeWeight_branches {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {τ : HopfAlgebras.LRootedTree α} (hτ : τ.order ≤ n) :

∑ i : ι, rk.b τ.rootLabel i * rk.forestStageWeight τ.branches i = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.HasOrder.treeWeight_butcherProduct {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) {φ : HopfAlgebras.LRootedForest α} {τ : HopfAlgebras.LRootedTree α} (horder : φ.order + τ.order ≤ n) :

∑ i : ι, rk.b τ.rootLabel i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_treeWeight_butcherProduct {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α), φ.order + τ.order ≤ n → ∑ i : ι, rk.b τ.rootLabel i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_iff_treeWeight_graft {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder n ↔ ∀ (x : α) (φ : HopfAlgebras.LRootedForest α), 1 + φ.order ≤ n → ∑ i : ι, rk.b x i * rk.forestStageWeight φ i = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_ofRungeKutta {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : RungeKutta ι R} {n : ℕ} (h : rk.HasOrder n) :

(ofRungeKutta α rk).HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_ofRungeKutta_iff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] [Nonempty α] (rk : RungeKutta ι R) (n : ℕ) :

(ofRungeKutta α rk).HasOrder n ↔ rk.HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_ofRungeKutta_all {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : RungeKutta ι R} (h : ∀ (n : ℕ), rk.HasOrder n) (n : ℕ) :

(ofRungeKutta α rk).HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_ofRungeKutta_all_iff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] [Nonempty α] (rk : RungeKutta ι R) :

(∀ (n : ℕ), (ofRungeKutta α rk).HasOrder n) ↔ ∀ (n : ℕ), rk.HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {β : Type x} (f : α → β) {rk : LabelledRungeKutta β ι R} {n : ℕ} (h : rk.HasOrder n) :

(comapMapLabels f rk).HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_comapMapLabels_iff_of_surjective {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {β : Type x} {f : α → β} (hf : Function.Surjective f) (rk : LabelledRungeKutta β ι R) (n : ℕ) :

(comapMapLabels f rk).HasOrder n ↔ rk.HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_comapMapLabels {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {β : Type x} (f : α → β) {rk : LabelledRungeKutta β ι R} (h : ∀ (n : ℕ), rk.HasOrder n) (n : ℕ) :

(comapMapLabels f rk).HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_comapMapLabels_iff_of_surjective {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {β : Type x} {f : α → β} (hf : Function.Surjective f) (rk : LabelledRungeKutta β ι R) :

(∀ (n : ℕ), (comapMapLabels f rk).HasOrder n) ↔ ∀ (n : ℕ), rk.HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (a : α) {rk : LabelledRungeKutta α ι R} {n : ℕ} (h : rk.HasOrder n) :

(comapConstLabel a rk).HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_comapConstLabel {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (a : α) {rk : LabelledRungeKutta α ι R} (h : ∀ (n : ℕ), rk.HasOrder n) (n : ℕ) :

(comapConstLabel a rk).HasOrder n

source

theorem BSeries.LabelledRungeKutta.hasOrder_zero {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

rk.HasOrder 0

source

theorem BSeries.LabelledRungeKutta.series_eq_exact_of_hasOrder_all {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] {rk : LabelledRungeKutta α ι R} (h : ∀ (n : ℕ), rk.HasOrder n) :

rk.series = LSeries.exact α R

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_series_eq_exact {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ rk.series = LSeries.exact α R

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_coeff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (ξ : LTreeIndex α), rk.series.coeff ξ = (LSeries.exact α R).coeff ξ

source

theorem BSeries.LabelledRungeKutta.series_ofRungeKutta_eq_exact_iff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] [Nonempty α] (rk : RungeKutta ι R) :

(ofRungeKutta α rk).series = LSeries.exact α R ↔ rk.series = Series.exact R

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_toCharacter_eq_exact {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ rk.series.toCharacter = (LSeries.exact α R).toCharacter

source

theorem BSeries.LabelledRungeKutta.characterEquiv_hasOrder_all_iff_exact {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ LSeries.characterEquiv ⟨rk.series, ⋯⟩ = LSeries.characterEquiv ⟨LSeries.exact α R, ⋯⟩

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (τ : HopfAlgebras.LRootedTree α), rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_treeCoeff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (τ : HopfAlgebras.LRootedTree α), rk.series.coeff (LTreeIndex.tree τ) = (↑τ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (t : HopfAlgebras.PLTree α), rk.weight t = (↑t.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_forestWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.LRootedForest α), rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_forestCoeff {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.LRootedForest α), rk.series.forestCoeff φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_toCharacter_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.LRootedForest α), rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_toCharacter_ofForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.LRootedForest α), rk.series.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_treeWeight_graft {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (x : α) (φ : HopfAlgebras.LRootedForest α), ∑ i : ι, rk.b x i * rk.forestStageWeight φ i = (↑(1 + φ.order))⁻¹ * (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_treeWeight_branches {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (τ : HopfAlgebras.LRootedTree α), ∑ i : ι, rk.b τ.rootLabel i * rk.forestStageWeight τ.branches i = (↑τ.order)⁻¹ * (↑τ.branches.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_treeWeight_butcherProduct {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (φ : HopfAlgebras.LRootedForest α) (τ : HopfAlgebras.LRootedTree α), ∑ i : ι, rk.b τ.rootLabel i * (rk.forestStageWeight φ i * rk.treeStageWeight τ i) = (↑(φ.order + τ.order))⁻¹ * (↑(φ + τ.branches).treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_all_iff_weightList {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) :

(∀ (n : ℕ), rk.HasOrder n) ↔ ∀ (ts : List (HopfAlgebras.PLTree α)), rk.weightList ts = (↑(HopfAlgebras.PLTree.treeFactorialList ts))⁻¹

source

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

rk.HasOrder m

source

theorem BSeries.LabelledRungeKutta.hasOrder_succ_iff_treeWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (τ : HopfAlgebras.LRootedTree α), τ.order = n + 1 → rk.treeWeight τ = (↑τ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_succ_iff_weight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (t : HopfAlgebras.PLTree α), t.order = n + 1 → rk.weight t = (↑t.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_succ_iff_forestWeight {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order = n + 1 → rk.forestWeight φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_succ_iff_weightList {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (ts : List (HopfAlgebras.PLTree α)), HopfAlgebras.PLTree.orderList ts = n + 1 → rk.weightList ts = (↑(HopfAlgebras.PLTree.treeFactorialList ts))⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_succ_iff_toCharacter_evalForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order = n + 1 → rk.series.toCharacter.evalForest φ = (↑φ.treeFactorial)⁻¹

source

theorem BSeries.LabelledRungeKutta.hasOrder_succ_iff_toCharacter_ofForest {α : Type u} {ι : Type v} {R : Type w} [Fintype ι] [Field R] (rk : LabelledRungeKutta α ι R) (n : ℕ) :

rk.HasOrder (n + 1) ↔ rk.HasOrder n ∧ ∀ (φ : HopfAlgebras.LRootedForest α), φ.order = n + 1 → rk.series.toCharacter (HopfAlgebras.LForestAlgebra.ofForest φ) = (↑φ.treeFactorial)⁻¹

Documentation

BSeries.Numerics.LabelledRungeKutta

Labelled Runge-Kutta B-series #

Main definitions #