feat: define contour integrals

[urkud]

Specialize curveIntegral to the case if the domain is ℂ.
In this case, we can integrate a function, not a 1-form.

I've decided not to specialize HasFDerivWithinAt etc theorems,
because I want to review API for curve integrals first.

This PR was written at ICERM meeting.

---

[github-actions]

PR summary 834e51690b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.MeasureTheory.Integral.ContourIntegral.Basic (new file)	2410

---

Declarations diff

+ ContinuousOn.contourIntegrable_of_contDiffOn
+ ContourIntegrable
+ ContourIntegrable.add
+ ContourIntegrable.cast
+ ContourIntegrable.neg
+ ContourIntegrable.refl
+ ContourIntegrable.smul
+ ContourIntegrable.sub
+ ContourIntegrable.symm
+ ContourIntegrable.trans
+ ContourIntegrable.zero
+ _root_.intervalIntegrable_fun_smul_iff
+ _root_.intervalIntegrable_smul_iff
+ contourIntegrable_cast_iff
+ contourIntegrable_fun_neg_iff
+ contourIntegrable_neg_iff
+ contourIntegrable_segment
+ contourIntegrable_smul_iff
+ contourIntegrable_symm
+ contourIntegral
+ contourIntegral_add
+ contourIntegral_cast
+ contourIntegral_eq_intervalIntegral_derivWithin_smul
+ contourIntegral_eq_intervalIntegral_deriv_smul
+ contourIntegral_fun_add
+ contourIntegral_fun_neg
+ contourIntegral_fun_smul
+ contourIntegral_fun_sub
+ contourIntegral_fun_zero
+ contourIntegral_neg
+ contourIntegral_of_not_completeSpace
+ contourIntegral_refl
+ contourIntegral_segment
+ contourIntegral_segment_const
+ contourIntegral_smul
+ contourIntegral_sub
+ contourIntegral_symm
+ contourIntegral_trans
+ contourIntegral_zero
+ curveIntegrable_fun_smul_iff
+ norm_contourIntegral_segment_le
+ toSpanSingleton_neg
+ toSpanSingleton_sub

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to strong technical debt.

No changes to weak technical debt.