Commit 2023-05-27 20:56 917c3c07

View on Github →

feat (analysis/mellin_transform): API for mellin transforms (#19110) This adds results about Mellin transforms of things like f(a * x) or f (x ^ a) in terms of the Mellin transform of f.

Estimated changes

Modified src/analysis/mellin_transform.lean

added theorem complex.cpow_mul_of_real_nonneg

added def has_mellin

added theorem has_mellin_add

added theorem has_mellin_cpow_Ioc

added theorem has_mellin_one_Ioc

added theorem has_mellin_sub

modified def mellin

added theorem mellin_comp_inv

added theorem mellin_comp_mul_left

added theorem mellin_comp_mul_right

added theorem mellin_comp_rpow

added theorem mellin_const_smul

added theorem mellin_convergent.comp_mul_left

added theorem mellin_convergent.comp_rpow

added theorem mellin_convergent.const_smul

added theorem mellin_convergent.cpow_smul

added theorem mellin_convergent.div_const

added def mellin_convergent

added theorem mellin_cpow_smul

added theorem mellin_div_const

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