Iterates Inflated Radius Scale

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_inflated_radius_ratio {e γ δ L F R : ℝ} (he : 0 < e) (he1 : e ≤ 1) (hL : 0 < L) (hFpos : 0 < F) (hR : 0 ≤ R) (hγδ : 4 * δ ≤ γ) (hF : F = e ^ (1 + γ / 2) * L) : R / e / e ^ (2 * δ) / L ≤ R / F

The exponent budget gamma >= 4 delta keeps the inflated analytic frequency below R/F times the chosen norm frequency.

theorem AVenhance.Infra.Section4.iterate_inflated_radius_geometric_conditions {r rvel L R F C₀ : ℝ} (hL : 0 < L) (hr : 0 ≤ r) (hrvel : 0 ≤ rvel) (_hR : 0 ≤ R) (hC₀ : 0 < C₀) (hF : C₀ ≤ F) (hlarge : 4 * R ≤ C₀) (hscale : r / L ≤ R / F) (hvel : rvel ≤ r) : 2 * (r / L) ^ 2 ≤ 1 / 2 ∧ 2 * (rvel / L) ^ 2 ≤ 1 / 4

One uniform numerical choice of the l.V constant supplies both radius conditions after inflation.