Zulip Chat Archive

Stream: triage

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


view this post on Zulip Random Issue Bot (Apr 02 2021 at 14:23):

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?

view this post on Zulip Kevin Buzzard (Apr 02 2021 at 16:43):

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.

view this post on Zulip Heather Macbeth (Apr 02 2021 at 17:00):

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.)

view this post on Zulip Kevin Buzzard (Apr 02 2021 at 18:11):

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).

view this post on Zulip Kevin Buzzard (Apr 02 2021 at 18:12):

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

view this post on Zulip Yury G. Kudryashov (Apr 08 2021 at 15:07):

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.


Last updated: May 09 2021 at 16:20 UTC