Commit 2022-05-09 08:31 b38aee47

View on Github →

feat(analysis/special_functions): differentiability of Gamma function (#13000) Third instalment of my Gamma-function project (following #12917 and #13156). This PR adds the proof that the Gamma function is complex-analytic, away from the poles at non-positive integers.

Estimated changes

Modified src/analysis/special_functions/gamma.lean

added theorem complex.differentiable_at_Gamma

added theorem complex.differentiable_at_Gamma_aux

added theorem complex.has_deriv_at_Gamma_integral

added theorem dGamma_integral_abs_convergent

added def dGamma_integrand

added theorem dGamma_integrand_is_O_at_top

added def dGamma_integrand_real

added theorem loc_unif_bound_dGamma_integrand

modified theorem real.Gamma_integrand_is_O

Modified src/analysis/special_functions/log/basic.lean

added theorem real.abs_log_mul_self_lt

Modified src/analysis/special_functions/pow.lean

added theorem real.abs_log_mul_self_rpow_lt