Theorems · Inductive type · complex analysis

Complex.IsExpCmpFilter

Filter ℂ → Prop

We say that l : Filter ℂ is an exponential comparison filter if the real part tends to infinity along l and the imaginary part grows subexponentially compared to the real part. These properties guarantee that (fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z)) for any complex a₁, a₂ and real b₁ < b₂. In particular, the second property is automatically satisfied if the imaginary part is bounded along l.

Defined in

Mathlib.Analysis.SpecialFunctions.CompareExp

Cited by

19 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms