Contour Integration over the complex numbers

Stream: Is there code for X?

[Jaime Diaz]

Hi all,
I'm pretty new to Lean and I was trying to work on the Cacuchy theorem for complex integration. As part of that I need to define integral over a path in Lean. I thought it was going to be pretty straight forward, however it wasn't. This is what I tried:

noncomputable def pathIntegral1 (x y : ℂ ) (f : ℂ → ℂ) (γ : Path x y) : ℂ := have aux : unitInterval → ℂ := (Function.comp f γ) * (deriv γ) ∫t in (Set.Icc 0 1), aux t

The issue is that the derivative and the integral both require the domain of the function to be a non trivial normed field, and to be a measure space. I thought being a subset of ℝ would suffice, but it does not.
I was wondering wether path integrals are already defined in Lean or if there is a way to fix this code.
Thank you in advance.

[Vincent Beffara]

Contour integrals are not yet in mathlib except in the special case of the circle. Essentially you will have two options, depending on your assumptions on the curve: if you have differentiability you can just say

noncomputable def curvint (t₁ t₂ : ℝ) (f : ℂ → ℂ) (γ : ℝ → ℂ) : ℂ :=
  ∫ t in t₁..t₂, deriv γ t • f (γ t)

(without using the Path API, and instead working with functions defined on the whole real line, might not be the best idea but at least it makes the definition simpler). You can use deriv_within instead of deriv, it will probably make some arguments easier down the line.

If the contour is just assumed do be continuous, then you have to pay for it by restricting f (it has to be holomorphic for the integral to make sense, if it isn't it is easy to find examples where the "correct" value of the integral is infinite). And then the definition is much more involved - but a version will probably be PRed to mathlib in the not so distant future.