Iterates Homogeneous Previous Scale

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_homogeneous_previous_material_scale_bound (n : ℕ) {κ D L Cs q H N : ℝ} (hκ : 0 < κ) (hD : 0 ≤ D) (hL : 0 < L) (hCs : 0 ≤ Cs) (hq : 0 ≤ q) (hH : 0 ≤ H) (hscale : D * L ^ 2 ≤ Cs * q) : 24 * D ^ 2 / κ * (H * κ ^ 2 * (N / √κ) ^ 2 * (↑(n + 2).factorial * L ^ (n + 2)) ^ 2) ≤ 24 * Cs ^ 2 * H * q ^ 2 * N ^ 2 * (↑(n + 2).factorial * L ^ n) ^ 2

Normalize the homogeneous previous-material contribution at q squared.