Complex.norm_partialLogSum_le_nat_mul_max_one_norm_pow

lemma norm_partialLogSum_le_nat_mul_max_one_norm_pow (m : ℕ) (z : ℂ) :    ‖partialLogSum m z‖ ≤ (m : ℝ) * max 1 (‖z‖ ^ m) := by  have hsum :      ‖partialLogSum m z‖ ≤ ∑ k ∈ Finset.range m, ‖z ^ (k + 1) / (k + 1)‖ := by    rw [partialLogSum_eq_sum]    exact norm_sum_le _ _  have hterm : ∀ k ∈ Finset.range m, ‖z ^ (k + 1) / (k + 1)‖ ≤ max 1 (‖z‖ ^ m) := by    intro k hk    rw [norm_div, norm_pow]    have hk1 : (1 : ℝ) ≤ (k : ℝ) + 1 := by      have hk1_nat : (1 : ℕ) ≤ k + 1 := Nat.succ_le_succ (Nat.zero_le k)      exact_mod_cast hk1_nat    have hdenom : ‖((k : ℂ) + 1)‖ = (k : ℝ) + 1 := by      simpa [Nat.cast_add, Nat.cast_one, add_assoc, add_comm, add_left_comm] using        (Complex.norm_natCast (k + 1))    have hk_le : k + 1 ≤ m := Nat.succ_le_iff.2 (Finset.mem_range.1 hk)    have hpow_le : ‖z‖ ^ (k + 1) ≤ max 1 (‖z‖ ^ m) := by      have hz0 : 0 ≤ ‖z‖ := norm_nonneg z      by_cases hz1 : ‖z‖ ≤ (1 : ℝ)      · have : ‖z‖ ^ (k + 1) ≤ 1 := by exact pow_le_one₀ hz0 hz1        exact this.trans (le_max_left _ _)      · have hz1' : (1 : ℝ) ≤ ‖z‖ := le_of_lt (lt_of_not_ge hz1)        have : ‖z‖ ^ (k + 1) ≤ ‖z‖ ^ m := pow_le_pow_right₀ hz1' hk_le        exact this.trans (le_max_right _ _)    calc      ‖z‖ ^ (k + 1) / ‖((k : ℂ) + 1)‖ = ‖z‖ ^ (k + 1) / ((k : ℝ) + 1) := by simp [hdenom]      _ ≤ ‖z‖ ^ (k + 1) := by            exact div_le_self (pow_nonneg (norm_nonneg z) _) hk1      _ ≤ max 1 (‖z‖ ^ m) := hpow_le  have hsum_le :      (∑ k ∈ Finset.range m, ‖z ^ (k + 1) / (k + 1)‖) ≤        ∑ _k ∈ Finset.range m, max 1 (‖z‖ ^ m) :=    Finset.sum_le_sum (fun k hk => hterm k hk)  have hcard : ∑ _k ∈ Finset.range m, max 1 (‖z‖ ^ m) = (m : ℝ) * max 1 (‖z‖ ^ m) := by    simp [Finset.sum_const]  exact hsum.trans (hsum_le.trans_eq hcard)