Growth estimates on x ^ y for complex x, y

Let l be a filter on ℂ such that Complex.re tends to infinity along l and Complex.im z grows at a subexponential rate compared to Complex.re z. Then

• Complex.isLittleO_log_abs_re: Real.log ∘ Complex.abs is o-small of Complex.re along l;

• Complex.isLittleO_cpow_mul_exp: $z^{a_1}e^{b_1 * z} = o\left(z^{a_1}e^{b_1 * z}\right)$ along l for any complex a₁, a₂ and real b₁ < b₂.

We use these assumptions on l for two reasons. First, these are the assumptions that naturally appear in the proof. Second, in some applications (e.g., in Ilyashenko's proof of the individual finiteness theorem for limit cycles of polynomial ODEs with hyperbolic singularities only) natural stronger assumptions (e.g., im z is bounded from below and from above) are not available.

structure Complex.IsExpCmpFilter (l : 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.

• tendsto_re : Filter.Tendsto re l Filter.atTop
• isBigO_im_pow_re (n : ℕ) : (fun (z : ℂ) => z.im ^ n) =O[l] fun (z : ℂ) => Real.exp z.re

Alternative constructors

theorem Complex.IsExpCmpFilter.of_isBigO_im_re_rpow {l : Filter ℂ} (hre : Filter.Tendsto re l Filter.atTop) (r : ℝ) (hr : im =O[l] fun (z : ℂ) => z.re ^ r) : IsExpCmpFilter l

theorem Complex.IsExpCmpFilter.of_isBigO_im_re_pow {l : Filter ℂ} (hre : Filter.Tendsto re l Filter.atTop) (n : ℕ) (hr : im =O[l] fun (z : ℂ) => z.re ^ n) : IsExpCmpFilter l

theorem Complex.IsExpCmpFilter.of_boundedUnder_abs_im {l : Filter ℂ} (hre : Filter.Tendsto re l Filter.atTop) (him : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l fun (z : ℂ) => |z.im|) : IsExpCmpFilter l

theorem Complex.IsExpCmpFilter.of_boundedUnder_im {l : Filter ℂ} (hre : Filter.Tendsto re l Filter.atTop) (him_le : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) l im) (him_ge : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) l im) : IsExpCmpFilter l

Preliminary lemmas

theorem Complex.IsExpCmpFilter.eventually_ne {l : Filter ℂ} (hl : IsExpCmpFilter l) : ∀ᶠ (w : ℂ) in l, w ≠ 0

theorem Complex.IsExpCmpFilter.tendsto_abs_re {l : Filter ℂ} (hl : IsExpCmpFilter l) : Filter.Tendsto (fun (z : ℂ) => |z.re|) l Filter.atTop

theorem Complex.IsExpCmpFilter.tendsto_norm {l : Filter ℂ} (hl : IsExpCmpFilter l) : Filter.Tendsto norm l Filter.atTop

@[deprecated Complex.IsExpCmpFilter.tendsto_norm (since := "2025-02-17")]

theorem Complex.IsExpCmpFilter.tendsto_abs {l : Filter ℂ} (hl : IsExpCmpFilter l) : Filter.Tendsto norm l Filter.atTop

Alias of Complex.IsExpCmpFilter.tendsto_norm.

theorem Complex.IsExpCmpFilter.isLittleO_log_re_re {l : Filter ℂ} (hl : IsExpCmpFilter l) : (fun (z : ℂ) => Real.log z.re) =o[l] re

theorem Complex.IsExpCmpFilter.isLittleO_im_pow_exp_re {l : Filter ℂ} (hl : IsExpCmpFilter l) (n : ℕ) : (fun (z : ℂ) => z.im ^ n) =o[l] fun (z : ℂ) => Real.exp z.re

theorem Complex.IsExpCmpFilter.abs_im_pow_eventuallyLE_exp_re {l : Filter ℂ} (hl : IsExpCmpFilter l) (n : ℕ) : (fun (z : ℂ) => |z.im| ^ n) ≤ᶠ[l] fun (z : ℂ) => Real.exp z.re

theorem Complex.IsExpCmpFilter.isLittleO_log_norm_re {l : Filter ℂ} (hl : IsExpCmpFilter l) : (fun (z : ℂ) => Real.log ‖z‖) =o[l] re

If l : Filter ℂ is an "exponential comparison filter", then $\log |z| =o(ℜ z)$ along l. This is the main lemma in the proof of Complex.IsExpCmpFilter.isLittleO_cpow_exp below.

@[deprecated Complex.IsExpCmpFilter.isLittleO_log_norm_re (since := "2025-02-17")]

theorem Complex.IsExpCmpFilter.isLittleO_log_abs_re {l : Filter ℂ} (hl : IsExpCmpFilter l) : (fun (z : ℂ) => Real.log ‖z‖) =o[l] re

Alias of Complex.IsExpCmpFilter.isLittleO_log_norm_re.

---

If l : Filter ℂ is an "exponential comparison filter", then $\log |z| =o(ℜ z)$ along l. This is the main lemma in the proof of Complex.IsExpCmpFilter.isLittleO_cpow_exp below.

Main results

theorem Complex.IsExpCmpFilter.isTheta_cpow_exp_re_mul_log {l : Filter ℂ} (hl : IsExpCmpFilter l) (a : ℂ) : (fun (x : ℂ) => x ^ a) =Θ[l] fun (z : ℂ) => Real.exp (a.re * Real.log ‖z‖)

theorem Complex.IsExpCmpFilter.isLittleO_cpow_exp {l : Filter ℂ} (hl : IsExpCmpFilter l) (a : ℂ) {b : ℝ} (hb : 0 < b) : (fun (z : ℂ) => z ^ a) =o[l] fun (z : ℂ) => 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)).

theorem Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp {l : Filter ℂ} {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (a₁ a₂ : ℂ) : (fun (z : ℂ) => z ^ a₁ * exp (↑b₁ * z)) =o[l] fun (z : ℂ) => z ^ a₂ * 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)).

theorem Complex.IsExpCmpFilter.isLittleO_exp_cpow {l : Filter ℂ} (hl : IsExpCmpFilter l) (a : ℂ) {b : ℝ} (hb : b < 0) : (fun (z : ℂ) => exp (↑b * z)) =o[l] fun (z : ℂ) => z ^ a

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

theorem Complex.IsExpCmpFilter.isLittleO_pow_mul_exp {l : Filter ℂ} {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (m n : ℕ) : (fun (z : ℂ) => z ^ m * exp (↑b₁ * z)) =o[l] fun (z : ℂ) => z ^ n * exp (↑b₂ * z)

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

theorem Complex.IsExpCmpFilter.isLittleO_zpow_mul_exp {l : Filter ℂ} {b₁ b₂ : ℝ} (hl : IsExpCmpFilter l) (hb : b₁ < b₂) (m n : ℤ) : (fun (z : ℂ) => z ^ m * exp (↑b₁ * z)) =o[l] fun (z : ℂ) => z ^ n * 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)).