Theorems · Theorem · complex analysis

Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp

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

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

Defined in

Mathlib.Analysis.SpecialFunctions.CompareExp

Cited by

3 results in Mathlib

Foundations

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