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
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
norm_cast
no goals
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
exact hr.pow n
no goals
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
simp only [Real.rpow_mul hz r n, Real.rpow_nat_cast]