Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-12 08:46 9e6d4aec

View on Github →

feat(analysis/mellin_transform): Mellin transforms (#18822) This PR defines the Mellin transform of a locally integrable function, and proves it is holomorphic on a suitable vertical strip.

Estimated changes

Created src/analysis/mellin_transform.lean

added theorem is_O_rpow_top_log_smul

added theorem is_O_rpow_zero_log_smul

added def mellin

added theorem mellin_convergent_iff_norm

added theorem mellin_convergent_of_is_O_rpow

added theorem mellin_convergent_of_is_O_rpow_exp

added theorem mellin_convergent_of_is_O_scalar

added theorem mellin_convergent_top_of_is_O

added theorem mellin_convergent_zero_of_is_O

added theorem mellin_differentiable_at_of_is_O_rpow

added theorem mellin_differentiable_at_of_is_O_rpow_exp

added theorem mellin_has_deriv_of_is_O_rpow

Modified src/analysis/special_functions/pow.lean

added theorem is_o_exp_neg_mul_rpow_at_top