Complex.Hadamard.norm_inv_weierstrassFactor_le_exp_far

lemma norm_inv_weierstrassFactor_le_exp_far    {m : ℕ} {τ r : ℝ} {u a : ℂ}    (hur : ‖u‖ = r) (ha : a ≠ 0)    (hz : ‖u / a‖ ≤ (1 / 2 : ℝ)) (hτ_le : τ ≤ (m + 1 : ℝ)) :    ‖(weierstrassFactor m (u / a))⁻¹‖ ≤ Real.exp ((2 : ℝ) * (r / ‖a‖) ^ τ) := by  by_cases hu : u = 0  · subst hu    have hr0 : r = 0 := by simpa [hur] using (norm_zero : ‖(0 : ℂ)‖ = 0)    subst hr0    have h0 : 0 ≤ ((0 : ℝ) / ‖a‖) ^ τ := by      exact Real.rpow_nonneg (by positivity : (0 : ℝ) ≤ 0 / ‖a‖) τ    have h0' : 0 ≤ (2 : ℝ) * ((0 : ℝ) / ‖a‖) ^ τ := mul_nonneg (by norm_num) h0    have hexp : (1 : ℝ) ≤ Real.exp ((2 : ℝ) * ((0 : ℝ) / ‖a‖) ^ τ) :=      (Real.one_le_exp_iff).2 h0'    simpa using hexp  have hlogE :=    log_norm_weierstrassFactor_ge_neg_two_pow (m := m) (z := (u / a)) hz  have hneglog : -Real.log ‖weierstrassFactor m (u / a)‖ ≤ (2 : ℝ) * (r / ‖a‖) ^ τ := by    have h1 : -Real.log ‖weierstrassFactor m (u / a)‖ ≤ (2 : ℝ) * ‖u / a‖ ^ (m + 1) := by      linarith [hlogE]    set x : ℝ := ‖u / a‖    have hx1 : x ≤ 1 := le_trans (by simpa [x] using hz) (by norm_num)    have hxpos : 0 < x := by      simpa [x] using (norm_pos_iff.2 (div_ne_zero hu ha))    have hτ_le' : τ ≤ ((m + 1 : ℕ) : ℝ) := by      simpa [Nat.cast_add, Nat.cast_one] using hτ_le    have hpow_rpow : x ^ ((m + 1 : ℕ) : ℝ) ≤ x ^ τ :=      Real.rpow_le_rpow_of_exponent_ge hxpos hx1 hτ_le'    have hpow : x ^ (m + 1) ≤ x ^ τ := by      simpa [← Real.rpow_natCast] using hpow_rpow    have h2x : (2 : ℝ) * x ^ (m + 1) ≤ (2 : ℝ) * x ^ τ :=      mul_le_mul_of_nonneg_left hpow (by positivity)    have h2 : (2 : ℝ) * ‖u / a‖ ^ (m + 1) ≤ (2 : ℝ) * (‖u / a‖ : ℝ) ^ τ := by      simpa [x] using h2x    have h3 : (‖u‖ / ‖a‖) ^ τ = (r / ‖a‖) ^ τ := by      simp [hur]    exact (h1.trans h2).trans_eq (by simp [h3])  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 : (‖u / a‖ : ℝ) = 1 := by simpa [this] using (by simp [ha])      linarith [hz, this]    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