Iterates First Material Budget

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Section4.iterateFirstMaterialCoefficient (C Ccoef : ℝ) : ℝ

The exceptional first-increment material coefficient.

Equations

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

noncomputable def AVenhance.Infra.Section4.iterateFirstMaterialBudget (C Ccoef ρ q N W Wbase : ℝ) : ℝ

Budget combining the three contributions to the first material derivative estimate.

Equations

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

theorem AVenhance.Infra.Section4.iterate_first_material_budget_majorant {C Ccoef ρ q N W Wbase : ℝ} (hρ : 0 ≤ ρ) (hρq : ρ ≤ q) (hW : 0 ≤ Wbase) (hWle : Wbase ≤ W) : iterateFirstMaterialBudget C Ccoef ρ q N W Wbase ≤ (iterateFirstMaterialCoefficient C Ccoef + 384 * C ^ 2 + 32 * Ccoef ^ 2) * q ^ 2 * N ^ 2 * W ^ 2

The first material budget carries two powers of q.

theorem AVenhance.Infra.Section4.iterate_first_material_budget_normalized {C Ccoef ρ q N W Wbase C₀ : ℝ} (hρ : 0 ≤ ρ) (hρq : ρ ≤ q) (hW : 0 ≤ Wbase) (hWle : Wbase ≤ W) (hC₀ : C₀ ≠ 0) : 24 * iterateFirstMaterialBudget C Ccoef ρ q N W Wbase ≤ 24 * (iterateFirstMaterialCoefficient C Ccoef + 384 * C ^ 2 + 32 * Ccoef ^ 2) / C₀ ^ 2 * N ^ 2 * (C₀ * q) ^ 2 * W ^ 2

First-increment normalization avoids division by the initial-data norm.