Commit 2023-06-14 06:27 6054b3d4

View on Github →

feat: port Analysis.MellinTransform (#4932)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/MellinTransform.lean

added theorem Complex.cpow_mul_ofReal_nonneg

added def HasMellin

added theorem MellinConvergent.comp_mul_left

added theorem MellinConvergent.comp_rpow

added theorem MellinConvergent.const_smul

added theorem MellinConvergent.cpow_smul

added def MellinConvergent

added theorem hasMellin_add

added theorem hasMellin_cpow_Ioc

added theorem hasMellin_one_Ioc

added theorem hasMellin_sub

added theorem isBigO_rpow_top_log_smul

added theorem isBigO_rpow_zero_log_smul

added def mellin

added theorem mellinConvergent_of_isBigO_rpow

added theorem mellinConvergent_of_isBigO_rpow_exp

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_iff_norm

added theorem mellin_convergent_of_isBigO_scalar

added theorem mellin_convergent_top_of_isBigO

added theorem mellin_convergent_zero_of_isBigO

added theorem mellin_cpow_smul

added theorem mellin_differentiableAt_of_isBigO_rpow

added theorem mellin_differentiableAt_of_isBigO_rpow_exp

added theorem mellin_div_const

added theorem mellin_hasDerivAt_of_isBigO_rpow