Complex.Gamma.half_bound_re_ge_zero

theorem half_bound_re_ge_zero :    ∃ C : ℝ, 0 < C ∧      ∀ s : ℂ, 0 ≤ s.re → 1 ≤ ‖s‖ →        ‖Gamma (s / 2)‖ ≤ Real.exp (C * ‖s‖ * Real.log (1 + ‖s‖)) := by  classical  rcases stirling_bound_re_ge_zero with ⟨C₀, hC₀_pos, hC₀⟩  let A : ℝ := Real.Stirling.half_shift_log_constant  have hA_pos := Real.Stirling.half_shift_log_constant_pos  let C : ℝ := 1 + C₀ * A  refine ⟨C, by nlinarith [hC₀_pos, hA_pos], ?_⟩  intro s hs_re hs_norm  have hs0 : s ≠ 0 := (norm_pos_iff).1 (lt_of_lt_of_le (by norm_num) hs_norm)  have hs2_neq : s / 2 ≠ 0 := div_ne_zero hs0 (by norm_num : (2 : ℂ) ≠ 0)  have hs2_lb : (1 / 2 : ℝ) ≤ ‖s / 2‖ := by    simpa using (show (1 / 2 : ℝ) ≤ ‖s‖ / 2 by nlinarith)  have hdiv := norm_Gamma_le_two_mul_norm_Gamma_add_one hs2_neq hs2_lb  have hz_re : 0 ≤ (s / 2 + 1).re := by simp [Complex.add_re]; linarith  have hz_norm : (1 : ℝ) ≤ ‖s / 2 + 1‖ := by    have : (1 : ℝ) ≤ (s / 2 + 1).re := by simp [Complex.add_re]; linarith    exact le_trans this (Complex.re_le_norm (s / 2 + 1))  have hΓz :      ‖Gamma (s / 2 + 1)‖ ≤        Real.exp (C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)) :=    hC₀ (s / 2 + 1) hz_re hz_norm  have hprod_w :      ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖) ≤ A * (‖s‖ * Real.log (1 + ‖s‖)) := by    simpa [A] using norm_mul_log_shift_half_bound hs_norm  have hlog2_le_xlog := Real.Stirling.log_two_le_mul_log_one_add hs_norm  -- Put everything together.  have hmain :      ‖Gamma (s / 2)‖ ≤ Real.exp (C * ‖s‖ * Real.log (1 + ‖s‖)) := by    -- from `‖Γ(s/2)‖ ≤ 2‖Γ(s/2+1)‖`    have htmp :        ‖Gamma (s / 2)‖ ≤          2 * Real.exp (C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)) :=      le_trans hdiv (mul_le_mul_of_nonneg_left hΓz (by norm_num))    -- rewrite `2 = exp(log 2)`    -- convert to a single exponential and compare exponents    have htmp' :        2 * Real.exp (C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖))          = Real.exp (Real.log 2 + C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)) := by      have htwo : Real.exp (Real.log 2) = (2 : ℝ) := by        have : (0 : ℝ) < 2 := by norm_num        simp [Real.exp_log this]      -- `exp(log 2) * exp(A) = exp(log 2 + A)`      calc        2 * Real.exp (C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖))            = Real.exp (Real.log 2) *                Real.exp (C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)) := by                simp [htwo, mul_assoc]        _ = Real.exp (Real.log 2 + C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)) := by              simp [Real.exp_add]    refine le_trans htmp (by      -- compare exponents      have hexp_le :          Real.log 2 + C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)            ≤ C * (‖s‖ * Real.log (1 + ‖s‖)) := by        have hC0_nonneg : 0 ≤ C₀ := le_of_lt hC₀_pos        have hA_term :            C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖) ≤              (C₀ * A) * (‖s‖ * Real.log (1 + ‖s‖)) := by          -- use `hprod_w`          have := mul_le_mul_of_nonneg_left hprod_w hC0_nonneg          -- rearrange          simpa [mul_assoc, mul_left_comm, mul_comm] using this        have hlog2_term : Real.log 2 ≤ 1 * (‖s‖ * Real.log (1 + ‖s‖)) := by          simpa using hlog2_le_xlog        -- combine and expand `C = 1 + C₀*A`        nlinarith [hA_term, hlog2_term, C]      -- apply exp monotonicity      have h_exp :          Real.exp (Real.log 2 + C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖))            ≤ Real.exp (C * (‖s‖ * Real.log (1 + ‖s‖))) :=        Real.exp_le_exp.mpr hexp_le      -- rewrite the left-hand side using `htmp'`      have :          2 * Real.exp (C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖))            ≤ Real.exp (C * (‖s‖ * Real.log (1 + ‖s‖))) := by        calc          2 * Real.exp (C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖))              = Real.exp (Real.log 2 + C₀ * ‖s / 2 + 1‖ * Real.log (1 + ‖s / 2 + 1‖)) := htmp'          _ ≤ Real.exp (C * (‖s‖ * Real.log (1 + ‖s‖))) := h_exp      simpa [mul_assoc] using this)  -- final rewriting of the exponent  simpa [mul_assoc] using hmain