Iterates Radius Inflation

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_positive_radius_inflation (n : ℕ) (hn : 1 ≤ n) {r ρ : ℝ} (hr : 0 ≤ r) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) : r ^ n ≤ ρ * (r / ρ) ^ n

A small zeroth jet and an analytic positive-jet profile can use one common small profile by enlarging the radius parameter by the inverse smallness.

theorem AVenhance.Infra.Section4.iterate_positive_profile_radius_inflation (n : ℕ) (hn : 1 ≤ n) {B r ρ f : ℝ} (hB : 0 ≤ B) (hr : 0 ≤ r) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hf : |f| ≤ B * ↑n.factorial * r ^ n) : |f| ≤ B * ρ * ↑n.factorial * (r / ρ) ^ n

Positive analytic jets inherit a common small prefactor after inflation.