theorem arg_pow_aux (n : ℕ) (x : ℂ) (hx : x ≠ 0) (hna : |x.arg| < Real.pi / ↑n) : (x ^ n).arg = ↑n * x.arg

theorem one_add_abs_half_ne_zero {x : ℂ} (hb : ‖x‖ < 1 / 2) : 1 + x ≠ 0

theorem arg_pow (n : ℕ) (f : ℕ → ℂ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) : ∀ᶠ (m : ℕ) in Filter.atTop, ((1 + f m) ^ n).arg = ↑n * (1 + f m).arg

theorem arg_pow2 (n : ℕ) (f : UpperHalfPlane → ℂ) (hf : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds 0)) : ∀ᶠ (m : UpperHalfPlane) in UpperHalfPlane.atImInfty, ((1 + f m) ^ n).arg = ↑n * (1 + f m).arg

theorem clog_pow (n : ℕ) (f : ℕ → ℂ) (hf : Filter.Tendsto f Filter.atTop (nhds 0)) : ∀ᶠ (m : ℕ) in Filter.atTop, Complex.log ((1 + f m) ^ n) = ↑n * Complex.log (1 + f m)

theorem clog_pow2 (n : ℕ) (f : UpperHalfPlane → ℂ) (hf : Filter.Tendsto f UpperHalfPlane.atImInfty (nhds 0)) : ∀ᶠ (m : UpperHalfPlane) in UpperHalfPlane.atImInfty, Complex.log ((1 + f m) ^ n) = ↑n * Complex.log (1 + f m)

theorem log_summable_pow (f : ℕ → ℂ) (hf : Summable f) (m : ℕ) : Summable fun (n : ℕ) => Complex.log ((1 + f n) ^ m)