FKS.remark_2_6_a

@[blueprint  "fks-remark-2-6-a"  (title := "FKS Remark 2-6-a")  (statement := /-- $\Gamma(3,x) = (x^2 + 2(x+1)) e^{-x}$. -/)]theorem remark_2_6_a (x : ℝ) (hx : 0 ≤ x) :    Gamma.incomplete 3 x = (x ^ 2 + 2 * (x + 1)) * exp (-x) := by  have integrableOn_Ioi (s : ℝ) {a : ℝ} (hs : 0 < s) (ha : 0 ≤ a) :      IntegrableOn (fun t ↦ exp (-t) * t ^ (s - 1)) (Set.Ioi a) :=    (GammaIntegral_convergent hs).mono_set (Set.Ioi_subset_Ioi ha)  have recurrence (s : ℝ) (hs : 0 < s) {y : ℝ} (hy : 0 ≤ y) :      Gamma.incomplete (s + 1) y = y ^ s * exp (-y) + s * Gamma.incomplete s y := by    unfold Gamma.incomplete    conv_lhs => arg 2; intro t; rw [mul_comm]    norm_num    rw [integral_Ioi_mul_deriv_eq_deriv_mul (u := fun t ↦ t ^ s) (v := fun t ↦ -exp (-t))        (u' := fun t ↦ s * t ^ (s - 1)) (v' := fun t ↦ exp (-t))        (a' := -y ^ s * exp (-y)) (b' := 0)]    · ring_nf      simp [sub_eq_add_neg, integral_neg, ← integral_const_mul, mul_assoc, mul_comm]    · exact fun t ht ↦ hasDerivAt_rpow_const (by grind)    · exact fun t _ ↦ by convert! (hasDerivAt_neg t).exp.neg using 1; norm_num    · simpa [mul_comm] using! integrableOn_Ioi (s + 1) (by grind) (by grind : 0 ≤ y)    · refine ((integrableOn_Ioi s hs hy).const_mul (-s)).congr ?_      filter_upwards [ae_restrict_mem measurableSet_Ioi] with t _; norm_num; ring    · convert Filter.Tendsto.mul        (Filter.Tendsto.rpow (Filter.tendsto_id.mono_left inf_le_left) tendsto_const_nhds _)        (Filter.Tendsto.neg (continuous_exp.continuousAt.tendsto.comp          (Filter.Tendsto.neg (Filter.tendsto_id.mono_left inf_le_left)))) using 1 <;> aesop    · have h_lim : Filter.Tendsto (fun t : ℝ ↦ t ^ s * exp (-t)) Filter.atTop (nhds 0) := by        apply squeeze_zero_norm' _ (tendsto_pow_mul_exp_neg_atTop_nhds_zero ⌈s⌉₊)        filter_upwards [Filter.eventually_gt_atTop 1] with t ht        rw [norm_of_nonneg (by positivity)]        exact mul_le_mul_of_nonneg_right          (by simpa using rpow_le_rpow_of_exponent_le ht.le <| Nat.le_ceil s) (by positivity)      convert h_lim.neg using 2 <;> norm_num  rw [show (3 : ℝ) = 2 + 1 by norm_num, recurrence 2 (by norm_num) hx,      show (2 : ℝ) = 1 + 1 by norm_num, recurrence 1 (by norm_num) hx]  norm_num [Gamma.incomplete, integral_exp_neg_Ioi x]; ring