Define complex (path) integrals

Stream: mathlib4

[Juanan]

Hi,
I am trying to find a good definition for complex path integrals but can't come up with much. Do you know of any effective definition or have any suggestion?
Thanks!

[Yury G. Kudryashov]

What generality do you want?

[Juanan]

Yury G. Kudryashov said:

What generality do you want?

Hi Yury,
I am trying to define them for an arbitrary path γ and a given complex function. However, integration itself is not defined for complex numbers (except for contour integrals) so it's being quite tricky

[Kalle Kytölä]

Here is some earlier discussion on setting up complex contour integrals in a good generality. One of the main issues is that while it is easy to write down a definition for (piecewise) $C^1$ paths (and say continuous integrands), for integrals of holomorphic functions one really wants homotopy invariance in the usual $C^0$ sense, so the definition of contour integration had better make sense for $C^0$ paths and holomorphic integrands. So I think the ultimate mathlib-style definition is not yet in mathlib, but if you don't need homotopies and your paths are piecewise $C^1$ then it is not difficult to write down a direct definition.

[Kalle Kytölä]

For concreteness, something like the following would be ok for $C^1$ paths. When the mathlib-appropriate definition is made, there will certainly be a lemma showing that it coincides with this when $\gamma$ is $C^1$ and $f$ is holomorphic (continuity of $f$ is "enough" but the general $C^0$ definition will only work for holomorphic integrands since it requires local exactness).

import Mathlib.Analysis.Complex.CauchyIntegral

/-- Contour integral of `f : ℂ → ℂ` along a path `γ : [a,b] → ℂ`. -/
noncomputable def contourIntegral (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) : ℂ :=
  ∫ t in a..b, deriv γ t • f (γ t)

[Juanan]

Kalle Kytölä said:

For concreteness, something like the following would be ok for $C^1$ paths. When the mathlib-appropriate definition is made, there will certainly be a lemma showing that it coincides with this when $\gamma$ is $C^1$ and $f$ is holomorphic (continuity of $f$ is "enough" but the general $C^0$ definition will only work for holomorphic integrands since it requires local exactness).

import Mathlib.Analysis.Complex.CauchyIntegral

/-- Contour integral of `f : ℂ → ℂ` along a path `γ : [a,b] → ℂ`. -/
noncomputable def contourIntegral (γ : ℝ → ℂ) (a b : ℝ) (f : ℂ → ℂ) : ℂ :=
  ∫ t in a..b, deriv γ t • f (γ t)

I'll try this!
Thank you so much Kalle :)