English
Let s ∈ ℂ with Re(s) > 0 and n ∈ ℕ with n ≠ 0. Then GammaSeq(s,n) equals the complex integral from 0 to n of (1 − x/n)^n · x^{s−1}.
Русский
Пусть s ∈ ℂ с Re(s) > 0 и n ∈ ℕ, n ≠ 0. Тогда GammaSeq(s,n) равняется комплексному интегралу по [0, n] от (1 − x/n)^n · x^{s−1}.
LaTeX
$$$$ \GammaSeq(s,n) = \int_{0}^{n} \bigl(1 - \frac{x}{n}\bigr)^{n} \; x^{s-1} \, dx. $$$$
Lean4
theorem GammaSeq_eq_approx_Gamma_integral {s : ℂ} (hs : 0 < re s) {n : ℕ} (hn : n ≠ 0) :
GammaSeq s n = ∫ x : ℝ in 0..n, ↑((1 - x / n) ^ n) * (x : ℂ) ^ (s - 1) :=
by
have : ∀ x : ℝ, x = x / n * n := by intro x; rw [div_mul_cancel₀]; exact Nat.cast_ne_zero.mpr hn
conv_rhs => enter [1, x, 2, 1]; rw [this x]
rw [GammaSeq_eq_betaIntegral_of_re_pos hs]
have :=
intervalIntegral.integral_comp_div (a := 0) (b := n) (fun x => ↑((1 - x) ^ n) * ↑(x * ↑n) ^ (s - 1) : ℝ → ℂ)
(Nat.cast_ne_zero.mpr hn)
dsimp only at this
rw [betaIntegral, this, real_smul, zero_div, div_self, add_sub_cancel_right, ← intervalIntegral.integral_const_mul, ←
intervalIntegral.integral_const_mul]
swap; · exact Nat.cast_ne_zero.mpr hn
simp_rw [intervalIntegral.integral_of_le zero_le_one]
refine setIntegral_congr_fun measurableSet_Ioc fun x hx => ?_
push_cast
have hn' : (n : ℂ) ≠ 0 := Nat.cast_ne_zero.mpr hn
have A : (n : ℂ) ^ s = (n : ℂ) ^ (s - 1) * n :=
by
conv_lhs => rw [(by ring : s = s - 1 + 1), cpow_add _ _ hn']
simp
have B : ((x : ℂ) * ↑n) ^ (s - 1) = (x : ℂ) ^ (s - 1) * (n : ℂ) ^ (s - 1) := by
rw [← ofReal_natCast, mul_cpow_ofReal_nonneg hx.1.le (Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)).le]
rw [A, B, cpow_natCast]; ring
