Iterates Stream Budget Normalized

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_stream_quadratic_normalization {κ u N A : ℝ} (hκ : 0 < κ) : u * (N * A / √κ) ^ 2 = u / κ * N ^ 2 * A ^ 2

Scalar diffusive normalization of a quadratic stream coefficient.

theorem AVenhance.Infra.Section4.iterate_stream_linear_normalization {κ c N Aprev A : ℝ} (hκ : 0 < κ) : c * (N * Aprev / √κ) * (N * A / √κ) = c / κ * N ^ 2 * Aprev * A

Scalar diffusive normalization of the linear drift convolution.

theorem AVenhance.Infra.Section4.iterate_stream_budget_normalized (n : ℕ) {κ u v c N Aprev A W C F ρ : ℝ} (hκ : 0 < κ) (hu : 0 ≤ u) (hv : 0 ≤ v) (hc : 0 ≤ c) (hAp : 0 ≤ Aprev) (hA : 0 ≤ A) (huF : u / κ ≤ C / F ^ 2) (hvF : v / κ ≤ C / F ^ 4) (hcρ : c / κ ≤ C * ρ) : (iterateStreamEnergyBudget n (u * (N * A / √κ) ^ 2) (v * (N * A / √κ) ^ 2) (c * (N * Aprev / √κ) * (N * A / √κ)) W fun (x : ℕ) => 1) ≤ N ^ 2 * ((C / F ^ 2 + 2 * (C / F ^ 4)) * A ^ 2 + 2 * C * ρ * Aprev * A) * W ^ 2

Both geometric kernels in the actual stream budget have their printed normalized gains. No division by the initial-data norm occurs.