Complex.norm_mul_riemannZeta_le_exp_of_reflected

lemma norm_mul_riemannZeta_le_exp_of_reflected {z w : ℂ} {A CΓ C : ℝ}    (hw : w = 1 - z)    (hzeta_fe : riemannZeta z = 2 * (2 * π) ^ (-w) * Complex.Gamma w * Complex.cos (π * w / 2) *      riemannZeta w)    (hpow_le1 : ‖(2 * π : ℂ) ^ (-w)‖ ≤ 1)    (hw_norm_le : ‖w‖ ≤ A) (hA1 : 1 ≤ A) (hA2_nonneg : 0 ≤ A ^ (2 : ℝ))    (hΓw : ‖Complex.Gamma w‖ ≤ rexp (CΓ * A ^ (2 : ℝ)))    (hcosw : ‖Complex.cos (π * w / 2)‖ ≤ rexp (2 * A ^ (2 : ℝ)))    (hζw : ‖riemannZeta w‖ ≤ rexp (40 * A ^ (2 : ℝ)))    (hcoef : (2 + CΓ + 2 + 40 : ℝ) ≤ C) :    ‖(z - 1) * riemannZeta z‖ ≤ rexp (C * A ^ (2 : ℝ)) := by  have hprod :      ‖(z - 1) * riemannZeta z‖ ≤        (‖w‖ * 2) * ‖Complex.Gamma w‖ *          ‖Complex.cos (π * w / 2)‖ * ‖riemannZeta w‖ := by    have hz1 : (z - 1 : ℂ) = -w := by      rw [hw]      ring    have hζ :        ‖riemannZeta z‖ ≤          ‖2 * (2 * π) ^ (-w) * Complex.Gamma w *            Complex.cos (π * w / 2) * riemannZeta w‖ := by      simp [hzeta_fe]    calc      ‖(z - 1) * riemannZeta z‖          ≤ ‖z - 1‖ * ‖riemannZeta z‖ := by simp      _ ≤ ‖z - 1‖ *            ‖2 * (2 * π) ^ (-w) * Complex.Gamma w *              Complex.cos (π * w / 2) * riemannZeta w‖ := by          gcongr      _ = ‖w‖ *            ‖2 * (2 * π) ^ (-w) * Complex.Gamma w *              Complex.cos (π * w / 2) * riemannZeta w‖ := by          simp [hz1]      _ ≤ ‖w‖ * ((2 : ℝ) * ‖(2 * π : ℂ) ^ (-w)‖ *            ‖Complex.Gamma w‖ * ‖Complex.cos (π * w / 2)‖ *            ‖riemannZeta w‖) := by          have :              ‖2 * (2 * π) ^ (-w) * Complex.Gamma w *                  Complex.cos (π * w / 2) * riemannZeta w‖                ≤ (2 : ℝ) * ‖(2 * π : ℂ) ^ (-w)‖ *                  ‖Complex.Gamma w‖ * ‖Complex.cos (π * w / 2)‖ *                  ‖riemannZeta w‖ := by            simp [mul_assoc, mul_left_comm, mul_comm]          gcongr      _ ≤ ‖w‖ * ((2 : ℝ) * 1 * ‖Complex.Gamma w‖ *            ‖Complex.cos (π * w / 2)‖ * ‖riemannZeta w‖) := by          gcongr      _ = (‖w‖ * 2) * ‖Complex.Gamma w‖ *            ‖Complex.cos (π * w / 2)‖ * ‖riemannZeta w‖ := by          ring  have hw2 : ‖w‖ * 2 ≤ rexp (2 * A ^ (2 : ℝ)) := by    simpa [Real.rpow_two, sq] using Real.two_mul_le_exp_two_mul_sq hw_norm_le hA1  have hmul_exp :      (‖w‖ * 2) * ‖Complex.Gamma w‖ * ‖Complex.cos (π * w / 2)‖ *          ‖riemannZeta w‖ ≤        rexp ((2 + CΓ + 2 + 40) * A ^ (2 : ℝ)) := by    have h := Real.mul_four_le_exp_add (a := ‖w‖ * 2) (b := ‖Complex.Gamma w‖)      (c := ‖Complex.cos (π * w / 2)‖) (d := ‖riemannZeta w‖)      (A := 2 * A ^ (2 : ℝ)) (B := CΓ * A ^ (2 : ℝ))      (C := 2 * A ^ (2 : ℝ)) (D := 40 * A ^ (2 : ℝ))      (norm_nonneg _) (norm_nonneg _) (norm_nonneg _) hw2 hΓw hcosw hζw    have hsum :        2 * A ^ (2 : ℝ) + CΓ * A ^ (2 : ℝ) +            2 * A ^ (2 : ℝ) + 40 * A ^ (2 : ℝ) =          (2 + CΓ + 2 + 40) * A ^ (2 : ℝ) := by      ring    exact h.trans_eq (congrArg rexp hsum)  have hdom :      rexp ((2 + CΓ + 2 + 40) * A ^ (2 : ℝ)) ≤ rexp (C * A ^ (2 : ℝ)) := by    refine (Real.exp_le_exp).2 ?_    simpa [mul_assoc] using mul_le_mul_of_nonneg_right hcoef hA2_nonneg  exact le_trans (le_trans hprod hmul_exp) hdom