no goals
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ (x : ℂ), ((fun z => z.im ^ ↑n) ^ 2) x = (x.im ^ ↑n) ^ 2
simp
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ (x✝.im ^ n) ^ 2 = x✝.im ^ (2 * n)
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ (x✝.im ^ ↑n) ^ 2 = x✝.im ^ (2 * ↑n)
norm_cast
no goals
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ (x✝.im ^ n) ^ 2 = x✝.im ^ (2 * n)
rw [pow_mul']
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
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => z.im ^ (2 * ↑n)) =O[l] fun z => Real.exp z.re
have := hl.isBigO_im_pow_re (2 * n)
no goals
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
norm_cast at *
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ Real.exp x✝.re = Real.exp x✝.re ^ 1
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ Real.exp x✝.re = Real.exp x✝.re ^ 1
norm_cast
no goals
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
x✝ : ℂ
⊢ Real.exp x✝.re = Real.exp x✝.re ^ 1
rw [pow_one]
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
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ (fun z => Real.exp z.re ^ 1) =o[l] fun z => Real.exp z.re ^ 2
have := (isLittleO_pow_pow_atTop_of_lt one_lt_two).comp_tendsto <|
  Real.tendsto_exp_atTop.comp hl.tendsto_re
no goals
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
simpa only [pow_one, Real.rpow_one, Real.rpow_two]
no goals
l : Filter ℂ
hl : IsExpCmpFilter l
n : ℕ
⊢ ∀ (x : ℂ), Real.exp x.re ^ 2 = ((fun z => Real.exp z.re) ^ 2) x
simp