Ben Eltschig

Stream: new members

[Ben Eltschig]

Hi!
I'm Ben, an undergrad currently studying mathematics, physics and CS at the Humbolt university of Berlin, with a focus on topology and differential geometry. I've been lurking here for a while now, but only recently started actually investing some serious time into learning Lean.

In the process I've spent the last few weeks formalising some very basic Riemannian geometry, both to acquaint myself with the differential geometry section of Mathlib4 and to see how far I'd come and what obstacles arise. One thing I've noticed is that as far as I'm aware, Mathlib doesn't yet have the notion of piecewise differentiable/smooth paths, and also not anything related to the derivative of paths at all - could that maybe be a good first project? I've been looking to contribute for a while now, and this seems like something that is both entirely within my reach and will be useful to have in mathlib.

[Patrick Massot]

Probably @Yury G. Kudryashov had thought about piecewise path when working on our complex analysis library.

[Patrick Massot]

Ben, how advanced are you in your studies? Did you get a chance to work with Chris Wendl at Humbolt already?

[Ben Eltschig]

Yes! I took his topology 1 course this semester, and am currently reading his differential geometry lecture notes

[Ben Eltschig]

didn't have the chance to attend his differential geometry 1 lecture in person sadly, but attended that of another lecturer (Marc Kegel) as well as his seminar on hyperbolic knot theory already

[Patrick Massot]

Nice. He was my collaborator before I got distracted by formalized mathematics, and I warmly encourage you to get has much knowledge from him as you can.

[Ben Eltschig]

I sure will, he made a really good impression so far ^^

[Patrick Massot]

He is both a great mathematician and a great teacher (of course I saw him lecture only on very advanced topics, at least at PhD level, but I'm sure he is also great for more elementary stuff).

[Yury G. Kudryashov]

I thought about PW paths but never came to formalize them.

[Yury G. Kudryashov]

I think that we need both a predicate and a constructor.

[Yury G. Kudryashov]

I have a cold right now and can't think clearly. You may ping me in 2-3 days if you want more input from me.

[Ben Eltschig]

By constructor you mean one that takes in the individual smooth/differentiable segments and joins them into a single path, I assume? That sounds useful for concrete computations indeed

[Ben Eltschig]

What I mostly had in mind so far was a predicate with some lemmas showing that for example differentiable paths, inverses of piecewise differentiable paths and concatenations of piecewise differentiable paths are all piecewise differentiable

[Kevin Buzzard]

One approach to the finite-dimensionality of spaces of modular forms would be via proving results about an integral around the boundary of the canonical fundamental domain of $SL_2(\Z)$.

[Ben Eltschig]

So that's one example of where piecewise paths would come in use inside the complex analysis part of mathlib?

[Ben Eltschig]

maybe I should clarify - the case I'm mostly interested in is not paths in R^n, but paths in smooth manifolds

[Ben Eltschig]

I'm assuming those would require two seperate definitions, similar to how CondDiff and ContMDiff are two seperate things? or does R^n have some instances that would make this immediately carry over

[Kevin Buzzard]

This would be an integral in the upper half plane.

[Yury G. Kudryashov]

In this case, you can define the manifold version first, then specialize it (if needed) in the case of a normed space.

[Yury G. Kudryashov]

Ben Eltschig said:

By constructor you mean one that takes in the individual smooth/differentiable segments and joins them into a single path, I assume? That sounds useful for concrete computations indeed

Yes, I think that we should have a constructor for a piecewise path or a piecewise function on real numbers and a theorem saying that if all inputs are smooth on the corresponding intervals, then the result is piecewise smooth.

[Yury G. Kudryashov]

And maybe a theorem saying that any PW-smooth path can be obtained from this constructor.