Commit 2023-01-20 07:10 52e2fbbd

View on Github →

feat(special_functions/gamma): Bohr-Mollerup theorem (#18188) Add the characterisation of the Gamma function as the unique log-convex function with the correct functional equation.

Estimated changes

Modified src/analysis/special_functions/gamma.lean

modified theorem complex.Gamma_eq_integral

modified theorem complex.Gamma_nat_eq_factorial

added theorem complex.Gamma_one

added def real.Gamma

added theorem real.Gamma_add_one

added theorem real.Gamma_eq_integral

deleted def real.Gamma_integral

deleted theorem real.Gamma_integral_one

added theorem real.Gamma_mul_add_mul_le_rpow_Gamma_mul_rpow_Gamma

added theorem real.Gamma_nat_eq_factorial

added theorem real.Gamma_ne_zero

added theorem real.Gamma_one

added theorem real.Gamma_pos_of_pos

added theorem real.bohr_mollerup.f_add_nat_eq

added theorem real.bohr_mollerup.f_add_nat_ge

added theorem real.bohr_mollerup.f_add_nat_le

added theorem real.bohr_mollerup.f_nat_eq

added theorem real.bohr_mollerup.ge_log_gamma_seq

added theorem real.bohr_mollerup.le_log_gamma_seq

added theorem real.bohr_mollerup.log_gamma_seq_add_one

added theorem real.bohr_mollerup.tendsto_log_gamma_seq

added theorem real.bohr_mollerup.tendsto_log_gamma_seq_of_le_one

added theorem real.convex_on_log_Gamma

added theorem real.differentiable_at_Gamma

added theorem real.eq_Gamma_of_log_convex

added def real.log_gamma_seq

added theorem real.tendsto_log_Gamma

Modified src/analysis/special_functions/gaussian.lean

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

added theorem real.tendsto_log_comp_add_sub_log

added theorem real.tendsto_log_nat_add_one_sub_log

Modified src/data/real/conjugate_exponents.lean

added theorem real.is_conjugate_exponent_one_div