Using Diffeomorph with two intervals

Stream: new members

[Michael Novak]

Suppose I have two real intervals

variable (J : Set ℝ) [J.OrdConnected] (I : Set ℝ) [I.OrdConnected]

How do I write the type of bijective functions from J to I which are are also r times continuously differentiable and their inverse is also r times continuously differentiable? I don't really understand the definition of a diffeomorphism in mathlib, in particular what is a ModelWithCorners, I tried to do the following:

variable  (J : Set ℝ) [J.OrdConnected] (I : Set ℝ) [I.OrdConnected] (r : WithTop ℕ∞) (φ : J ≃ₘ^r ⟮ℝ, ℝ⟯ I)

but I get some error which I don't understand. I would appreciate if someone could explain me how to use the diffeomorphism definition, especially in my particular situation.

[Sébastien Gouëzel]

Can you explain why you need to consider this type?

If you just need to talk about one such diffeomorphism (instead of the type of all of them), the simplest situation would probably be to consider a PartialEquiv between I and J (seen as subsets of the real line) requiring that it is ContDiffOn r I, as well as its inverse.

(Note that in general a real interval is not a one-dimensional manifold, because it could be reduced to a point, so there are subtleties -- the way to resolve them really depends on what you want to do)

[Michael Novak]

I'm working on formalizing parametrized curves and the next thing I want to do is define what is a reparametrization of a parametrized curve. To do this I first wanted to define what is a parameter transformation - which is exactly what I'm trying to define here, but I remembered that what I want to define is essentially a diffeomorphism, so I searched for it in mathlib, but the definition is probably a bit more general / complicated than the simpler definition of a diffeomorphism that I know of. Do you think it's better to define what is a parameter transformation by myself instead of using the existing definition of Diffeomorph?

[Sébastien Gouëzel]

Yes, definitely don't use Diffeomorph there, it's overkill. Instead use a map from R to R which is C^r on your interval of definition and with nonvanishing derivative there.

[Michael Novak]

O.k, thank you very much! Is it fine if I define a small structure for this?

[Sébastien Gouëzel]

Will the structure really be helpful? Don't forget that definitions are expensive in mathlib (in the sense that you need to develop a whole API around it to make it useful). For instance, the fact that the length of a curve in a Riemannian manifold is invariant under reparameterization is docs#Manifold.pathELength_comp_of_monotoneOn -- it doesn't use a structure, just stating the necessary properties of the reparameterization (which makes it easier to use in practice).

[Michael Novak]

I get why it's easier not to create a structure in terms of having less work to do, but it seems to me like this theorem you sent is not very readable. Wouldn't it be more readable if instead of having many hypotheses for the reparametrization I would have just one saying that it is of type reparametrization? Just like in math textbooks we don't fold many definitions in every theorem we state - this would make theorems extremely long and unclear. Also, suppose for example that I work with concrete parametrized curves - let's say the unit sphere in R^2, and I proved that I have some reparametrization of it, then wouldn't it be more comfortable to use this in other theorems I want to use which have a reparametrization in as one of their assumptions? Anyways, I'm planing of writing a small file with how I plan everything, and then I would like to create a new topic in the mathlib4 channel and ask for feedback about my plan.

[Sébastien Gouëzel]

The theorem doesn't look readable in the docs because there are many typeclass assumptions. If you go to the source code, it's more readable: the code looks like

/-- The length of a path in a manifold is invariant under a monotone reparametrization. -/
lemma pathELength_comp_of_monotoneOn {f : ℝ → ℝ} (h : a ≤ b) (hf : MonotoneOn f (Icc a b))
    (h'f : DifferentiableOn ℝ f (Icc a b)) (hγ : MDifferentiableOn 𝓘(ℝ) I γ (Icc (f a) (f b))) :
    pathELength I (γ ∘ f) a b = pathELength I γ (f a) (f b) := by

The assumptions on the reparameterization f are just that it's monotone on [a, b] and differentiable there. If you introduced a new definition for these reparameterizations, then you would also need to introduce another one for the antitone case, and then for the C^r case, and then maybe sometimes you want strict monotonicity instead of monotonicity, and maybe even positive derivative. If you introduce definitions for each of these classes, you will also need a lot of theorems saying that a strictly monotone reparameterization is also a monotone reparameterization, and that the composition of two antitone reparameterizations is a monotone reparameterization, with versions in the different classes of smoothness, and so on. In the end, you will need 1000 lines of boilerplate to make your definitions usable. Avoiding the definitions and going for the unbundled properties is just much much more practical!

[Michael Novak]

Thank you for explaining this. It's hard for me to get used to this. Where do we draw the line? Obviously we do have structures in Mathlib, we don't state every theorem using the most primitive types in lean. I also remember I saw a talk on YouTube by Kevin Buzzard where he mentioned that there is value in just creating new definitions in lean. But in this example especially I can't argue with your explanation.

[Sébastien Gouëzel]

There is no clear cut line, it mostly comes with experience. A good way is to begin the development without the definition, prove interesting theorems, and then if afterwards you feel that a definition would have helped, make it and refactor. The other way around (start with the definitions) is worse as you can easily be stuck with a bad definition.