Complex.Gammaℝ.Stirling.finite_order

theorem finite_order :    ∃ (A B : ℝ), 0 < A ∧ 0 < B ∧      ∀ s : ℂ, 0 ≤ s.re → 1 ≤ ‖s‖ →        ‖Complex.Gammaℝ s‖ ≤ Real.exp (A * ‖s‖ ^ B) := by  obtain ⟨C, hC_pos, hC⟩ := bound_re_ge_zero  use C + 1, 2  refine ⟨by linarith, by norm_num, ?_⟩  intro s hs_re hs_norm  have h := hC s hs_re hs_norm  apply le_trans h  apply Real.exp_le_exp.mpr  -- log(1 + |s|) ≤ |s| for |s| ≥ 1, so C|s|log(1+|s|) ≤ C|s|² ≤ (C+1)|s|²  have h_log : Real.log (1 + ‖s‖) ≤ ‖s‖ := by    have h1 : 0 < 1 + ‖s‖ := by linarith [norm_nonneg s]    have h2 : ‖s‖ + 1 ≤ Real.exp ‖s‖ := Real.add_one_le_exp ‖s‖    have h2' : 1 + ‖s‖ ≤ Real.exp ‖s‖ := by linarith    rw [Real.log_le_iff_le_exp (by linarith [norm_nonneg s])]    exact h2'  have step1 : C * ‖s‖ * Real.log (1 + ‖s‖) ≤ C * ‖s‖ * ‖s‖ := by    apply mul_le_mul_of_nonneg_left h_log    apply mul_nonneg (by linarith) (norm_nonneg s)  have step2 : C * ‖s‖ * ‖s‖ = C * ‖s‖ ^ 2 := by ring  have step3 : C * ‖s‖ ^ 2 ≤ (C + 1) * ‖s‖ ^ 2 := by    apply mul_le_mul_of_nonneg_right (by linarith) (sq_nonneg _)  have h_combined : C * ‖s‖ * Real.log (1 + ‖s‖) ≤ (C + 1) * ‖s‖ ^ 2 := by    calc C * ‖s‖ * Real.log (1 + ‖s‖)        ≤ C * ‖s‖ * ‖s‖ := step1      _ = C * ‖s‖ ^ 2 := step2      _ ≤ (C + 1) * ‖s‖ ^ 2 := step3  -- Convert from ℕ exponent (^ 2) to ℝ exponent (^ (2 : ℝ))  -- The goal is (C + 1) * ‖s‖ ^ (2 : ℝ), which equals (C + 1) * ‖s‖ ^ (2 : ℕ)  -- This type coercion is handled by norm_cast  have hconv : (C + 1) * ‖s‖ ^ 2 = (C + 1) * ‖s‖ ^ (2 : ℝ) := by norm_cast  rw [← hconv]  exact h_combined