Quantitative material bounds for one transported term in the stream recursion. The transport identity removes all spatial derivatives from the time cutoffs; the remaining spatial seminorm is the App. B.2/B.3 composition bound already used in the Section 2 induction.

noncomputable def AVenhance.Infra.Construction.MaterialRecursion.materialRecursionCutoff {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ℝ → ℝ

Product of the two time cutoffs in the material recursion.

Equations

• AVenhance.Infra.Construction.MaterialRecursion.materialRecursionCutoff I m k t = I.hatZetaML m (AVenhance.lIdx β I.Λ m k) t * I.zetaMK m k t

theorem AVenhance.Infra.Construction.MaterialRecursion.iteratedTimeDerivative_eq_iteratedDeriv {q : ℝ → ℝ} (ell : ℕ) : iteratedTimeDerivative ell q = iteratedDeriv ell q