Complex.Gamma.stirling_bound_re_ge_zero

theorem stirling_bound_re_ge_zero :    ∃ C : ℝ, 0 < C ∧      ∀ s : ℂ, 0 ≤ s.re → 1 ≤ ‖s‖ →        ‖Gamma s‖ ≤ Real.exp (C * ‖s‖ * Real.log (1 + ‖s‖)) := by  classical  rcases norm_bound_re_ge_one with ⟨C₁, hC₁_pos, hC₁⟩  have hlog2_pos : 0 < Real.log 2 := by    have : (1 : ℝ) < 2 := by norm_num    exact Real.log_pos this  have hlog2_ne : Real.log 2 ≠ 0 := ne_of_gt hlog2_pos  let K : ℝ := |Real.log C₁| + 1  have hK_pos : 0 < K := by    have : 0 ≤ |Real.log C₁| := abs_nonneg _    linarith [K]  have hC₁_exp : C₁ ≤ Real.exp K := by    have hlog : Real.log C₁ ≤ |Real.log C₁| + 1 := by      have : Real.log C₁ ≤ |Real.log C₁| := le_abs_self _      linarith    have h := Real.exp_le_exp.mpr hlog    simpa [K, Real.exp_log hC₁_pos] using h  let Cbase : ℝ := K / Real.log 2 + 2  have hCbase_pos : 0 < Cbase := by    have hK_div_nonneg : 0 ≤ K / Real.log 2 := div_nonneg hK_pos.le hlog2_pos.le    linarith [Cbase, hK_div_nonneg]  let C : ℝ := 4 * Cbase  refine ⟨C, by nlinarith [hCbase_pos], ?_⟩  have h_re_ge_one :      ∀ z : ℂ, 1 ≤ z.re →        ‖Gamma z‖ ≤ Real.exp (Cbase * ‖z‖ * Real.log (1 + ‖z‖)) := by    intro z hz_re    have hz_norm : (1 : ℝ) ≤ ‖z‖ := le_trans hz_re (Complex.re_le_norm z)    have hx_pos : 0 < (1 + ‖z‖ : ℝ) := by linarith [norm_nonneg z]    have hL_nonneg : 0 ≤ Real.log (1 + ‖z‖) := Real.log_nonneg (by linarith [norm_nonneg z])    have hlog2_le_log : Real.log 2 ≤ Real.log (1 + ‖z‖) :=      Real.Stirling.log_one_add_ge_log_two hz_norm    have hlog2_le : Real.log 2 ≤ ‖z‖ * Real.log (1 + ‖z‖) := by      have hx_mul : ‖z‖ * Real.log 2 ≤ ‖z‖ * Real.log (1 + ‖z‖) :=        mul_le_mul_of_nonneg_left hlog2_le_log (by linarith)      have hx_ge : Real.log 2 ≤ ‖z‖ * Real.log 2 := by        have := mul_le_mul_of_nonneg_right hz_norm hlog2_pos.le        simpa [one_mul] using this      exact le_trans hx_ge hx_mul    have hcoef_nonneg : 0 ≤ K / Real.log 2 := div_nonneg hK_pos.le hlog2_pos.le    have hscaled :        (K / Real.log 2) * Real.log 2 ≤ (K / Real.log 2) * (‖z‖ * Real.log (1 + ‖z‖)) :=      mul_le_mul_of_nonneg_left hlog2_le hcoef_nonneg    have hK_le : K ≤ (K / Real.log 2) * (‖z‖ * Real.log (1 + ‖z‖)) := by      have : (K / Real.log 2) * Real.log 2 = K := by field_simp [hlog2_ne]      simpa [this] using hscaled    have hlin :        Real.log (1 + ‖z‖) * (‖z‖ + 1) ≤          2 * (‖z‖ * Real.log (1 + ‖z‖)) := by      have hz_le : ‖z‖ + 1 ≤ 2 * ‖z‖ := by linarith [hz_norm]      have hmul :          Real.log (1 + ‖z‖) * (‖z‖ + 1) ≤            Real.log (1 + ‖z‖) * (2 * ‖z‖) :=        mul_le_mul_of_nonneg_left hz_le hL_nonneg      -- rewrite      simpa [mul_assoc, mul_left_comm, mul_comm, two_mul] using hmul    -- Convert the polynomial bound into an exponential bound.    have hpoly : ‖Gamma z‖ ≤ C₁ * (1 + ‖z‖) ^ (‖z‖ + 1) := hC₁ z hz_re    have hnonneg_rpow : 0 ≤ (1 + ‖z‖) ^ (‖z‖ + 1) :=      Real.rpow_nonneg (by linarith [norm_nonneg z]) _    have hmul :        C₁ * (1 + ‖z‖) ^ (‖z‖ + 1) ≤          Real.exp K * (1 + ‖z‖) ^ (‖z‖ + 1) :=      mul_le_mul_of_nonneg_right hC₁_exp hnonneg_rpow    have hrpow :        (1 + ‖z‖) ^ (‖z‖ + 1) =          Real.exp (Real.log (1 + ‖z‖) * (‖z‖ + 1)) := by      simp [Real.rpow_def_of_pos hx_pos, mul_comm]    have hexp1 :        C₁ * (1 + ‖z‖) ^ (‖z‖ + 1) ≤          Real.exp (K + Real.log (1 + ‖z‖) * (‖z‖ + 1)) := by      calc        C₁ * (1 + ‖z‖) ^ (‖z‖ + 1)            ≤ Real.exp K * (1 + ‖z‖) ^ (‖z‖ + 1) := hmul        _ = Real.exp K * Real.exp (Real.log (1 + ‖z‖) * (‖z‖ + 1)) := by simp [hrpow]        _ = Real.exp (K + Real.log (1 + ‖z‖) * (‖z‖ + 1)) := by              simp [Real.exp_add]    have hexp2 :        Real.exp (K + Real.log (1 + ‖z‖) * (‖z‖ + 1))          ≤ Real.exp (Cbase * (‖z‖ * Real.log (1 + ‖z‖))) := by      apply Real.exp_le_exp.mpr      have hsum :          K + Real.log (1 + ‖z‖) * (‖z‖ + 1)            ≤ (K / Real.log 2 + 2) * (‖z‖ * Real.log (1 + ‖z‖)) := by        -- split into the constant term and the rpow term        have hK_term : K ≤ (K / Real.log 2) * (‖z‖ * Real.log (1 + ‖z‖)) := by          -- `‖z‖ * log(1+‖z‖)` is ≥ log 2, so we can scale          -- (we already proved it with `hK_le`, but written with `‖z‖*log` instead of `log*‖z‖`)          simpa [mul_assoc] using hK_le        have h2_term :            Real.log (1 + ‖z‖) * (‖z‖ + 1) ≤ 2 * (‖z‖ * Real.log (1 + ‖z‖)) := hlin        -- combine        have :            K + Real.log (1 + ‖z‖) * (‖z‖ + 1) ≤              (K / Real.log 2) * (‖z‖ * Real.log (1 + ‖z‖)) +                2 * (‖z‖ * Real.log (1 + ‖z‖)) := by          nlinarith [hK_term, h2_term]        -- factor        simpa [Cbase, add_mul, mul_add, two_mul, mul_assoc, mul_left_comm, mul_comm] using this      simpa [Cbase, mul_assoc] using hsum    have hexp3 :        Real.exp (Cbase * (‖z‖ * Real.log (1 + ‖z‖)))          = Real.exp (Cbase * ‖z‖ * Real.log (1 + ‖z‖)) := by ring_nf    have : ‖Gamma z‖ ≤ Real.exp (Cbase * ‖z‖ * Real.log (1 + ‖z‖)) :=      le_trans hpoly (le_trans hexp1 (le_trans hexp2 (by simp [hexp3] )))    simpa [mul_assoc] using this  intro s hs_re hs_norm  have hs0 : s ≠ 0 := (norm_pos_iff).1 (lt_of_lt_of_le (by norm_num) hs_norm)  by_cases hs_ge_one : 1 ≤ s.re  · have h1 := h_re_ge_one s hs_ge_one    -- upgrade from `Cbase` to `C = 4*Cbase`    have hmul_nonneg : 0 ≤ ‖s‖ * Real.log (1 + ‖s‖) := by      have : 0 ≤ Real.log (1 + ‖s‖) := Real.log_nonneg (by linarith [norm_nonneg s])      exact mul_nonneg (norm_nonneg _) this    have hC_le : Cbase * (‖s‖ * Real.log (1 + ‖s‖)) ≤ C * (‖s‖ * Real.log (1 + ‖s‖)) := by      have : Cbase ≤ C := by simp [C, le_mul_of_one_le_left, hCbase_pos.le]      exact mul_le_mul_of_nonneg_right this hmul_nonneg    have h2 : Real.exp (Cbase * ‖s‖ * Real.log (1 + ‖s‖))        ≤ Real.exp (C * ‖s‖ * Real.log (1 + ‖s‖)) := by      apply Real.exp_le_exp.mpr      -- rewrite to use `hC_le`      have hleft : Cbase * ‖s‖ * Real.log (1 + ‖s‖) = Cbase * (‖s‖ * Real.log (1 + ‖s‖)) := by ring      have hright : C * ‖s‖ * Real.log (1 + ‖s‖) = C * (‖s‖ * Real.log (1 + ‖s‖)) := by ring      -- `simp` both sides      simpa [hleft, hright] using hC_le    exact le_trans h1 h2  · have hs_lt_one : s.re < 1 := lt_of_not_ge hs_ge_one    -- relate `Γ(s)` to `Γ(s+1)` and bound using the `re≥1` case.    have hnorm_eq : ‖Gamma s‖ = ‖Gamma (s + 1)‖ / ‖s‖ := by      have h := Complex.Gamma_add_one s hs0      have hn : ‖Gamma (s + 1)‖ = ‖s‖ * ‖Gamma s‖ := by        calc          ‖Gamma (s + 1)‖ = ‖s * Gamma s‖ := by simp [h]          _ = ‖s‖ * ‖Gamma s‖ := by simp      have hs_norm_ne : ‖s‖ ≠ 0 := (norm_ne_zero_iff).2 hs0      calc        ‖Gamma s‖ = (‖s‖ * ‖Gamma s‖) / ‖s‖ := by field_simp [hs_norm_ne]        _ = ‖Gamma (s + 1)‖ / ‖s‖ := by simp [hn]    have hdiv : ‖Gamma s‖ ≤ ‖Gamma (s + 1)‖ := by      rw [hnorm_eq]      exact div_le_self (norm_nonneg _) hs_norm    have hs1 : (1 : ℝ) ≤ (s + 1).re := by      -- `re(s+1) = re(s)+1`      simp [Complex.add_re]      linarith [hs_re]    have hG1 : ‖Gamma (s + 1)‖ ≤ Real.exp (C * ‖s‖ * Real.log (1 + ‖s‖)) := by      have h0 := h_re_ge_one (s + 1) hs1      have hshift := norm_mul_log_shift_add_one_bound hs_norm      have hC_nonneg : 0 ≤ Cbase := le_of_lt hCbase_pos      have hCshift :          Cbase * (‖s + 1‖ * Real.log (1 + ‖s + 1‖)) ≤ C * (‖s‖ * Real.log (1 + ‖s‖)) := by        calc          Cbase * (‖s + 1‖ * Real.log (1 + ‖s + 1‖))              ≤ Cbase * (4 * (‖s‖ * Real.log (1 + ‖s‖))) := by                    exact mul_le_mul_of_nonneg_left hshift hC_nonneg          _ = C * (‖s‖ * Real.log (1 + ‖s‖)) := by simp [C, mul_assoc, mul_left_comm, mul_comm]      have h0' :          Cbase * ‖s + 1‖ * Real.log (1 + ‖s + 1‖) =            Cbase * (‖s + 1‖ * Real.log (1 + ‖s + 1‖)) := by        ring      have h1' :          C * ‖s‖ * Real.log (1 + ‖s‖) =            C * (‖s‖ * Real.log (1 + ‖s‖)) := by        ring      exact le_trans h0 (by        apply Real.exp_le_exp.mpr        simpa [h0', h1'] using hCshift)    exact le_trans hdiv hG1