Iterates Higher Budget Small

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_higher_energy_budget_small (n : ℕ) {i : ℕ} {κ D a e L Ccoef Cs Cv Cf N ρ F C₀ C : ℝ} (hi : 1 ≤ i) (hκ : 0 < κ) (hD : 0 ≤ D) (ha : 0 ≤ a) (he : 0 ≤ e) (hL : 0 < L) (hρ : 0 < ρ) (hρq : ρ ≤ ρ * F ^ 2) (hC : 0 ≤ C) (hC₀ : 1 ≤ C₀) (hF : C₀ ≤ F) (hlarge : 32 * C ≤ C₀) (hsmall : C₀ * (ρ * F ^ 2) ≤ 1) (hmat : 24 * amnrMaterialMajorantConstant Ccoef Cs Cv Cf ≤ C) (hu : 24 * (2 * (2 ^ 19 * a) / L ^ 2) / κ ≤ C / F ^ 2) (hv : 24 * (16 / κ * (32 * a * e ^ 2) ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2) / κ ≤ C / F ^ 4) (hc : 24 * (8 * D * (8192 * a * e) * (256 * e⁻¹)) / κ ≤ C * ρ) : (24 * iterateHigherEnergyBudget n i κ D a e L Ccoef Cs Cv Cf (N * iterateAmplitude (C₀ * (ρ * F ^ 2)) (i + 1) / √κ) (N * iterateAmplitude (C₀ * (ρ * F ^ 2)) i / √κ) (N * iterateAmplitude (C₀ * (ρ * F ^ 2)) (i - 1) / √κ) (N * iterateAmplitude (C₀ * (ρ * F ^ 2)) i) ρ (ρ * F ^ 2) fun (x : ℕ) => 1) ≤ N ^ 2 * iterateAmplitude (C₀ * (ρ * F ^ 2)) (i + 1) ^ 2 * iterateAnalyticWeight n (i + 1) L ^ 2 / 4

The complete explicit higher-increment remainder closes under scalar coefficient scales. The PDE energy inequality is not an assumption here.