Complex.Hadamard.norm_inv_weierstrassFactor_le_exp_near

lemma norm_inv_weierstrassFactor_le_exp_near    {m : ℕ} {τ r : ℝ} {u a : ℂ}    (hur : ‖u‖ = r) (ha : a ≠ 0) (hr : r ≠ ‖a‖)    (hmτ : (m : ℝ) ≤ τ) :    ‖(weierstrassFactor m (u / a))⁻¹‖      ≤ Real.exp (CartanBound.φ (r / ‖a‖) + (m : ℝ) * (1 + (r / ‖a‖) ^ τ)) := by  have hlog_one :      Real.log ‖(1 : ℂ) - u / a‖ ≥ -CartanBound.φ (r / ‖a‖) :=    CartanBound.log_norm_one_sub_div_ge_neg_phi (hur := hur) (ha := ha) (hr := hr)  have hbase :=    log_norm_weierstrassFactor_ge_log_norm_one_sub_sub (m := m) (z := (u / a))  have hlogE :      Real.log ‖weierstrassFactor m (u / a)‖        ≥ -CartanBound.φ (r / ‖a‖) - (m : ℝ) * max 1 (‖u / a‖ ^ m) := by    have hpls :=      norm_partialLogSum_le_nat_mul_max_one_norm_pow m (u / a)    linarith [hbase, hlog_one, hpls]  have hmax :      max 1 (‖u / a‖ ^ m) ≤ 1 + (r / ‖a‖) ^ τ :=    max_one_norm_div_pow_le_one_add_rpow (m := m) (τ := τ) (r := r) (u := u) (a := a) hur hmτ  have hneglog :      -Real.log ‖weierstrassFactor m (u / a)‖        ≤ CartanBound.φ (r / ‖a‖) + (m : ℝ) * (1 + (r / ‖a‖) ^ τ) := by    have : -Real.log ‖weierstrassFactor m (u / a)‖        ≤ CartanBound.φ (r / ‖a‖) + (m : ℝ) * max 1 (‖u / a‖ ^ m) := by      linarith [hlogE]    have hm0 : 0 ≤ (m : ℝ) := by exact_mod_cast (Nat.zero_le m)    exact this.trans (by nlinarith [mul_le_mul_of_nonneg_left hmax hm0])  have hpos : 0 < ‖weierstrassFactor m (u / a)‖ := by    have : weierstrassFactor m (u / a) ≠ 0 := by      intro h0      have : u / a = (1 : ℂ) := (weierstrassFactor_eq_zero_iff m (u / a)).1 h0      have : u = a := (div_eq_one_iff_eq ha).1 this      have : r = ‖a‖ := by simpa [this] using hur.symm      exact (hr this).elim    exact norm_pos_iff.2 this  have hEq :      ‖(weierstrassFactor m (u / a))⁻¹‖ =        Real.exp (-Real.log ‖weierstrassFactor m (u / a)‖) := by    simp [norm_inv, Real.exp_neg, Real.exp_log hpos]  have := Real.exp_le_exp.2 hneglog  simpa [hEq] using this