Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-25 08:04 f02c7844

View on Github →

feat(special_functions/gamma): recurrence relation for Gamma function (#13156)

Estimated changes

Modified src/analysis/special_functions/gamma.lean

added def complex.Gamma

added theorem complex.Gamma_add_one

added theorem complex.Gamma_aux_recurrence1

added theorem complex.Gamma_aux_recurrence2

added theorem complex.Gamma_eq_Gamma_aux

added theorem complex.Gamma_eq_integral

modified def complex.Gamma_integral

added theorem complex.Gamma_integral_add_one

added theorem complex.Gamma_nat_eq_factorial

added def complex.partial_Gamma

added theorem complex.partial_Gamma_add_one

added theorem complex.tendsto_partial_Gamma