expGrowthInf_comp_nonneg — Mathlib

English

Let u: ℕ → ℝ≥0∞ be monotone and not identically zero, and let v: ℕ → ℕ tend to infinity. Then the infimum growth of the composition is nonnegative: expGrowthInf(u ∘ v) ≥ 0.

Русский

Пусть u: ℕ → ℝ≥0∞ монотонна и не тождественно равна нулю, а v: ℕ → ℕ сходится к бесконечности. Тогда инфимум экспоненциального роста композиции неотрицателен: expGrowthInf(u ∘ v) ≥ 0.

LaTeX

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

Lean4

theorem expGrowthInf_comp_nonneg (h : Monotone u) (h' : u ≠ 0) (hv : Tendsto v atTop atTop) :
    0 ≤ expGrowthInf (u ∘ v) :=
  by
  apply linearGrowthInf_comp_nonneg (u := log ∘ u) (log_monotone.comp h) _ hv
  simp only [ne_eq, funext_iff, comp_apply, Pi.bot_apply, log_eq_bot_iff, Pi.zero_apply] at h' ⊢
  exact h'

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