Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-15 07:25 372edc36

View on Github →

feat (analysis/special_functions): limit formula and reflection formula for Gamma (#18404) This adds Euler's limit formula and the reflection formula for the Gamma function. As a consequence we get that Gamma does not vanish on the complex plane (except at non-positive integers, where it is undefined, and we have arbitrarily chosen it to be 0).

Estimated changes

Modified src/analysis/normed/field/basic.lean

Modified src/analysis/special_functions/gamma.lean

added theorem complex.Gamma_eq_zero_iff

added theorem complex.Gamma_mul_Gamma_one_sub

added theorem complex.Gamma_ne_zero

added theorem complex.Gamma_neg_nat_eq_zero

added theorem complex.Gamma_seq_add_one_left

added theorem complex.Gamma_seq_eq_approx_Gamma_integral

added theorem complex.Gamma_seq_eq_beta_integral_of_re_pos

added theorem complex.Gamma_seq_mul

added theorem complex.Gamma_seq_tendsto_Gamma

added theorem complex.Gamma_zero

added theorem complex.approx_Gamma_integral_tendsto_Gamma_integral

modified theorem complex.differentiable_at_Gamma

modified theorem complex.differentiable_at_Gamma_aux

added theorem real.Gamma_eq_zero_iff

added theorem real.Gamma_mul_Gamma_one_sub

modified theorem real.Gamma_ne_zero

added theorem real.Gamma_neg_nat_eq_zero

added theorem real.Gamma_seq_tendsto_Gamma

added theorem real.Gamma_zero

added def real.bohr_mollerup.log_gamma_seq

added theorem real.bohr_mollerup.tendsto_log_Gamma

modified theorem real.differentiable_at_Gamma

deleted def real.log_gamma_seq

deleted theorem real.tendsto_log_Gamma

Modified src/analysis/specific_limits/basic.lean

added theorem tendsto_coe_nat_div_add_at_top

Modified src/data/complex/exponential.lean

added theorem real.one_sub_div_pow_le_exp_neg