no goals
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
simp only [Real.rpow_def_of_pos, abs.pos hz, mul_comm]
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * x.re - a.re * Real.log (↑abs x)) l atTop
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)‖
simp only [norm_eq_abs, abs_exp, ofReal_mul_re, Real.isLittleO_exp_comp_exp_comp]
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
l : Filter ℂ
hl : IsExpCmpFilter l
a : ℂ
b : ℝ
hb : 0 < b
⊢ Tendsto (fun x => b * x.re - a.re * Real.log (↑abs x)) l atTop
refine'
  (IsEquivalent.refl.sub_isLittleO _).symm.tendsto_atTop (hl.tendsto_re.const_mul_atTop hb)
no goals
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
exact (hl.isLittleO_log_abs_re.const_mul_left _).const_mul_right hb.ne'