Iterates Velocity Radius Extension #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_positive_profile_radius_extension
{B r₀ r f : ℝ}
{n : ℕ}
(hB : 0 ≤ B)
(hr₀ : 0 < r₀)
(hr : 0 < r)
(hle : r₀ ≤ r)
(hn : 1 ≤ n)
(hf : |f| ≤ B * ↑n.factorial * r₀ ^ n)
:
A positive-order analytic profile can use any larger frequency radius while preserving the product of its prefactor and radius.