expGrowthSup_comp_nonneg — Mathlib

English

If u is monotone, nonzero, and v grows to infinity, then the supremum growth of the composition is nonnegative: expGrowthSup(u ∘ v) ≥ 0.

Русский

Пусть u монотонна, не нулевая, а v растет до бесконечности. Тогда рост над экспонентой композиции неотрицателен: expGrowthSup(u ∘ v) ≥ 0.

LaTeX

$$$0 \le \expGrowthSup (u \circ v)$$$

Lean4

theorem expGrowthSup_comp_nonneg (h : Monotone u) (h' : u ≠ 0) (hv : Tendsto v atTop atTop) :
    0 ≤ expGrowthSup (u ∘ v) :=
  (expGrowthInf_comp_nonneg h h' hv).trans expGrowthInf_le_expGrowthSup

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