English
For z ∈ ℂ and n ∈ ℕ, GammaSeq(z,n) · GammaSeq(1 − z,n) equals n/(n+1−z) times 1/( z ∏_{j=0}^{n-1} (1 − z^2/(j+1)^2) ).
Русский
Для z ∈ ℂ и n ∈ ℕ выражение GammaSeq(z,n) · GammaSeq(1 − z,n) равно n/(n+1−z) · 1/( z ∏_{j=0}^{n-1} (1 − z^2/(j+1)^2) ).
LaTeX
$$$$ \GammaSeq(z,n) \;\GammaSeq(1 - z,n) = \frac{n}{n+1 - z} \cdot \frac{1}{ z \prod_{j=0}^{n-1} \left(1 - \frac{z^2}{(j+1)^2}\right) }. $$$$
Lean4
theorem GammaSeq_mul (z : ℂ) {n : ℕ} (hn : n ≠ 0) :
GammaSeq z n * GammaSeq (1 - z) n =
n / (n + ↑1 - z) * (↑1 / (z * ∏ j ∈ Finset.range n, (↑1 - z ^ 2 / ((j : ℂ) + 1) ^ 2))) :=
by
-- also true for n = 0 but we don't need it
have aux : ∀ a b c d : ℂ, a * b * (c * d) = a * c * (b * d) := by intros; ring
rw [GammaSeq, GammaSeq, div_mul_div_comm, aux, ← pow_two]
have : (n : ℂ) ^ z * (n : ℂ) ^ (1 - z) = n := by
rw [← cpow_add _ _ (Nat.cast_ne_zero.mpr hn), add_sub_cancel, cpow_one]
rw [this, Finset.prod_range_succ', Finset.prod_range_succ, aux, ← Finset.prod_mul_distrib, Nat.cast_zero, add_zero,
add_comm (1 - z) n, ← add_sub_assoc]
have : ∀ j : ℕ, (z + ↑(j + 1)) * (↑1 - z + ↑j) = ((j + 1) ^ 2 :) * (↑1 - z ^ 2 / ((j : ℂ) + 1) ^ 2) :=
by
intro j
push_cast
have : (j : ℂ) + 1 ≠ 0 := by rw [← Nat.cast_succ, Nat.cast_ne_zero]; exact Nat.succ_ne_zero j
field_simp; ring
simp_rw [this]
rw [Finset.prod_mul_distrib, ← Nat.cast_prod, Finset.prod_pow, Finset.prod_range_add_one_eq_factorial, Nat.cast_pow,
(by intros; ring : ∀ a b c d : ℂ, a * b * (c * d) = a * (d * (b * c))), ← div_div, mul_div_cancel_right₀, ← div_div,
mul_comm z _, mul_one_div]
exact pow_ne_zero 2 (Nat.cast_ne_zero.mpr <| by positivity)
