issue #694: We don't have Cauchy's integral formula

Stream: triage

[Random Issue Bot]

Today I chose issue 694 for discussion!

We don't have Cauchy's integral formula
Created by @Kevin Buzzard (@kbuzzard) on 2019-02-07
Labels: feature-request, hard, long term

Is this issue still relevant? Any recent updates? Anyone making progress?

[Kevin Buzzard]

As far as I know we're still bikeshedding about whether we should be integrating a holomorphic function around a smooth curve, a piecewise differentiable curve, a locally rectifiable curve,... . I am not an analyst so I don't really know the correct generality; I would imagine that there are people around here who do know though. I would imagine that we're getting to the point where if we come up with a definition, we might be able to integrate 1/z around the unit circle, which would be a cool and related result.

[Heather Macbeth]

I think that the Cauchy integral formula itself is not the real issue. We should be able to do a lot of complex analysis once we have the Cauchy integral formula for some fixed simple class of curves, like (say) triangles, or rectangles, or circles.

And this basically already exists, just hasn't been PR'd: see Yury's huge branch#stokes-thm, and this discussion of its status:
https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Stokes'.20theorem/near/225379719
(From Stokes to the Cauchy integral formula is just the Cauchy-Riemann equations, which isn't PR'd but also isn't difficult, see my branch#complex-diff.)

[Kevin Buzzard]

Yes -- Cauchy's integral formula was just a completely random theorem plucked out of my memory of undergrad complex variable and the issue is just supposed to be a reminder that in some sense this whole area is the most "basic" (from the point of view of an undergraduate education in pure mathematics) area which we're not really covering right now. I would have no objections to you closing the issue and opening a new one which says "we don't have (something you believe is more representative of the issue that we don't have anything like a first course in complex analysis).

[Kevin Buzzard]

It's also great to hear that we are closing in on this area! A lot of applied mathematicians use this stuff.

[Yury G. Kudryashov]

I did not PR my branch#stokes-thm because I want to prove it in a slightly more general case. I'll try to do it this or next week.

[Jack J Garzella]

@Yury G. Kudryashov Do we know what the current status of this is?

[Yury G. Kudryashov]

I'll try to come back to this tonight or on Monday.

[Random Issue Bot]

Today I chose issue 694 for discussion!

We don't have Cauchy's integral formula
Created by @Kevin Buzzard (@kbuzzard) on 2019-02-07
Labels: hard, long term, feature-request

Is this issue still relevant? Any recent updates? Anyone making progress?

[Sebastien Gouezel]

Just closed by #10000

[Johan Commelin]

It's like the bot is sentient! What a timing (-;

[Kevin Buzzard]

Great -- I'll have to think of another issue!