Formalizing the fundamental theorem of plane curves

Stream: mathlib4

[Michael Novak]

I plan to formalize what's sometimes called "The fundamental theorem of plane curves" in elementary differential geometry, which roughly says that given a curvature function we can pretty much completely determine the plane curve.
What I wanted to ask here is first how do you recommend to define what a plane curve is.
Secondly, I originally wanted to define the curvature at point of a plane curve using the arc-length reparamentrization which I proved exists for any regular parametrized curve in PR #33330, and then show that it also can be calculated in general with some formula (which holds not only for arc-length curves), however it seems like some people in Mathlib work on a general definition of length for curves and plan to define with it a more general definition of arc-length reparamentrization (although I still didn't get an answer as to whether my work could be useful in any way or not), so maybe I should just define curvature using the general formula (and perhaps also write a theorem about the case where the plane curve is parametrized by arc-length, although that's not essential) ?
Additionally, please let me know if there are plans to create any generalizations that would make this work a waste of time, because when I worked on the arc-length reparametrization project and talked with experienced Mathlib contributors here in Zulip no one told me that there are plans of writing somemthing more general. I've been told that there is work being done on defining curvature very generally, but that I can have a definition just for plane curves and in the future once the general definition exists we could prove that the plane curves definition is the same as the general definition applied to plane curves, so I think this work should be a productive contribution to Mathlib, but still I want to ask this again to make sure.

[Michael Novak]

So I made a first draft skeleton for this project and would really appreciate some feedback about it:

import Mathlib

noncomputable section

/-- Curvature for plane curves. This definition is meaningful only for regular plane curves which
are twice continuousely differentiable on an interval I. -/
def curvature (c : ℝ →  Fin 2 → ℝ) (t : ℝ) : ℝ :=
  let M : Matrix (Fin 2) (Fin 2) ℝ :=
    fun i j ↦  if j=0 then (deriv c t) i else (iteratedDeriv 2 c t) i
  M.det / (‖deriv c t‖^3)

/-- This is the plane curve we construct in the fundamental theorem of plane curves, given curvature
function κ, initial position p₀ at time t₀ and initial velocity vector condition given by an angle
θ₀ (this angle is a choice of direction for the unit velocity vector at time t₀). This definition is
only meaningful when κ is continuous on some given interval. -/
def curvatureToPlaneCurve  (κ : ℝ → ℝ) (t₀ : ℝ)  (p₀ : Fin 2 → ℝ) (θ₀ : ℝ) : ℝ → Fin 2 → ℝ :=
  fun t ↦  fun i ↦ if i=0 then p₀ 0 + (∫τ in t₀..t, (Real.cos (θ₀ + ∫ξ in t₀..τ, κ ξ)))
    else p₀ 1 + (∫τ in t₀..t, (Real.sin (θ₀ + ∫ξ in t₀..τ, κ ξ)))

/-- The plane curve we construct from the given curvature function κ is twice continuousely
differentiable on the given interval I. -/
theorem curvatureToPlaneCurve_is_twice_contDiff {I : Set ℝ} [I.OrdConnected] (hI : IsOpen I)
  {κ : ℝ → ℝ} (hκ : ContinuousOn κ I) {t₀ : ℝ} (ht₀ : t₀ ∈ I) (p₀ : Fin 2 → ℝ) (θ₀ : ℝ) :
  ContDiffOn ℝ 2 (curvatureToPlaneCurve κ t₀ p₀ θ₀) I := sorry

/-- The plane curve we construct from the given curvature function κ is parametrized by
  arc-length or in other words has unit speed. -/
theorem curvatureToPlaneCurve_has_unit_speed {I : Set ℝ} [I.OrdConnected] (hI : IsOpen I)
  {κ : ℝ → ℝ} (hκ : ContinuousOn κ I) {t₀ : ℝ} (ht₀ : t₀ ∈ I) (p₀ : Fin 2 → ℝ) (θ₀ : ℝ) {t : ℝ}
  (ht : t ∈ I): ‖deriv (curvatureToPlaneCurve κ t₀ p₀ θ₀) t‖ = 1 := sorry

/-- The plane curve we construct from a given function κ has curvature function κ. -/
theorem curvatureToPlaneCurve_to_curvature {I : Set ℝ} [I.OrdConnected] (hI : IsOpen I)
  {κ : ℝ → ℝ} (hκ : ContinuousOn κ I) {t₀ : ℝ} (ht₀ : t₀ ∈ I) (p₀ : Fin 2 → ℝ) (θ₀ : ℝ) {t : ℝ}
  (ht : t ∈ I): curvature (curvatureToPlaneCurve κ t₀ p₀ θ₀) t = κ t := sorry

/-- The plane curve we construct is at the point p₀ at time t₀ (position initial condition). -/
theorem curvatureToPlaneCurve_position_initial_condition {I : Set ℝ} [I.OrdConnected]
  (hI : IsOpen I) {κ : ℝ → ℝ} (hκ : ContinuousOn κ I) {t₀ : ℝ} (ht₀ : t₀ ∈ I) (p₀ : Fin 2 → ℝ)
  (θ₀ : ℝ) : (curvatureToPlaneCurve κ t₀ p₀ θ₀) t₀ = p₀ := sorry

/-- The plane curve we construct has unit velocity vector at the direction of the angle θ₀ at time
t₀ (velocity initial condition). -/
theorem curvatureToPlaneCurve_velocity_initial_condition {I : Set ℝ} [I.OrdConnected]
  (hI : IsOpen I) {κ : ℝ → ℝ} (hκ : ContinuousOn κ I) {t₀ : ℝ} (ht₀ : t₀ ∈ I) (p₀ : Fin 2 → ℝ)
  (θ₀ : ℝ) :
  deriv (curvatureToPlaneCurve κ t₀ p₀ θ₀) t₀ = fun i ↦  if i=0 then Real.cos θ₀ else Real.sin θ₀
  := sorry

/-- This is the uniqueness part of the fundamental theorem of plane curves: given a curvature
function κ and intital conditions (position p₀ at some time t₀ and unit velocity vector at time t₀
at direction given by angle θ₀) the plane curve we construct is the only such twice continuousely
differentiable plane curve parametrized bt arc-length with curvature κ ands satisfing the initial
position and velocity conditions. -/
theorem curvatureToPlaneCurve_is_unique {I : Set ℝ} [I.OrdConnected] (hI : IsOpen I) {κ : ℝ → ℝ}
  (hκ : ContinuousOn κ I) {t₀ : ℝ} (ht₀ : t₀ ∈ I) (p₀ : Fin 2 → ℝ) (θ₀ : ℝ) {c : ℝ → Fin 2 → ℝ}
  (twice_contDiff : ContDiffOn ℝ 2 c I) (has_unit_speed : ∀ t ∈ I, ‖deriv c t‖ = 1)
  (has_curvature_κ : ∀ t ∈ I, curvature c t = κ t) (position_condition : c t₀ = p₀)
  (velocity_condition : deriv c t₀ = fun i ↦  if i=0 then Real.cos θ₀ else Real.sin θ₀):
  I.EqOn c (curvatureToPlaneCurve κ t₀ p₀ θ₀) := sorry

[Michael Novak]

By the way here is the theorem written in English, with similar (although slightly different) notation to what I use in my file:
image.png

[Michael Rothgang]

I do think #33330 can be useful for mathlib --- it just needs to be revised to take the review feedback into account. (I am aware that this is a substantial revision.) In other words, you could

• define the arc-length of a curve (without requiring differentiability) edit: already exists, see below
• prove that the arc-length coincides with your formula for C¹ curves
• prove that the reparametrisation you give yields curves of unit speed

The first bullet could be its own PR. Definitions can be tricky to formalise nicely; I'm sure @Jireh Loreaux or I could suggest some useful basic properties for you to prove (as a test that your definition works well). (I'm just on my way to two weeks of holiday/work travel, so likely will only have time after that.)

[Michael Rothgang]

In other words: it's not a binary "your work is useful" / "your work is no good"! Working on this topic can be useful --- to get incorporated into mathlib, it just needs to be at the right level of generality. (Knowing this level can require some mathematical maturity; you can always ask here on zulip if you're unsure.)

[Michael Rothgang]

Regarding your question above:

• my medium-term goal is to define curvature "in general" (for Riemannian manifolds). This will take a few months to get merged into mathlib, I'm sure.
• even when this is completed, having a lemma/theorem "for a plane curve, its curvature is given by the following expression" is useful! So, it's fine to define a notion of curvature the way you propose (and later, when the definition of curvature for manifolds gets merged, prove that it equals the formula you give).
• it's good to have a curvature formula for all plane curves (and then have a specialisation to unit speed curves)! (It's also good to have arc length defined, as I said above.)

[Michael Rothgang]

Here are some comments about the code snippet you posted.

• is your first definition curvature also meaningful for a curve into R^n? If so, you could use a general indexing type ι (with the assumption [Finite ι]) instead of Fin 2 (in many places). It's very possible some results will work in n dimensions, and others will be specific to two.
• Your name curvature is very general; you probably want to move it to some namespace (to make clear it's not Ricci/scalar/... curvature defined on manifolds). Maybe EuclideanSpace.curvature? (It's fine to not address this at first, and only do so when you're polishing your code for a mathlib PR.)
• I'd call curvatureToPlaneCurverather initialCurve_of_curvature.
• curvatureToPlaneCurve_is_twice_contDiff should be ContDiffOn.curvatureToPlanCurve (and renamed accordingly to that you name your previous definition).
• curvatureToPlaneCurve_to_curvature should be named curvature_curvatureToPlaneCurve (and adapted, etc.) --- a statement about curvature foo is named curvature_foo in mathlib's convention.

[Michael Rothgang]

A final question: the fundamental theorem I saw in class worked for curves into R^3 (and this also generalises to R^n, to some extent). I wonder if it's useful to make your code more forward-looking, by anticipating such a generalisation.

[Sébastien Gouëzel]

Michael Rothgang said:

I do think #33330 can be useful for mathlib --- it just needs to be revised to take the review feedback into account. (I am aware that this is a substantial revision.) In other words, you could

• define the arc-length of a curve (without requiring differentiability)
• prove that the arc-length coincides with your formula for C¹ curves
• prove that the reparametrisation you give yields curves of unit speed

We already have the arc-length of a curve. It's called docs#variationOnFromTo.

[Michael Novak]

Michael Rothgang said:

A final question: the fundamental theorem I saw in class worked for curves into R^3 (and this also generalises to R^n, to some extent). I wonder if it's useful to make your code more forward-looking, by anticipating such a generalisation.

There's also such a theorem for space curves as you said, but in the case of space curves, the curve is determined not only by the curvature function but also by the torsion function. I probably would like to prove the theorem for space curves as well after I finish with the theorem for plane curves.

[Michael Novak]

Michael Rothgang said:

Here are some comments about the code snippet you posted.

• is your first definition curvature also meaningful for a curve into R^n? If so, you could use a general indexing type ι (with the assumption [Finite ι]) instead of Fin 2 (in many places). It's very possible some results will work in n dimensions, and others will be specific to two.
• Your name curvature is very general; you probably want to move it to some namespace (to make clear it's not Ricci/scalar/... curvature defined on manifolds). Maybe EuclideanSpace.curvature? (It's fine to not address this at first, and only do so when you're polishing your code for a mathlib PR.)
• I'd call curvatureToPlaneCurverather initialCurve_of_curvature.
• curvatureToPlaneCurve_is_twice_contDiff should be ContDiffOn.curvatureToPlanCurve (and renamed accordingly to that you name your previous definition).
• curvatureToPlaneCurve_to_curvature should be named curvature_curvatureToPlaneCurve (and adapted, etc.) --- a statement about curvature foo is named curvature_foo in mathlib's convention.

Thank you very much for all the suggestions. I made quite a few challenges to the code already, for example I work now in EuclideanSpace ℝ (Fin 2), and I will do further changes based on your suggestions. I have two questions:

1. Since I only learned very basic elementary differential geometry I don't know if there's a general formula for curvature of curves in R^n, is there such a formula? From the little I did learned I'm inclined to believe that at least for the case of plane curves, how curvature is usually defined is unique or at least different from space curves because for plane curves the curvature can be positive, negative or zero, but for space curves the curvature is always non-negative - it is the length of the acceleration vector (assuming the curve is parametrized by arc-length).
2. when I work with plane curves is it o.k that I use Fin 2 or should I use a general finite type with two elements?

[Michael Novak]

Sébastien Gouëzel said:

Michael Rothgang said:

I do think #33330 can be useful for mathlib --- it just needs to be revised to take the review feedback into account. (I am aware that this is a substantial revision.) In other words, you could

• define the arc-length of a curve (without requiring differentiability)
• prove that the arc-length coincides with your formula for C¹ curves
• prove that the reparametrisation you give yields curves of unit speed

We already have the arc-length of a curve. It's called docs#variationOnFromTo.

My question is: Is there work being done about also defining the speed of a curve more generally and also arc-length (i.e, unit-speed) reparametrization generally? And could my work (PR #33330) be somewhat useful in any way for proving some theorem in the special case of differentiable curves?

[Michael Rothgang]

I'm not aware of such work.

[Jireh Loreaux]

@Sébastien Gouëzel what do you think we should do with #31766 ? Do you think it's simply not necessary?

[Michael Novak]

Michael Rothgang said:

I'm not aware of such work.

In this case, should it be done (I possibly could try to do it), or is there no need for such generality and using speed only for differentiable curves enough (in which case it seems like that's exactly what I did in #33330 - I didn't define the length of a curve - I defined the arc-length reparametrization of a curve, i.e, unit-speed reparametrization)?

[Sébastien Gouëzel]

Jireh Loreaux said:

Sébastien Gouëzel what do you think we should do with #31766 ? Do you think it's simply not necessary?

There are two parts in #31766:
(a): introducing a new definition for arclength, which is essentially a wrapper around eVariationOn (Icc ...)
(b) prove continuity statements for the arclength.

I have no opinion on (a): I have the impression that working just with eVariationOn would be perfectly viable, but if it helps to add the wrapper then why not (although duplicating API is often not a good idea). For (b), though, I'd rather see the statements proved in the right generality, i.e., directly for eVariationOn as this would apply in strictly more cases. Incidentally, I have an open PR which does essentially this, see #34559...

[Jireh Loreaux]

I've put it on my list.

[Michael Novak]

Michael Novak said:

Michael Rothgang said:

Here are some comments about the code snippet you posted.

• is your first definition curvature also meaningful for a curve into R^n? If so, you could use a general indexing type ι (with the assumption [Finite ι]) instead of Fin 2 (in many places). It's very possible some results will work in n dimensions, and others will be specific to two.
• Your name curvature is very general; you probably want to move it to some namespace (to make clear it's not Ricci/scalar/... curvature defined on manifolds). Maybe EuclideanSpace.curvature? (It's fine to not address this at first, and only do so when you're polishing your code for a mathlib PR.)
• I'd call curvatureToPlaneCurverather initialCurve_of_curvature.
• curvatureToPlaneCurve_is_twice_contDiff should be ContDiffOn.curvatureToPlanCurve (and renamed accordingly to that you name your previous definition).
• curvatureToPlaneCurve_to_curvature should be named curvature_curvatureToPlaneCurve (and adapted, etc.) --- a statement about curvature foo is named curvature_foo in mathlib's convention.

Thank you very much for all the suggestions. I made quite a few challenges to the code already, for example I work now in EuclideanSpace ℝ (Fin 2), and I will do further changes based on your suggestions. I have two questions:

1. Since I only learned very basic elementary differential geometry I don't know if there's a general formula for curvature of curves in R^n, is there such a formula? From the little I did learned I'm inclined to believe that at least for the case of plane curves, how curvature is usually defined is unique or at least different from space curves because for plane curves the curvature can be positive, negative or zero, but for space curves the curvature is always non-negative - it is the length of the acceleration vector (assuming the curve is parametrized by arc-length).
2. when I work with plane curves is it o.k that I use Fin 2 or should I use a general finite type with two elements?

In regards to question 1., I've read a bit about how curvature of curves is defined in general in the curves section of this Wikipedia article and it seems like in general it is the same as what one usually learns about space curves in elementary differential geometry - it is the magnitude of the derivative of the unit tangent vector, and there is also the curvature vector which is the derivative of the unit tangent vector. But for the special case of plane curves, what in most elementary differential geometry books is called just the curvature is called in this Wikipedia article the signed / oriented curvature, which is the curvature that's used in the fundamental theorem of plane curves. So, I think maybe we should also call it something like PlaneCurves.orientedCurvature, or something similar, and in the future when formalizing the fundamental theorem for space curves we can work with curvature which is defined for any curve (any dimension). What do you think?