Commit 2023-06-05 08:24 a3209ddf

View on Github →

feat (special_functions/gamma): doubling formula (#19136) This PR adds the proof of the Legendre doubling formula, relating Gamma s * Gamma (s + 1 / 2) to Gamma (2 * s).

Estimated changes

Modified src/analysis/analytic/isolated_zeros.lean

added theorem analytic_on.eq_of_frequently_eq

Modified src/analysis/analytic/uniqueness.lean

added theorem analytic_on.eq_of_eventually_eq

Modified src/analysis/special_functions/gamma/beta.lean

added theorem complex.Gamma_mul_Gamma_add_half

added theorem real.Gamma_mul_Gamma_add_half

Modified src/analysis/special_functions/gamma/bohr_mollerup.lean

added theorem concave_on.add_const

added theorem concave_on.congr

added theorem convex_on.add_const

added theorem convex_on.congr

added theorem real.Gamma_mul_Gamma_add_half_of_pos

added def real.doubling_Gamma

added theorem real.doubling_Gamma_add_one

added theorem real.doubling_Gamma_eq_Gamma

added theorem real.doubling_Gamma_log_convex_Ioi

added theorem real.doubling_Gamma_one

added theorem real.log_doubling_Gamma_eq

added theorem strict_concave_on.add_const

added theorem strict_concave_on.congr

added theorem strict_convex_on.add_const

added theorem strict_convex_on.congr