mathlib3

e9be2fa7 - feat(analysis/complex): integration and differentiation `ℝ → ℂ` (#17989)

feat(analysis/complex): integration and differentiation `ℝ → ℂ` (#17989) In Fourier theory it's often necessary to work with integrals and derivatives of functions `ℝ → ℂ`. This adds a couple of shortcuts for doing so, and uses them to slightly simplify some code already in the library. (Cherry-picked out of my Riemann zeta values project.)