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]