Iterates Stream Budget Kernel

Support for the Armstrong–Vicol anomalous-diffusion formalization.

noncomputable def AVenhance.Infra.Section4.iterateStreamEnergyBudget (n : ℕ) (u v c W : ℝ) (d : ℕ → ℝ) : ℝ

The three current-order stream contributions, with their actual kernels.

Equations

• One or more equations did not get rendered due to their size.

theorem AVenhance.Infra.Section4.iterate_stream_budget_unit_profile (n : ℕ) {u v c W : ℝ} (hu : 0 ≤ u) (hv : 0 ≤ v) (hc : 0 ≤ c) : (iterateStreamEnergyBudget n u v c W fun (x : ℕ) => 1) ≤ (u + 2 * v + 2 * c) * W ^ 2

Under the lower-order induction bound the two kernels have mass at most two; no supremum over derivative orders is required.