Commit 2022-06-07 21:09 905374c4

View on Github →

feat(special_functions/gamma): better convergence bounds (#14496) Use the stronger form of FTC-2 added #14147 to strengthen some results about the gamma function.

Estimated changes

Modified src/analysis/special_functions/gamma.lean

modified def complex.Gamma

modified theorem complex.Gamma_aux_recurrence1

modified theorem complex.Gamma_aux_recurrence2

modified theorem complex.Gamma_eq_Gamma_aux

modified theorem complex.Gamma_eq_integral

modified theorem complex.Gamma_integral_add_one

modified theorem complex.Gamma_integral_convergent

modified theorem complex.partial_Gamma_add_one

modified theorem complex.tendsto_partial_Gamma

modified theorem real.Gamma_integral_convergent