Runge's Theorem?

Stream: Is there code for X?

[Dattabhasvant Ghadiyaram]

I am an undergrad looking for ideas for my course project. My first thought was the Riemann Mapping Theorem, but as it turns out, that's already done, pending a PR into mathlib.

After a code search on GitHub, I've found that Runge's Theorem has not been formalized in Lean. Is there any similar project currently underway, or would this be a worthwhile new direction to explore?

[Kevin Buzzard]

Hmm, looking at the Wikipedia article, I'm not convinced that our contour integration library is ready for that proof? Do we have Cauchy's integral formula for piecewise linear contours?

[Weiyi Wang]

I searched for cauchy integral formula for arbitrary contour the other day and didn't find it, so I guess that is needed first

[Dattabhasvant Ghadiyaram]

I could work on cauchy integral formula for general closed curves then. Would it be doable in about a month or so?

[Yaël Dillies]

How much experience do you have in Lean? If this is your first project ever, I would tend to say "That will be hard to do within one month"

[Dattabhasvant Ghadiyaram]

I'm a beginner, and this is my first project. What would be a more achievable goal in this direction?

[Johan Commelin]

Kevin Buzzard said:

Luigi Massacci said:

isn’t all the work of Eberl on complex path integrals in the afp?

I talked to Manuel about this quite a bit and he explained to me a more simple approach than what he implemented (which I talked about with David Loeffler), probably that's what we want.

@Kevin Buzzard Is this written up somewhere? Are components of that suitable as a beginner project? E.g. defining a bunch of "puzzle pieces" as building blocks for contours.

[Kevin Buzzard]

I didn't write anything, and I don't think Eberl did either

[Kevin Buzzard]

Certainly the undergraduates who do my course have far less lofty goals than "prove something that isn't in mathlib" for their projects. Many things are not yet in mathlib for a good reason :-)

[Luigi Massacci]

I think it’s worthwhile to remember there’s also the option to prove something not in mathlib, but with no expectation it will ever get there