Iterates Material Budget Majorant

Support for the Armstrong–Vicol anomalous-diffusion formalization.

def AVenhance.Infra.Section4.iterateHigherMaterialBudget (κ Ccoef Cs Cv Cf Gprev Gprevprev Nprev ρ q W Wprev : ℝ) : ℝ

The five material contributions in the explicit higher-increment budget.

Equations

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

theorem AVenhance.Infra.Section4.iterate_higher_material_budget_majorant {κ Ccoef Cs Cv Cf Gprev Gprevprev Nprev Nprevprev ρ q W Wprev : ℝ} (hκ : 0 ≤ κ) (hρ : 0 ≤ ρ) (hρq : ρ ≤ q) (hW : 0 ≤ Wprev) (hWle : Wprev ≤ W) (hprev : κ * Gprev ^ 2 ≤ Nprev ^ 2) (hprevprev : κ * Gprevprev ^ 2 ≤ Nprevprev ^ 2) : iterateHigherMaterialBudget κ Ccoef Cs Cv Cf Gprev Gprevprev Nprev ρ q W Wprev ≤ ((16 * Cs ^ 2 + Cs ^ 2 * (192 + 13056 * Cv ^ 2) + 96 * Cs ^ 2 + 384 * Cf ^ 2 + 32 * Ccoef ^ 2) * q ^ 2 * Nprev ^ 2 + 4 * (1 + 32 * Cs ^ 2 * Ccoef ^ 2) * q * Nprev ^ 2 + 12288 * Cs ^ 2 * Ccoef ^ 2 * q ^ 2 * Nprevprev ^ 2) * W ^ 2

The material budget has exactly the three corrected amplitude terms. The middle term is linear in q and remains in the induction.