Complex.Gammaℝ.Stirling.bound_re_ge_zero

theorem bound_re_ge_zero :    ∃ C : ℝ, 0 < C ∧      ∀ s : ℂ, 0 ≤ s.re → 1 ≤ ‖s‖ →        ‖Complex.Gammaℝ s‖ ≤ Real.exp (C * ‖s‖ * Real.log (1 + ‖s‖)) := by  obtain ⟨C₁, hC₁_pos, hC₁⟩ := Complex.Gamma.half_bound_re_ge_zero  refine ⟨C₁ + 2, by linarith, ?_⟩  intro s hs_re hs_norm  have hdef : Complex.Gammaℝ s = (Real.pi : ℂ) ^ (-s / 2) * Complex.Gamma (s / 2) := by    simp [Complex.Gammaℝ_def]  have hΓ : ‖Complex.Gamma (s / 2)‖ ≤ Real.exp (C₁ * ‖s‖ * Real.log (1 + ‖s‖)) :=    hC₁ s hs_re hs_norm  have hpi : ‖(Real.pi : ℂ) ^ (-s / 2)‖ ≤ 1 := norm_cpow_pi_neg_half_le_one hs_re  have h1 : ‖Complex.Gammaℝ s‖ ≤ ‖(Real.pi : ℂ) ^ (-s / 2)‖ * ‖Complex.Gamma (s / 2)‖ := by    rw [hdef]; exact norm_mul_le _ _  have h2 : ‖(Real.pi : ℂ) ^ (-s / 2)‖ * ‖Complex.Gamma (s / 2)‖        ≤ Real.exp (C₁ * ‖s‖ * Real.log (1 + ‖s‖)) := by    calc ‖(Real.pi : ℂ) ^ (-s / 2)‖ * ‖Complex.Gamma (s / 2)‖        ≤ 1 * ‖Complex.Gamma (s / 2)‖ := mul_le_mul_of_nonneg_right hpi (norm_nonneg _)      _ = ‖Complex.Gamma (s / 2)‖ := by ring      _ ≤ Real.exp (C₁ * ‖s‖ * Real.log (1 + ‖s‖)) := hΓ  have hlog_nonneg : 0 ≤ Real.log (1 + ‖s‖) := Real.log_nonneg (by linarith [norm_nonneg s])  have hnorm_nonneg : 0 ≤ ‖s‖ := norm_nonneg _  have hC_le : C₁ * ‖s‖ * Real.log (1 + ‖s‖) ≤ (C₁ + 2) * ‖s‖ * Real.log (1 + ‖s‖) := by    apply mul_le_mul_of_nonneg_right _ hlog_nonneg    apply mul_le_mul_of_nonneg_right _ hnorm_nonneg    linarith  exact le_trans (le_trans h1 h2) (Real.exp_le_exp.mpr hC_le)