Theorems · Theorem · complex analysis

Complex.tendsto_one_add_pow_exp_of_tendsto

∀ {g : ℕ → ℂ} {t : ℂ},
  Filter.Tendsto (fun n => ↑n * g n) Filter.atTop (nhds t) →
    Filter.Tendsto (fun n => (1 + g n) ^ n) Filter.atTop (nhds (Complex.exp t))

The limit of (1 + g n) ^ n as (n : ℝ) → ∞ is exp t, where t : ℂ is the limit of n * g n.

Defined in

Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Cited by

1 results in Mathlib

Foundations

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