expGrowthSup_inv — Mathlib

English

For any u: ℕ → ENNReal, the supremum of the inverse is the negative of the infimum: expGrowthSup(u^{-1}) = - expGrowthInf(u).

Русский

Для любой u: ℕ → ENNReal верно: expGrowthSup(u^{-1}) = - expGrowthInf(u).

LaTeX

$$$\expGrowthSup(u^{-1}) = -\expGrowthInf(u)$$$

Lean4

theorem expGrowthSup_inv : expGrowthSup u⁻¹ = -expGrowthInf u :=
  by
  rw [expGrowthInf, ← limsup_neg]
  refine limsup_congr (Eventually.of_forall fun n ↦ ?_)
  rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]

Похожие утверждения