English
A variant form of the two-sub reflection relation: (Γℝ(2−s))^{-1} = Γℂ(s) sin(π s/2) (Γℝ(s+1))^{-1}.
Русский
Вариант второй формулы отражения: (Γℝ(2−s))^{-1} = Γℂ(s) sin(π s/2) (Γℝ(s+1))^{-1}.
LaTeX
$$$$ (\Gamma_{\mathbb{R}}(2 - s))^{-1} = \Gamma_{\mathbb{C}}(s) \sin\left(\frac{\pi s}{2}\right) \big( \Gamma_{\mathbb{R}}(s + 1)\big)^{-1}. $$$$
Lean4
/-- The derivative of the `Γ` integral, at any `s ∈ ℂ` with `1 < re s`, is given by the Mellin
transform of `log t * exp (-t)`. -/
theorem hasDerivAt_GammaIntegral {s : ℂ} (hs : 0 < s.re) :
HasDerivAt GammaIntegral (∫ t : ℝ in Ioi 0, t ^ (s - 1) * (Real.log t * Real.exp (-t))) s :=
by
rw [GammaIntegral_eq_mellin]
convert (mellin_hasDerivAt_of_isBigO_rpow (E := ℂ) _ _ (lt_add_one _) _ hs).2
· refine (Continuous.continuousOn ?_).locallyIntegrableOn measurableSet_Ioi
exact continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)
· rw [← isBigO_norm_left]
simp_rw [norm_real, isBigO_norm_left]
simpa only [neg_one_mul] using (isLittleO_exp_neg_mul_rpow_atTop zero_lt_one _).isBigO
· simp_rw [neg_zero, rpow_zero]
refine isBigO_const_of_tendsto (?_ : Tendsto _ _ (𝓝 (1 : ℂ))) one_ne_zero
rw [(by simp : (1 : ℂ) = Real.exp (-0))]
exact (continuous_ofReal.comp (Real.continuous_exp.comp continuous_neg)).continuousWithinAt
