Iterates Corrected Unnormalized Quarter

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_corrected_unnormalized_quarter_budget {C C₀ ρ F : ℝ} {i : ℕ} (hC : 0 ≤ C) (hC₀ : 1 ≤ C₀) (hρ : 0 < ρ) (hF : C₀ ≤ F) (hlarge : 32 * C ≤ C₀) (hsmall : C₀ * (ρ * F ^ 2) ≤ 1) (hi : 1 ≤ i) : (C / F ^ 2 + 2 * (C / F ^ 4)) * iterateAmplitude (C₀ * (ρ * F ^ 2)) i ^ 2 + 2 * C * ρ * iterateAmplitude (C₀ * (ρ * F ^ 2)) (i - 1) * iterateAmplitude (C₀ * (ρ * F ^ 2)) i + (C / C₀ + 2 * C / C₀ ^ 2) * iterateAmplitude (C₀ * (ρ * F ^ 2)) i ^ 2 ≤ iterateAmplitude (C₀ * (ρ * F ^ 2)) i ^ 2 / 4

Corrected total induction budget in unnormalized form. Its material term contains C/C0, and C0 is chosen large enough to absorb it.