expGrowthInf_comp — Mathlib

English

If u is monotone and the sequence v has an asymptotic linear growth with limit a (a ∈ EReal, a ≠ 0, a ≠ ∞), then expGrowthInf (u ∘ v) = a · expGrowthInf u.

Русский

Если u монотонна, и v имеет асимптотически линейный рост с пределом a, где a ≠ 0 и a ≠ ∞, тогда expGrowthInf (u ∘ v) = a · expGrowthInf u.

LaTeX

$${a : EReal} (h : Monotone u) (hv : Tendsto (fun n => (v n : EReal) / n) atTop (𝓝 a)) (ha : a ≠ 0) (ha' : a ≠ ⊤) : expGrowthInf (u ∘ v) = a * expGrowthInf u$$

Lean4

theorem _root_.Monotone.expGrowthInf_comp {a : EReal} (h : Monotone u)
    (hv : Tendsto (fun n ↦ (v n : EReal) / n) atTop (𝓝 a)) (ha : a ≠ 0) (ha' : a ≠ ⊤) :
    expGrowthInf (u ∘ v) = a * expGrowthInf u :=
  (log_monotone.comp h).linearGrowthInf_comp hv ha ha'

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