le_expGrowthSup_comp — Mathlib

English

If u is monotone and the infimum of v is finite and nonzero, then the product of the infimum of v and expGrowthSup u is bounded above by expGrowthSup (u ∘ v).

Русский

Если u монотонна, а inf(v) конечен и ненулевой, то inf(v) · expGrowthSup u ≤ expGrowthSup (u ∘ v).

LaTeX

$$(linearGrowthInf v) · expGrowthSup u ≤ expGrowthSup (u ∘ v)$$

Lean4

theorem _root_.Monotone.le_expGrowthSup_comp (h : Monotone u) (hv : (linearGrowthInf fun n ↦ v n : EReal) ≠ 0) :
    (linearGrowthInf fun n ↦ v n : EReal) * expGrowthSup u ≤ expGrowthSup (u ∘ v) :=
  (log_monotone.comp h).le_linearGrowthSup_comp hv

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