Finite combinatorial bounds for actual material correction lists.

theorem AVenhance.Infra.Section4.amnrAdvectionDerivativeTerms_length (d : Option (Fin 2)) (A : List AmnrAdvectionFactor) (w : List (Option (Fin 2))) : (amnrAdvectionDerivativeTerms d A w).length = A.length + 1

theorem AVenhance.Infra.Section4.amnrChangedAdvectionDerivativeTerms_length (t : AmnrAdvectionTerm) : (amnrChangedAdvectionDerivativeTerms t).length = 3 * (t.factors.length + 1)

theorem AVenhance.Infra.Section4.amnr_flatMap_length_le {α : Type u_1} {β : Type u_2} (T : List α) (F : α → List β) (K : ℕ) (hK : ∀ t ∈ T, (F t).length ≤ K) : (List.flatMap F T).length ≤ T.length * K

A finite sum of derivative-list lengths is controlled by the common bound; no analytic assumption enters the number of correction monomials.

def AVenhance.Infra.Section4.amnrMaterialErrorCardinality : ℕ → ℕ

Recursive bound on the number of terms in the material error expansion.

Equations

• AVenhance.Infra.Section4.amnrMaterialErrorCardinality 0 = 0
• AVenhance.Infra.Section4.amnrMaterialErrorCardinality n.succ = AVenhance.Infra.Section4.amnrMaterialErrorCardinality n * (3 * (n + 1)) + 2

theorem AVenhance.Infra.Section4.amnrMaterialErrorTerms_length_le (n : ℕ) : (amnrMaterialErrorTerms n).length ≤ amnrMaterialErrorCardinality n

theorem AVenhance.Infra.Section4.amnrSpatialAdvectionTerms_length_le (α : List (Fin 2)) (T : List AmnrAdvectionTerm) (n : ℕ) (hT : ∀ t ∈ T, t.factors.length ≤ n) : (amnrSpatialAdvectionTerms α T).length ≤ T.length * (n + 1) ^ α.length

theorem AVenhance.Infra.Section4.amnrSpatialMaterialErrorTerms_length_le (α : List (Fin 2)) (n : ℕ) : (amnrSpatialAdvectionTerms α (amnrMaterialErrorTerms n)).length ≤ amnrMaterialErrorCardinality n * (n + 1) ^ α.length

Uniform finite bound at each material level and each spatial order.