English
For all z ∈ ℂ, Gamma(z) Gamma(1 − z) = π / sin(π z).
Русский
Для любого z ∈ ℂ выполняется Gamma(z) Gamma(1 − z) = π / sin(π z).
LaTeX
$$$$ \Gamma(z) \Gamma(1 - z) = \frac{\pi}{\sin(\pi z)}. $$$$
Lean4
/-- Euler's reflection formula for the complex Gamma function. -/
theorem Gamma_mul_Gamma_one_sub (z : ℂ) : Gamma z * Gamma (1 - z) = π / sin (π * z) :=
by
have pi_ne : (π : ℂ) ≠ 0 := Complex.ofReal_ne_zero.mpr pi_ne_zero
by_cases hs : sin (↑π * z) = 0
· -- first deal with silly case z = integer
rw [hs, div_zero]
rw [← neg_eq_zero, ← Complex.sin_neg, ← mul_neg, Complex.sin_eq_zero_iff, mul_comm] at hs
obtain ⟨k, hk⟩ := hs
rw [mul_eq_mul_right_iff, eq_false (ofReal_ne_zero.mpr pi_pos.ne'), or_false, neg_eq_iff_eq_neg] at hk
rw [hk]
cases k
· rw [Int.ofNat_eq_coe, Int.cast_natCast, Complex.Gamma_neg_nat_eq_zero, zero_mul]
·
rw [Int.cast_negSucc, neg_neg, Nat.cast_add, Nat.cast_one, add_comm, sub_add_cancel_left,
Complex.Gamma_neg_nat_eq_zero, mul_zero]
refine tendsto_nhds_unique ((GammaSeq_tendsto_Gamma z).mul (GammaSeq_tendsto_Gamma <| 1 - z)) ?_
have : ↑π / sin (↑π * z) = 1 * (π / sin (π * z)) := by rw [one_mul]
convert
Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => (GammaSeq_mul z hn).symm))
(Tendsto.mul _ _)
· convert tendsto_natCast_div_add_atTop (1 - z) using 1; ext1 n; rw [add_sub_assoc]
· have : ↑π / sin (↑π * z) = 1 / (sin (π * z) / π) := by simp
convert tendsto_const_nhds.div _ (div_ne_zero hs pi_ne)
rw [← tendsto_mul_iff_of_ne_zero tendsto_const_nhds pi_ne, div_mul_cancel₀ _ pi_ne]
convert tendsto_euler_sin_prod z using 1
ext1 n; rw [mul_comm, ← mul_assoc]
