expGrowthInf_inv — Mathlib

English

For any u: ℕ → ENNReal, the inverse transform relates inf and sup by expGrowthInf(u^{-1}) = - expGrowthSup(u).

Русский

Для любой u: ℕ → ENNReal выполняется взаимосвязь между инф и суп через инверсию: expGrowthInf(u^{-1}) = - expGrowthSup(u).

LaTeX

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

Lean4

theorem expGrowthInf_inv : expGrowthInf u⁻¹ = -expGrowthSup u :=
  by
  rw [expGrowthSup, ← liminf_neg]
  refine liminf_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]

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