Theorems · Theorem · complex analysis

Complex.IsExpCmpFilter.isLittleO_zpow_mul_exp

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

If l : Filter ℂ is an "exponential comparison filter", then for any complex a₁, a₂ and any integer 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

0 results in Mathlib

Foundations

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