Theorems · Theorem · approximation theory

Monotone.linearGrowthSup_comp

∀ {u : ℕ → EReal} {v : ℕ → ℕ} {a : EReal},
  Monotone u →
    Filter.Tendsto (fun n => ↑(v n) / ↑n) Filter.atTop (nhds a) →
      a ≠ 0 → a ≠ ⊤ → LinearGrowth.linearGrowthSup (u ∘ v) = a * LinearGrowth.linearGrowthSup u

Defined in

Mathlib.Analysis.Asymptotics.LinearGrowth

Cited by

2 results in Mathlib

Foundations

Depth 172 from the axioms · uses propext, Classical.choice, Quot.sound