Smallness From Power

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

theorem CIV.forall_eps_of_le_ofReal_rpow {F : ℝ → ENNReal} {K γ r₁ : ℝ} (hγ : 0 < γ) (hr₁ : 0 < r₁) (hF : ∀ (r : ℝ), 0 < r → r ≤ r₁ → F r ≤ ENNReal.ofReal (K * r ^ γ)) (ε : ℝ) : 0 < ε → ∃ (r₀ : ℝ), 0 < r₀ ∧ ∀ (r : ℝ), 0 < r → r < r₀ → F r ≤ ENNReal.ofReal ε

If F r is bounded by K * r^γ for small r, then F r can be made arbitrarily small. This is the key analytic fact that smallness of F follows from a power‑law bound: lemma lem:aniso:closure in arXiv:2609.20803.