Statement of Cauchy's integral formula

Stream: Is there code for X?

[Kevin Buzzard]

Do we have the statement of Cauchy's Integral Formula in Lean? If not, would this be relatively easy to knock up, possibly with some stub definition of what continuity class the curve needed to be in?

[Kevin Buzzard]

If we could turn this into a theorem with a sorry proof, even if we use undefined constants, it would be a really cool summer project for the hoardes at the discord. I don't trust myself to formalise the statement, because I don't understand the implementation decisions that have been made. I don't want to be making levels, I want to be proving theorems. If the experts could formalise the statement it would be brilliant. If you use an undefined typeclass like [is_smooth_curve] or whatever, then we could just skip the proof that the closed unit disc is a closed curve, for example. If there is more than one possibility for setting this question up, and you think it's worth an experiment, then just guess one and we can try it.

[Yury G. Kudryashov]

Please ping me about it tomorrow. I have some old code with outline of the proof of a version of this theorem but it needs much better integrals library.

[Kevin Buzzard]

I want to go top down so this would be perfect