Commit 2022-06-15 21:34 ea2dbcbb

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.