A memoised elementary-weight evaluator

The recursive elementary weight RungeKutta.weight recomputes stage weights of shared subtrees once per surrounding stage index, which is exponentially slow for native_decide sweeps over expensive coefficient fields (rational functions of a generic parameter). This file provides RungeKutta.fastWeight, which annotates each subtree once with its full stage-weight vector, together with the correctness theorem fastWeight_eq identifying it with weight.

Composed tableaux are sum-indexed; combine with weight_reindex and finSumFinEquiv to evaluate them through a Fin-indexed scheme.

@[irreducible]

def BSeries.RungeKutta.stageAnn {R : Type v} [CommSemiring R] {n : ℕ} (rk : RungeKutta (Fin n) R) : HopfAlgebras.PTree → List R

The stage-weight vector of a tree, computed bottom-up: each subtree is annotated exactly once.

Equations

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

def BSeries.RungeKutta.fastWeight {R : Type v} [CommSemiring R] {n : ℕ} (rk : RungeKutta (Fin n) R) (t : HopfAlgebras.PTree) : R

The memoised elementary weight.

Equations

• rk.fastWeight t = (List.map (fun (i : ℕ) => (if h : i < n then rk.b ⟨i, h⟩ else 0) * (rk.stageAnn t).getD i 0) (List.range n)).sum

def BSeries.RungeKutta.materialize {R : Type v} [CommSemiring R] {n : ℕ} (rk : RungeKutta (Fin n) R) : RungeKutta (Fin n) R

Materialise a Fin-indexed tableau: all entries are computed once and stored as lists, so that repeated access during a weight sweep does not re-evaluate expensive coefficient expressions.

Equations

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

theorem BSeries.RungeKutta.materialize_eq {R : Type v} [CommSemiring R] {n : ℕ} (rk : RungeKutta (Fin n) R) : rk.materialize = rk

theorem BSeries.RungeKutta.fastWeight_eq {R : Type v} [CommSemiring R] {n : ℕ} (rk : RungeKutta (Fin n) R) (t : HopfAlgebras.PTree) : rk.fastWeight t = rk.weight t

The memoised evaluator computes the elementary weight.