Differentiability of paths in manifolds

Stream: mathlib4

[Ben Eltschig]

Over the past few months I've been playing around a bit with formalising Riemannian manifolds in lean, and in the process wrote quite a few lemmas on smoothness and derivatives of paths in manifolds. I'm now at a point where I'm thinking about potentially PR-ing some of those to mathlib, and would like to know whether such a PR would be welcome, or whether my approach is maybe not the one mathlib should use.

Specifically, I've used the SmoothManifoldWithCorners-instance on the unit interval to talk about smoothness of paths using the existing API for smooth maps between manifolds with corners, and also defined the derivative of paths as a function $t\mapsto\gamma'(t)\in T_{\gamma(t)}M$ using the existing mfderiv-API by evaluating it as needed. The main results include:

• γ.symm is differentiable/C^n/smooth at t iff γis the same at unitInterval.symm t
• for $t<\frac12$ γ.trans γ' is differentiable/C^n/smooth at $t$ iff γis the same at $2t$
• for $t>\frac12$ γ.trans γ' is differentiable/C^n/smooth at $t$ iff γ'is the same at $2t-1$
• γ.trans γ'is differentiable iff both γ and γ' are differentiable and their derivatives at the endpoints match
• the derivative of γ.symm at t equals minus the derivative of γ at unitInterval.symm t
• for $t<\frac12$ the derivative of γ.trans γ' at $t$ equals twice the derivative of γ at $2t$
• for $t>\frac12$ the derivative of γ.trans γ' at $t$ equals twice the derivative of γ' at $2t-1$.

The reason that I think those would be useful to have in mathlib is that they are required for example to define the length of paths in Riemannian manifolds and prove some basic properties like additivity under concatenation (in fact I've already done so in another file), or to define and work with piecewise C^n/smooth paths, which will eventually be required to define the distance function on Riemannian manifolds.
I however also know that mathlib has a preference towards working with functions defined on all of ℝ rather than just $[0,1]$, and indeed working with the smooth structure of the unit interval has made parts of my code quite lengthy; the lemmas outlined above with all their variants take about 600 lines of code, but also another 500 lines of prerequisites on smoothness and derivatives of certain functions like $t\mapsto\min(2t,1)$ on the unit interval. This has me questioning a bit whether this really was the right approach, or whether doing most computations with γ.extend instead might've been a better choice.

So, is this something that would still be an good/acceptable starting point for a PR? If it is, what would be the next steps I should take?

[Johan Commelin]

Let me ping our manifold crowd: @Heather Macbeth @Sebastien Gouezel @Patrick Massot @Yury G. Kudryashov

[Yury G. Kudryashov]

I think that using functions from real numbers is easier.

[Yury G. Kudryashov]

And we should have lemmas about length of a path parametrized by $[a, b]$, not only $[0, 1]$.

[Yury G. Kudryashov]

BTW, do we have lemmas like t ≤ 1/2 → (γ.trans γ').extend t = γ.extend(2 * t)?

[Yury G. Kudryashov]

And simple corollaries like t < 1/2 → (γ.trans γ').extend =ᶠ[𝓝 t] (γ <| 2 * ⋅)?

[Junyan Xu]

Yury G. Kudryashov said:

BTW, do we have lemmas like t ≤ 1/2 → (γ.trans γ').extend t = γ.extend(2 * t)?

Haha, we have exactly almost this at mathlib3#18375 (which it's also about lengths of paths!) It should indeed be stated in terms of Path.extend, not sure why I chose the statement. Maybe because it's about two functions on the unit interval, not the reals? (If someone can help porting the PR please do.)

[Junyan Xu]

We had some discussion about integration of a function along a curve in the context of contour integrals in complex analysis. I think the generality we should aim for is defining it for measurable functions and rectifiable curves, for which we can pullback the arclength to a measure on an interval and do Lebesgue integration on the interval. (Rectifiability is independent of the choice of a (smooth) chart. I guess your definition of length also requires choosing a chart. Have you made progress proving the length is invariant under change of coordinates?)

[Ben Eltschig]

Junyan Xu said:

Yury G. Kudryashov said:

BTW, do we have lemmas like t ≤ 1/2 → (γ.trans γ').extend t = γ.extend(2 * t)?

Haha, we have exactly almost this at mathlib3#18375 (which it's also about lengths of paths!) It should indeed be stated in terms of Path.extend, not sure why I chose the statement. Maybe because it's about two functions on the unit interval, not the reals? (If someone can help porting the PR please do.)

That's actually really similar to how I've written the lemma too, except I've given names to even more common functions like your div_two because they kept appearing all over the place. Talking about extended paths instead is probably a good way to avoid having to do that indeed.

[Ben Eltschig]

Junyan Xu said:

We had some discussion about integration of a function along a curve in the context of contour integrals in complex analysis. I think the generality we should aim for is defining it for measurable functions and rectifiable curves, for which we can pullback the arclength to a measure on an interval and do Lebesgue integration on the interval. (Rectifiability is independent of the choice of a (smooth) chart. I guess your definition of length also requires choosing a chart. Have you made progress proving the length is invariant under change of coordinates?)

I don't think I've defined length in a coordinate-dependent way actually - I just did it as the integral over the norm of the derivative as a function on $[0,1]$. Of course that only works right for differentiable paths though, so I agree that this should probably be done more generally in mathlib.
What I'm really here to ask about is not lengths of paths though, but the lemmas on differentiability outlined above. I'd assume that with smooth paths being so common in differential geometry they'd still be useful to have around - or is differentiability also something that should be talked about only in terms of γ.extend, not just in the proofs of those lemmas but also their statements?