Commit 2023-02-08 20:27 c8fc41b2

View on Github →

feat (analysis/special_functions): add the Beta function (#18373) Add the Beta function, and prove its relation to the Gamma function via convolution integrals.

Estimated changes

Modified src/analysis/special_functions/gamma.lean

added theorem complex.Gamma_mul_Gamma_eq_beta_integral

added theorem complex.beta_integral_convergent

added theorem complex.beta_integral_convergent_left

added theorem complex.beta_integral_eval_nat_add_one_right

added theorem complex.beta_integral_eval_one_right

added theorem complex.beta_integral_recurrence

added theorem complex.beta_integral_scaled

added theorem complex.beta_integral_symm