Theorems · Theorem · complex analysis

Complex.tendsto_pow_exp_of_isLittleO_sub_add_div

∀ {f : ℕ → ℂ} (t : ℂ),
  ((fun n => f n - (1 + t / ↑n)) =o[Filter.atTop] fun n => 1 / ↑n) →
    Filter.Tendsto (fun n => f n ^ n) Filter.atTop (nhds (Complex.exp t))

(1 + t/n + o(1/n)) ^ n → exp t for t ∈ ℂ.

Defined in

Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Cited by

1 results in Mathlib

Foundations

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