Cutoff Average

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.coarseCoeff_hatXi_average_abs_le {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) (f : ℤ → ℝ) {B : ℝ} (hb : ∀ (l : ℤ), I.hatXiML m l t ≠ 0 → |f l| ≤ B) : |∑' (l : ℤ), I.hatXiML m l t * f l| ≤ B

Convexity of the large-cutoff average, including its actual finite support.