Iterates Material Budget Amplitude

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_corrected_material_unnormalized {C C₀ q : ℝ} (hC : 0 ≤ C) (hC₀ : 0 < C₀) (hq : 0 < q) (hsmall : C₀ * q ≤ 1) {i : ℕ} (hi : 2 ≤ i) : C * (q ^ 2 * iterateAmplitude (C₀ * q) (i - 1) ^ 2 + q * iterateAmplitude (C₀ * q) (i - 1) ^ 2 + q ^ 2 * iterateAmplitude (C₀ * q) (i - 2) ^ 2) ≤ (C / C₀ + 2 * C / C₀ ^ 2) * iterateAmplitude (C₀ * q) i ^ 2

The corrected material budget without dividing by the initial norm. This therefore also applies to zero initial data.