Complex.Gamma.norm_le_one_div_add_sqrt_pi_of_re_ge_of_re_le

lemma norm_le_one_div_add_sqrt_pi_of_re_ge_of_re_le {w : ℂ} {a : ℝ}    (ha_pos : 0 < a) (hw : a ≤ w.re) (hw_ub : w.re ≤ 1) :    ‖Complex.Gamma w‖ ≤ 1 / a + Real.sqrt Real.pi := by  set f : ℝ → ℂ := fun t ↦ Complex.exp (-t) * t ^ (w - 1)  set g : ℝ → ℝ := fun t ↦ Real.exp (-t) * t ^ (w.re - 1)  have hw_pos : 0 < w.re := ha_pos.trans_le hw  have hΓ : Complex.Gamma w = ∫ t in Ioi (0 : ℝ), f t := by    rw [Complex.Gamma_eq_integral hw_pos]    simp [Complex.GammaIntegral, f]  have h_norm :      ‖Complex.Gamma w‖ =        ‖∫ t in Ioi (0 : ℝ), f t‖ := by    simp [hΓ]  have h_le_int :      ‖∫ t in Ioi (0 : ℝ), f t‖        ≤ ∫ t in Ioi (0 : ℝ), ‖f t‖ :=    MeasureTheory.norm_integral_le_integral_norm _  have h_int_real :      ∫ t in Ioi (0 : ℝ), ‖f t‖        = ∫ t in Ioi (0 : ℝ), g t := by    refine MeasureTheory.setIntegral_congr_fun measurableSet_Ioi ?_    intro t ht    simp [f, g, Complex.norm_exp, Complex.norm_cpow_eq_rpow_re_of_pos ht (w - 1)]  have h_split :      (∫ t in Ioi (0 : ℝ), g t)        = (∫ t in Ioc 0 1, g t) + (∫ t in Ioi 1, g t) := by    have hIoc : IntegrableOn g (Ioc 0 1) :=      (Real.GammaIntegral_convergent hw_pos).mono_set Ioc_subset_Ioi_self    have hIoi : IntegrableOn g (Ioi 1) :=      (Real.GammaIntegral_convergent hw_pos).mono_set        (fun t ht => mem_Ioi.mpr (lt_trans zero_lt_one (mem_Ioi.mp ht)))    simpa [Ioc_union_Ioi_eq_Ioi zero_le_one] using      (MeasureTheory.setIntegral_union          (Ioc_disjoint_Ioi_same (a := 0) (b := 1))          measurableSet_Ioi hIoc hIoi)  have h_ae_drop :      (fun t : ℝ ↦ g t) ≤ᵐ[volume.restrict (Ioc 0 1)]        (fun t : ℝ ↦ t ^ (w.re - 1)) := by    refine (ae_restrict_iff' measurableSet_Ioc).2 (Filter.Eventually.of_forall ?_)    intro t ht    have h_exp : Real.exp (-t) ≤ 1 := by      have : (-t : ℝ) ≤ 0 := by linarith [ht.1]      exact exp_le_one_iff.mpr this    have h_nonneg : (0 : ℝ) ≤ t ^ (w.re - 1) :=      Real.rpow_nonneg (le_of_lt ht.1) _    simpa [g] using mul_le_of_le_one_left h_nonneg h_exp  have hIoc₁ : IntegrableOn g (Ioc 0 1) :=    (Real.GammaIntegral_convergent hw_pos).mono_set Ioc_subset_Ioi_self  have hIoc₂ : IntegrableOn (fun t : ℝ ↦ t ^ (w.re - 1)) (Ioc 0 1) := by    have hInt :        IntervalIntegrable (fun t : ℝ ↦ t ^ (w.re - 1)) volume 0 1 := by      simpa using        intervalIntegral.intervalIntegrable_rpow' (by linarith : -1 < w.re - 1)    simpa using      (intervalIntegrable_iff_integrableOn_Ioc_of_le          (a := 0) (b := 1) zero_le_one).1 hInt  have h_drop_exp :      (∫ t in Ioc 0 1, g t)        ≤ ∫ t in Ioc 0 1, t ^ (w.re - 1) :=    MeasureTheory.setIntegral_mono_ae_restrict hIoc₁ hIoc₂ h_ae_drop  have h_big :      ‖Complex.Gamma w‖        ≤ (∫ t in Ioc 0 1, t ^ (w.re - 1)) + (∫ t in Ioi 1, g t) := by    have step1 : ‖∫ t in Ioi (0 : ℝ), f t‖        ≤ (∫ t in Ioc 0 1, g t) + (∫ t in Ioi 1, g t) := by      simpa [h_int_real, h_split] using h_le_int    have step2 : (∫ t in Ioc 0 1, g t) + (∫ t in Ioi 1, g t)        ≤ (∫ t in Ioc 0 1, t ^ (w.re - 1)) + (∫ t in Ioi 1, g t) :=      add_le_add_left h_drop_exp _    simpa [h_norm] using (le_trans step1 step2)  have h_Ioc_exact :      ∫ t in Ioc 0 1, t ^ (w.re - 1) = 1 / w.re :=    integral_rpow_Ioc_zero_one hw_pos  have h_tail :      ∫ t in Ioi 1, g t ≤ Real.sqrt Real.pi := by    by_cases hhalf : (1 / 2 : ℝ) ≤ w.re    · have := integral_exp_neg_rpow_Ioi_one_le hhalf hw_ub      simpa [g] using this    · have h_ae :          (fun t : ℝ ↦ g t) ≤ᵐ[volume.restrict (Ioi 1)]            (fun t : ℝ ↦ Real.exp (-t) * t ^ ((1 / 2 : ℝ) - 1)) := by        refine (ae_restrict_iff' measurableSet_Ioi).2 (Filter.Eventually.of_forall ?_)        intro t ht        have ht1 : (1 : ℝ) ≤ t := le_of_lt ht        have hpow : t ^ (w.re - 1) ≤ t ^ ((1 / 2 : ℝ) - 1) := by          have : w.re - 1 ≤ (1 / 2 : ℝ) - 1 := by linarith [hhalf]          exact Real.rpow_le_rpow_of_exponent_le ht1 this        have hnonneg : (0 : ℝ) ≤ Real.exp (-t) := (Real.exp_pos _).le        simpa [g] using mul_le_mul_of_nonneg_left hpow hnonneg      have hIntL : IntegrableOn g (Ioi 1) :=        (Real.GammaIntegral_convergent hw_pos).mono_set          (fun x hx => mem_Ioi.mpr (lt_trans zero_lt_one (mem_Ioi.mp hx)))      have hIntR : IntegrableOn            (fun t : ℝ ↦ Real.exp (-t) * t ^ ((1 / 2 : ℝ) - 1)) (Ioi 1) :=        (Real.GammaIntegral_convergent (by norm_num : 0 < (1 / 2 : ℝ))).mono_set          (fun x hx => mem_Ioi.mpr (lt_trans zero_lt_one (mem_Ioi.mp hx)))      have h_le : ∫ t in Ioi 1, g t            ≤ ∫ t in Ioi 1, Real.exp (-t) * t ^ ((1 / 2 : ℝ) - 1) :=        MeasureTheory.setIntegral_mono_ae_restrict hIntL hIntR h_ae      have h_upper :          ∫ t in Ioi 1, Real.exp (-t) * t ^ ((1 / 2 : ℝ) - 1)            ≤ Real.sqrt Real.pi := by        have := integral_exp_neg_rpow_Ioi_one_le                  (by norm_num : (1 / 2 : ℝ) ≤ 1 / 2)                  (by norm_num : (1 / 2 : ℝ) ≤ (1 : ℝ))        simpa using this      exact h_le.trans h_upper  have h_main :      ‖Complex.Gamma w‖ ≤ 1 / w.re + Real.sqrt Real.pi := by    calc      ‖Complex.Gamma w‖          ≤ (∫ t in Ioc 0 1, t ^ (w.re - 1)) + (∫ t in Ioi 1, g t) := h_big      _ = 1 / w.re + (∫ t in Ioi 1, g t) := by rw [h_Ioc_exact]      _ ≤ 1 / w.re + Real.sqrt Real.pi := by exact add_le_add_right h_tail _  have h_one_div : (1 / w.re : ℝ) ≤ 1 / a :=    one_div_le_one_div_of_le ha_pos hw  have : 1 / w.re + Real.sqrt Real.pi ≤ 1 / a + Real.sqrt Real.pi :=    add_le_add_left h_one_div _  exact h_main.trans this