ENNReal Decay

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

theorem CIV.tendsto_ofReal_mul_abs_rpow_neg_atBot (C : ℝ) {kap : ℝ} (hkap : 0 < kap) : Filter.Tendsto (fun (t : ℝ) => ENNReal.ofReal (C * |t| ^ (-kap))) Filter.atBot (nhds 0)

The limit of C * |t|^(-kap) as t → -∞ is 0 in ℝ≥0∞, for any real C and positive exponent kap.

theorem CIV.eq_zero_of_le_of_tendsto_zero {a : ENNReal} {g : ℕ → ENNReal} (h : ∀ (n : ℕ), a ≤ g n) (hg : Filter.Tendsto g Filter.atTop (nhds 0)) : a = 0

If a ≤ g n for all n and g n → 0, then a = 0 in ℝ≥0∞.