Theorems · Theorem · complex analysis

Complex.IsExpCmpFilter.isLittleO_cpow_exp

∀ {l : Filter ℂ},
  Complex.IsExpCmpFilter l → ∀ (a : ℂ) {b : ℝ}, 0 < b → (fun z => z ^ a) =o[l] fun z => Complex.exp (↑b * z)

If l : Filter ℂ is an "exponential comparison filter", then for any complex a and any positive real b, we have (fun z ↦ z ^ a) =o[l] (fun z ↦ exp (b * z)).

Defined in

Mathlib.Analysis.SpecialFunctions.CompareExp

Cited by

1 results in Mathlib

Foundations

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