le_expGrowthInf_comp — Mathlib

English

For finite ι and u : ι → ℕ → ℝ≥0∞, expGrowthSup (iSup i, u i) = iSup i, expGrowthSup(u i).

Русский

Для конечного индекса i и семейства u_i: expGrowthSup(iSup_i u_i) = iSup_i expGrowthSup(u_i).

LaTeX

$$$\expGrowthSup\left(\iSup i, u_i\right) = \iSup i, \expGrowthSup(u_i)$$$

Lean4

theorem le_expGrowthInf_comp (hu : 1 ≤ᶠ[atTop] u) (hv : Tendsto v atTop atTop) :
    (linearGrowthInf fun n ↦ v n : EReal) * expGrowthInf u ≤ expGrowthInf (u ∘ v) :=
  by
  apply le_linearGrowthInf_comp (hu.mono fun n h ↦ ?_) hv
  rw [Pi.one_apply] at h
  rwa [Pi.zero_apply, zero_le_log_iff]

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