English
For all s ∈ ℂ, Gamma(s) Gamma(s+1/2) = Gamma(2s) 2^{1−2s} √π.
Русский
Для всех s ∈ ℂ: Γ(s) Γ(s+1/2) = Γ(2s) 2^{1−2s} √π.
LaTeX
$$$$ \Gamma(s) \Gamma\left(s + \tfrac{1}{2}\right) = \Gamma(2s) \; 2^{1-2s} \; \sqrt{\pi}. $$$$
Lean4
theorem Gamma_mul_Gamma_add_half (s : ℂ) :
Gamma s * Gamma (s + 1 / 2) = Gamma (2 * s) * (2 : ℂ) ^ (1 - 2 * s) * ↑(√π) :=
by
suffices (fun z => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) = fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π)
by
convert congr_arg Inv.inv (congr_fun this s) using 1
· rw [mul_inv, inv_inv, inv_inv]
· rw [div_eq_mul_inv, mul_inv, mul_inv, inv_inv, inv_inv, ← cpow_neg, neg_sub]
have h1 : AnalyticOnNhd ℂ (fun z : ℂ => (Gamma z)⁻¹ * (Gamma (z + 1 / 2))⁻¹) univ :=
by
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
refine (differentiable_one_div_Gamma.mul ?_).differentiableOn
exact differentiable_one_div_Gamma.comp (differentiable_id.add (differentiable_const _))
have h2 : AnalyticOnNhd ℂ (fun z => (Gamma (2 * z))⁻¹ * (2 : ℂ) ^ (2 * z - 1) / ↑(√π)) univ :=
by
refine DifferentiableOn.analyticOnNhd ?_ isOpen_univ
refine (Differentiable.mul ?_ (differentiable_const _)).differentiableOn
apply Differentiable.mul
· exact differentiable_one_div_Gamma.comp (differentiable_id.const_mul _)
· refine fun t => DifferentiableAt.const_cpow ?_ (Or.inl two_ne_zero)
exact DifferentiableAt.sub_const (differentiableAt_id.const_mul _) _
have h3 : Tendsto ((↑) : ℝ → ℂ) (𝓝[≠] 1) (𝓝[≠] 1) :=
by
rw [tendsto_nhdsWithin_iff]; constructor
· exact tendsto_nhdsWithin_of_tendsto_nhds continuous_ofReal.continuousAt
· exact eventually_nhdsWithin_iff.mpr (Eventually.of_forall fun t ht => ofReal_ne_one.mpr ht)
refine AnalyticOnNhd.eq_of_frequently_eq h1 h2 (h3.frequently ?_)
refine ((Eventually.filter_mono nhdsWithin_le_nhds) ?_).frequently
refine (eventually_gt_nhds zero_lt_one).mp (Eventually.of_forall fun t ht => ?_)
rw [← mul_inv, Gamma_ofReal, (by simp : (t : ℂ) + 1 / 2 = ↑(t + 1 / 2)), Gamma_ofReal, ← ofReal_mul,
Gamma_mul_Gamma_add_half_of_pos ht, ofReal_mul, ofReal_mul, ← Gamma_ofReal, mul_inv, mul_inv,
(by simp : 2 * (t : ℂ) = ↑(2 * t)), Gamma_ofReal, ofReal_cpow zero_le_two, show (2 : ℝ) = (2 : ℂ) by norm_cast, ←
cpow_neg, ofReal_sub, ofReal_one, neg_sub, ← div_eq_mul_inv]
