Commit 2024-02-01 20:02 2ba297e6

feat(Analysis/SpecialFunctions): some lemmas on complex functions of natural numbers (#10034) This is the fourth PR in a sequence that adds auxiliary lemmas from the EulerProducts project to Mathlib. It adds some lemmas on functions of complex numbers applied to natural numbers:

lemma Complex.natCast_log {n : ℕ} : Real.log n = log n
lemma Complex.natCast_arg {n : ℕ} : arg n = 0
lemma Complex.natCast_mul_natCast_cpow (m n : ℕ) (s : ℂ) : (m * n : ℂ) ^ s = m ^ s * n ^ s
lemma Complex.natCast_cpow_natCast_mul (n m : ℕ) (z : ℂ) : (n : ℂ) ^ (m * z) = ((n : ℂ) ^ m) ^ z
lemma Complex.norm_log_natCast_le_rpow_div (n : ℕ) {ε : ℝ} (hε : 0 < ε) : ‖log n‖ ≤ n ^ ε / ε

(and ofNat versions of the first two).