English
Recurrence: partialGamma(s+1,X) = s partialGamma(s,X) − e^{−X} X^s.
Русский
Рекуррентное соотношение: partialGamma(s+1,X) = s · partialGamma(s,X) − e^{−X} X^s.
LaTeX
$$$$ \text{partialGamma}(s+1,X) = s \cdot \text{partialGamma}(s,X) - e^{-X} X^{s}. $$$$
Lean4
/-- The recurrence relation for the indefinite version of the `Γ` function. -/
theorem partialGamma_add_one {s : ℂ} (hs : 0 < s.re) {X : ℝ} (hX : 0 ≤ X) :
partialGamma (s + 1) X = s * partialGamma s X - (-X).exp * X ^ s :=
by
rw [partialGamma, partialGamma, add_sub_cancel_right]
have F_der_I :
∀ x : ℝ,
x ∈ Ioo 0 X →
HasDerivAt (fun x => (-x).exp * x ^ s : ℝ → ℂ) (-((-x).exp * x ^ s) + (-x).exp * (s * x ^ (s - 1))) x :=
by
intro x hx
have d1 : HasDerivAt (fun y : ℝ => (-y).exp) (-(-x).exp) x := by simpa using (hasDerivAt_neg x).exp
have d2 : HasDerivAt (fun y : ℝ => (y : ℂ) ^ s) (s * x ^ (s - 1)) x :=
by
have t := @HasDerivAt.cpow_const _ _ _ s (hasDerivAt_id ↑x) ?_
· simpa only [mul_one] using t.comp_ofReal
· exact ofReal_mem_slitPlane.2 hx.1
simpa only [ofReal_neg, neg_mul] using d1.ofReal_comp.mul d2
have cont := (continuous_ofReal.comp continuous_neg.rexp).mul (continuous_ofReal_cpow_const hs)
have der_ible := (Gamma_integrand_deriv_integrable_A hs hX).add (Gamma_integrand_deriv_integrable_B hs hX)
have int_eval := integral_eq_sub_of_hasDerivAt_of_le hX cont.continuousOn F_der_I der_ible
apply_fun fun x : ℂ => -x at int_eval
rw [intervalIntegral.integral_add (Gamma_integrand_deriv_integrable_A hs hX)
(Gamma_integrand_deriv_integrable_B hs hX),
intervalIntegral.integral_neg, neg_add, neg_neg] at int_eval
rw [eq_sub_of_add_eq int_eval, sub_neg_eq_add, neg_sub, add_comm, add_sub]
have : (fun x => (-x).exp * (s * x ^ (s - 1)) : ℝ → ℂ) = (fun x => s * (-x).exp * x ^ (s - 1) : ℝ → ℂ) := by ext1;
ring
rw [this]
rw [← intervalIntegral.integral_const_mul, ofReal_zero, zero_cpow]
· rw [mul_zero, add_zero]; congr 2; ext1; ring
· contrapose! hs; rw [hs, zero_re]
