Iterates Analytic Radius Doubling

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_positive_order_radius_double {l L : ℝ} {n : ℕ} (hl : 0 ≤ l) (hL : 2 * l ≤ L) (hn : 1 ≤ n) : 2 * l ^ n ≤ L ^ n

Enlarging the norm frequency by two absorbs a fixed loss at every positive derivative order.

theorem AVenhance.Infra.Section4.iterate_positive_order_radius_four {l L : ℝ} {n : ℕ} (hl : 0 ≤ l) (hL : 4 * l ≤ L) (hn : 1 ≤ n) : 4 * l ^ n ≤ L ^ n

A larger fixed loss is absorbed in the radius at positive orders.