Iterates Material Budget Constant

Support for the Armstrong–Vicol anomalous-diffusion formalization.

def AVenhance.Infra.Section4.amnrMaterialMajorantConstant (Ccoef Cs Cv Cf : ℝ) : ℝ

One universal constant dominates the three material coefficients. It depends only on the coefficient constants, not on any iteration index.

Equations

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

theorem AVenhance.Infra.Section4.iterate_material_majorant_constant_nonneg (Ccoef Cs Cv Cf : ℝ) : 0 ≤ amnrMaterialMajorantConstant Ccoef Cs Cv Cf

theorem AVenhance.Infra.Section4.iterate_higher_material_budget_one_constant {κ 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 ≤ amnrMaterialMajorantConstant Ccoef Cs Cv Cf * (q ^ 2 * Nprev ^ 2 + q * Nprev ^ 2 + q ^ 2 * Nprevprev ^ 2) * W ^ 2

A single constant bounds the three distinct material remainders. The q term is retained separately from the two q-squared terms.