mathlib

ea2dbcbb - feat(analysis/special_functions/integrals): Add integral_cpow (#14491)

feat(analysis/special_functions/integrals): Add integral_cpow (#14491) Also adds various helper lemmas. The purpose of this commit is to provide a computed integral for the `cpow` function. The proof is functionally identical to that of `integral_rpow`, but places a different set of constraints on the various parameters due to different continuity constraints of the cpow function. Some notes on future improvments: * The range of valid integration can be expanded using ae_covers a la #14147 * We currently only contemplate a real argument. However, this should essentially work for any continuous path in the complex plane that avoids the negative real axis. That would require a lot more machinery, not currently in mathlib. Despite these restrictions, why is this important? This, Abel summation, #13500, and #14090 are the key ingredients to bootstrapping Dirichlet series.