[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z => z.re ^ r
n : ℕ
⊢ (fun z => z.im ^ ↑n) =O[l] fun z => (z.re ^ r) ^ ↑n
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z => z.re ^ r
n : ℕ
⊢ (fun z => z.im ^ n) =O[l] fun z => (z.re ^ r) ^ n
[PROOFSTEP]
exact hr.pow n
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
r : ℝ
hr : im =O[l] fun z => z.re ^ r
n : ℕ
z : ℂ
hz : 0 ≤ z.re
⊢ (fun z => (z.re ^ r) ^ ↑n) z = (fun z => z.re ^ (r * ↑n)) z
[PROOFSTEP]
simp only [Real.rpow_mul hz r n, Real.rpow_nat_cast]
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : im =O[l] fun z => z.re ^ ↑n
⊢ im =O[l] fun z => z.re ^ ↑n
[PROOFSTEP]
norm_cast at hr 
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
n : ℕ
hr : im =O[l] fun z => z.re ^ n
⊢ im =O[l] fun z => z.re ^ ↑n
[PROOFSTEP]
simpa only [Real.rpow_nat_cast]
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => |z.im|
⊢ im =O[l] fun z => z.re ^ ↑0
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hre : Tendsto re l atTop
him : IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun z => |z.im|
⊢ im =O[l] fun z => z.re ^ 0
[PROOFSTEP]
simpa only [pow_zero] using @IsBoundedUnder.isBigO_const ℂ ℝ ℝ _ _ _ l him 1 one_ne_zero
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ (x : ℂ), ((fun z => z.im ^ ↑n) ^ 2) x = (x.im ^ ↑n) ^ 2
[PROOFSTEP]
simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ (x✝.im ^ ↑n) ^ 2 = x✝.im ^ (2 * ↑n)
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ (x✝.im ^ n) ^ 2 = x✝.im ^ (2 * n)
[PROOFSTEP]
rw [pow_mul']
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => z.im ^ (2 * ↑n)) =O[l] fun z => Real.exp z.re
[PROOFSTEP]
have := hl.isBigO_im_pow_re (2 * n)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
this : (fun z => z.im ^ ↑(2 * n)) =O[l] fun z => Real.exp z.re
⊢ (fun z => z.im ^ (2 * ↑n)) =O[l] fun z => Real.exp z.re
[PROOFSTEP]
norm_cast at *
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ Real.exp x✝.re = Real.exp x✝.re ^ 1
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ Real.exp x✝.re = Real.exp x✝.re ^ 1
[PROOFSTEP]
rw [pow_one]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => Real.exp z.re ^ 1) =o[l] fun z => Real.exp z.re ^ 2
[PROOFSTEP]
have := (isLittleO_pow_pow_atTop_of_lt one_lt_two).comp_tendsto <| Real.tendsto_exp_atTop.comp hl.tendsto_re
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
this : ((fun x => x ^ 1) ∘ Real.exp ∘ re) =o[l] ((fun x => x ^ 2) ∘ Real.exp ∘ re)
⊢ (fun z => Real.exp z.re ^ 1) =o[l] fun z => Real.exp z.re ^ 2
[PROOFSTEP]
simpa only [pow_one, Real.rpow_one, Real.rpow_two]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ (x : ℂ), Real.exp x.re ^ 2 = ((fun z => Real.exp z.re) ^ 2) x
[PROOFSTEP]
simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => |z.im| ^ ↑n) ≤ᶠ[l] fun z => Real.exp z.re
[PROOFSTEP]
simpa using (hl.isLittleO_im_pow_exp_re n).bound zero_lt_one
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have h2 : 0 < Real.sqrt 2 := by simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
⊢ 0 < Real.sqrt 2
[PROOFSTEP]
simp
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have hz' : 1 ≤ abs z := hz.trans (re_le_abs z)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have _ : 0 < abs z := one_pos.trans_le hz'
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
have hm₀ : 0 < max z.re |z.im| := lt_max_iff.2 (Or.inl <| one_pos.trans_le hz)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ ‖Real.log (↑abs z)‖ ≤ 1 * ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
rw [one_mul, Real.norm_eq_abs, _root_.abs_of_nonneg (Real.log_nonneg hz')]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ Real.log (↑abs z) ≤ ‖Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)‖
[PROOFSTEP]
refine' le_trans _ (le_abs_self _)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ Real.log (↑abs z) ≤ Real.log (Real.sqrt 2) + Real.log (max z.re |z.im|)
[PROOFSTEP]
rw [← Real.log_mul, Real.log_le_log, ← _root_.abs_of_nonneg (le_trans zero_le_one hz)]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ ↑abs z ≤ Real.sqrt 2 * max |z.re| |z.im|
case h
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ 0 < ↑abs z
case h₁
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ 0 < Real.sqrt 2 * max z.re |z.im|
case hx
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ Real.sqrt 2 ≠ 0
case hy
l : Filter ℂ
hl : IsExpCmpFilter l
z : ℂ
hz : 1 ≤ z.re
h2 : 0 < Real.sqrt 2
hz' : 1 ≤ ↑abs z
x✝ : 0 < ↑abs z
hm₀ : 0 < max z.re |z.im|
⊢ max z.re |z.im| ≠ 0
[PROOFSTEP]
exacts [abs_le_sqrt_two_mul_max z, one_pos.trans_le hz', mul_pos h2 hm₀, h2.ne', hm₀.ne']
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ᶠ (x : ℂ) in l, ↑n * ‖Real.log (max x.re |x.im|)‖ ≤ ‖x.re‖
[PROOFSTEP]
filter_upwards [isLittleO_iff_nat_mul_le'.1 hl.isLittleO_log_re_re n, hl.abs_im_pow_eventuallyLE_exp_re n,
  hl.tendsto_re.eventually_gt_atTop 1] with z hre him h₁
[GOAL]
case h
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
cases' le_total |z.im| z.re with hle hle
[GOAL]
case h.inl
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : |z.im| ≤ z.re
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
rwa [max_eq_left hle]
[GOAL]
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
have H : 1 < |z.im| := h₁.trans_le hle
[GOAL]
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
him : |z.im| ^ ↑n ≤ Real.exp z.re
h₁ : 1 < z.re
hle : z.re ≤ |z.im|
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
norm_cast at *
[GOAL]
case h.inr
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
z : ℂ
hre : ↑n * ‖Real.log z.re‖ ≤ ‖z.re‖
hle : z.re ≤ |z.im|
him : |z.im| ^ n ≤ Real.exp z.re
h₁ : 1 < z.re
H : 1 < |z.im|
⊢ ↑n * ‖Real.log (max z.re |z.im|)‖ ≤ ‖z.re‖
[PROOFSTEP]
rwa [max_eq_right hle, Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos (Real.log_pos H), ← Real.log_pow,
  Real.log_le_iff_le_exp (pow_pos (one_pos.trans H) _), abs_of_pos (one_pos.trans h₁)]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
z : ℂ
hz : z ≠ 0
⊢ (let_fun this := fun z => ↑abs z ^ a.re;
      this)
      z =
    (fun z => Real.exp (a.re * Real.log (↑abs z))) z
[PROOFSTEP]
simp only [Real.rpow_def_of_pos, abs.pos hz, mul_comm]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun z => Real.exp (a.re * Real.log (↑abs z))) =o[l] fun x => ‖exp (↑b * x)‖
[PROOFSTEP]
simp only [norm_eq_abs, abs_exp, ofReal_mul_re, Real.isLittleO_exp_comp_exp_comp]
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * x.re - a.re * Real.log (↑abs x)) l atTop
[PROOFSTEP]
refine' (IsEquivalent.refl.sub_isLittleO _).symm.tendsto_atTop (hl.tendsto_re.const_mul_atTop hb)
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ (fun x => a.re * Real.log (↑abs x)) =o[l] fun x => b * x.re
[PROOFSTEP]
exact (hl.isLittleO_log_abs_re.const_mul_left _).const_mul_right hb.ne'
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ (fun z => z ^ a₁ * exp (↑b₁ * z)) z = (fun z => z ^ a₂ * exp (↑b₁ * z) * z ^ (a₁ - a₂)) z
[PROOFSTEP]
simp only
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ z : ℂ
hz : z ≠ 0
⊢ z ^ a₁ * exp (↑b₁ * z) = z ^ a₂ * exp (↑b₁ * z) * z ^ (a₁ - a₂)
[PROOFSTEP]
rw [mul_right_comm, ← cpow_add _ _ hz, add_sub_cancel'_right]
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * exp (↑b₁ * z) * exp (↑(b₂ - b₁) * z)) =ᶠ[l] fun z => z ^ a₂ * exp (↑b₂ * z)
[PROOFSTEP]
simp only [ofReal_sub, sub_mul, mul_assoc, ← exp_add, add_sub_cancel'_right]
[GOAL]
l : Filter ℂ
b₁ b₂ : ℝ
hl : IsExpCmpFilter l
hb : b₁ < b₂
a₁ a₂ : ℂ
⊢ (fun z => z ^ a₂ * exp (↑b₂ * z)) =ᶠ[l] fun z => z ^ a₂ * exp (↑b₂ * z)
[PROOFSTEP]
norm_cast
[GOAL]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : b < 0
⊢ (fun z => exp (↑b * z)) =o[l] fun z => z ^ a
[PROOFSTEP]
simpa using hl.isLittleO_cpow_mul_exp hb 0 a
[GOAL]
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)
[PROOFSTEP]
simpa only [cpow_nat_cast] using hl.isLittleO_cpow_mul_exp hb m n
[GOAL]
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)
[PROOFSTEP]
simpa only [cpow_int_cast] using hl.isLittleO_cpow_mul_exp hb m n
