Complex.log_norm_weierstrassFactor_ge_neg_two_pow

lemma log_norm_weierstrassFactor_ge_neg_two_pow {m : ℕ} {z : ℂ} (hz : ‖z‖ ≤ (1 / 2 : ℝ)) :    (-2 : ℝ) * ‖z‖ ^ (m + 1) ≤ Real.log ‖weierstrassFactor m z‖ := by  have hz_lt : ‖z‖ < (1 : ℝ) := lt_of_le_of_lt hz (by norm_num)  have hz1 : z ≠ (1 : ℂ) := by    intro h    have : (1 : ℝ) ≤ (1 / 2 : ℝ) := by      simpa [h] using hz    norm_num at this  have hEq : weierstrassFactor m z = Complex.exp (-logTail m z) :=    weierstrassFactor_eq_exp_neg_tail m hz_lt hz1  have hlog :      Real.log ‖weierstrassFactor m z‖ = (-logTail m z).re := by    simp [hEq, Complex.norm_exp, Real.log_exp]  have hre : (-logTail m z).re ≥ -‖logTail m z‖ := by    simpa [norm_neg] using Complex.neg_norm_le_re (-logTail m z)  have htail := norm_logTail_le_two_mul_norm_pow hz_lt hz m  have : (-logTail m z).re ≥ (-2 : ℝ) * ‖z‖ ^ (m + 1) := by    calc      (-logTail m z).re ≥ -‖logTail m z‖ := hre      _ ≥ (-2 : ℝ) * ‖z‖ ^ (m + 1) := by            nlinarith [htail]  simpa [hlog, mul_assoc, mul_left_comm, mul_comm] using this