Looking for feedback on a theorem statement

Stream: mathlib4

[Michael Novak]

Hi, I wanted to ask for feedback about the statement of a theorem I would like to prove and eventually contribute to Mathlib. I plan to write more theorems related to this subject, but I first wanted to make sure I understand the style / conventions of Mathlib. Personally I don't like how this theorem is stated very much, especially not all the many ands, but I was advised not to try to define too many structures and try to state things more directly, so that's what I try to do here. The theorem says that every regular parametrized curve has a unit speed reparametrization, i.e., reparametrization by arc-length:

theorem reparam_by_arc_length {ι : Type*} [Fintype ι] (I : Set ℝ) [I.OrdConnected] {r : WithTop ℕ∞}
  {once_diff : 1 ≤ r} (c : ℝ → EuclideanSpace ℝ ι) (hc : ContDiffOn ℝ r c I)
  (regular : ∀ t : I, deriv c t ≠ 0) :
  ∃ (φ : ℝ → ℝ) (J : Set ℝ), J.OrdConnected ∧ MonotoneOn φ J ∧ DifferentiableOn ℝ φ J
  ∧ φ '' J = I ∧ ∀ s : J, ‖deriv (c∘φ) s‖ = 1 := sorry

How would you modify it to be fit for Mathlib?

[Aaron Liu]

Is it specific to euclidean space or does it work for any real vector space or any finite dimensional real vector space or any normed real vector space or...

[Aaron Liu]

also once_diff probably shouldn't be an implicit argument since it's impossible to infer

[Michael Novak]

Aaron Liu said:

Is it specific to euclidean space or does it with for any real vector space or any finite dimensional real vector space or any normed real vector space or...

I'm not sure, but I think this might work in any normed real vector space

[Michael Novak]

In regards to the type of the theorem, i.e, the part with all the ands, do you think that's a good style? Is there a better way of doing it?

[Sébastien Gouëzel]

In the above theorem, I would make a definition arclengthReparamFrom c x₀ which would be the arclength reparameterization sending 0 to x₀. It would be defined without any assumption on c (using junk values at points where it is not well defined). And then you would state its properties, in separate lemmas. Note that it would work at once for all intervals I containing x₀ on which the function is C^1 with nonvanishing derivative.

This would be one definition (but of a function, not of a type), and many API lemmas establishing the properties of this function. Your statement above with existentials could be a technical lemma used in the proof of the properties of arclengthReparamFrom, but not the final statement as it is hard to use as you point out.

[Michael Novak]

Thank you very much! I'll try do it

[Michael Novak]

Is this a good statement of this definition (for now I still use euclidean space, but might change it later)?

def arclengthReparamFrom {I : Set ℝ} [I.OrdConnected] {ι : Type*} [Fintype ι]
  (c : ℝ → EuclideanSpace ℝ ι) (t₀ : I) : ℝ → EuclideanSpace ℝ ι := sorry

[Michael Novak]

I'm not sure if this is what you were thinking of, but I defined it like this:

noncomputable
def arclengthReparamFrom {I : Set ℝ} [I.OrdConnected] {ι : Type*} [Fintype ι]
  (c : ℝ → EuclideanSpace ℝ ι) (t₀ : I) : ℝ → EuclideanSpace ℝ ι := by
  let ψ : ℝ → ℝ := fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖
  exact c ∘ ψ⁻¹

The problem I see with this is that I would want to prove a few properties of ψ and it's inverse, in order to prove properties of the arc-length reparametrization.

[Sébastien Gouëzel]

I would rather let arclengthReparamFrom be the function ψ⁻¹, because that's the one you will use in statements. Also, there shouldn't be an I in your definition. And what exactly do you mean by ψ⁻¹?

I'd say, start with any definition you like and start proving theorems about it. You will see soon if your definition works well or if it should be tweaked.

[Michael Novak]

Sébastien Gouëzel said:

I would rather let arclengthReparamFrom be the function ψ⁻¹, because that's the one you will use in statements. Also, there shouldn't be an I in your definition. And what exactly do you mean by ψ⁻¹?

I'd say, start with any definition you like and start proving theorems about it. You will see soon if your definition works well or if it should be tweaked.

So essentially define the parameter transformation that gives us the arc-length reparametrization, i.e: φ := ψ⁻¹. Although I would also want to use properties of ψ, so maybe I should also define that before. Not sure what I would call it, but I'll think of something.

[Michael Novak]

So this is the updated definitions I came up with. Some of the names are a bit long, especially of the first definition, because I don't know what is a good description of this term - it's essentially a construction (an important one) we usually make inside a proof, I don't think there is a term for this in of itself.

import Mathlib

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E) (t₀ : ℝ)

--This is the reversed (inverse) parameter transformation for the arc-length reparametrization
def revParamTransformForArclengthReparamFrom : ℝ → ℝ :=
  fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization
def arclengthParamTransformFrom :=
  let ψ := revParamTransformForArclengthReparamFrom c t₀
  ψ⁻¹

--an arclength reparametrization of a parametrized curve
 def arclengthReparamFrom : ℝ → E :=
  let φ := arclengthParamTransformFrom c t₀
  c ∘ φ

[Michael Rothgang]

You should use letI inside your definitions. (Otherwise, your proof terms will be more complicated and your first step in using them will be to simplify them.)

[Michael Rothgang]

I'm not sure why there's a From in all your names: can you say why?

[Michael Rothgang]

Another option for definitions is to say arcLengthParamTransformAux - for "auxiliary definition". If you add a comment that they are auxiliary, that is not rare in mathlib.

[Michael Novak]

Michael Rothgang said:

You should use letI inside your definitions. (Otherwise, your proof terms will be more complicated and your first step in using them will be to simplify them.)

Thank you very much! I never heard of letI, it seems like a great idea, and also using Aux in the name is a great idea. The reason I have From in all the definitions is that it follows the naming @Sébastien Gouëzel suggested - they are constructed from c and t₀. Do you think I should avoid it?

[Michael Novak]

These are the updated definitions:

import Mathlib

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E) (t₀ : ℝ)

/-- Auxiliary definition, this is the reversed (inverse) parameter transformation
for the arclength reparametrization. -/
def revParamTransformForArclengthReparamAux : ℝ → ℝ :=
  fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization.
def arclengthParamTransformFrom :=
  letI ψ := revParamTransformForArclengthReparamAux c t₀
  ψ⁻¹

--Unit speed / arclength reparametrization of a parametrized curve
 def arclengthReparamFrom : ℝ → E :=
  letI φ := arclengthParamTransformFrom c t₀
  c ∘ φ

[Sébastien Gouëzel]

Once you have your definitions, the only way to see if they're good or if they're flawed is to start proving theorems about them. (I have the impression there are still issues, but it's more pedagogical if you discover them yourself while trying to prove theorems)

[Michael Novak]

Sébastien Gouëzel said:

Once you have your definitions, the only way to see if they're good or if they're flawed is to start proving theorems about them. (I have the impression there are still issues, but it's more pedagogical if you discover them yourself while trying to prove theorems)

O.k, I'll try to prove some theorems now and see how it goes. Thanks a lot!

[Michael Novak]

Is there some excepted way to create a short name (maybe ψ, for example) for the expressionrevParamTransformForArclengthReparamAux c t₀? I will be using it only in some auxiliary lemmas, but it looks a bit ridiculous having to type this long expression every time, especially in the statement of a lemma.

[Sébastien Gouëzel]

Does

local notation3 "ψ" => revParamTransformForArclengthReparamAux c t₀

work for you?

[Sébastien Gouëzel]

(Also, you can/should definitely use a shorter name!)

[Michael Novak]

Sébastien Gouëzel said:

Does

local notation3 "ψ" => revParamTransformForArclengthReparamAux c t₀

work for you?

It works great, thank you very much!

[Michael Novak]

Sébastien Gouëzel said:

(Also, you can/should definitely use a shorter name!)

You are absolutely right, but I don't know what is a good short description of it. Maybe I'll have some idea later.

[Michael Rothgang]

I was thinking of arclengthParamTransformAux, by the way.

[Michael Novak]

That's a good idea, it's definitely shorter. But is it still o.k., that I use the ψ notation (only on auxiliary lemmas) when I change it?

[Michael Novak]

I have this working code so far:

import Mathlib

open MeasureTheory intervalIntegral

/-- This is a version of the first part of FTC for a function which is continuous on an interval.
    Credit to Aaron Liu. -/
theorem derivWithin_integral_of_continuousOn_interval {I : Set ℝ} [I.OrdConnected] {f : ℝ → ℝ}
  (h : ContinuousOn f I) (x₀ x : I) : HasDerivWithinAt (fun t ↦  ∫ τ in x₀..t, f τ) (f x) I x :=
  have : intervalIntegral.FTCFilter x (nhdsWithin x I) (nhdsWithin x I) := by
    refine @intervalIntegral.FTCFilter.mk x (nhdsWithin x I) (nhdsWithin x I) ⟨?_⟩ ?_ ?_ ?_
    · rw [Filter.tendsto_smallSets_iff]
      intro t ht
      rw [mem_nhdsWithin_iff_exists_mem_nhds_inter] at ht
      obtain ⟨u, hu, hut⟩ := ht
      obtain ⟨a, b, haxb, habx, habu⟩ := exists_Icc_mem_subset_of_mem_nhds hu
      have hab : Set.Icc a b ∩ I ∈ nhdsWithin x.1 I :=
        Set.inter_comm _ _ ▸ inter_mem_nhdsWithin I habx
      filter_upwards [Filter.prod_mem_prod hab hab] with (i, j) ⟨hi, hj⟩
      refine subset_trans (Set.subset_inter ?_ ?_) hut
      · refine subset_trans ?_ habu
        intro k hk
        exact ⟨hi.1.1.trans hk.1.le, hk.2.trans hj.1.2⟩
      · intro k hk
        exact Set.Icc_subset I hi.2 hj.2 (Set.Ioc_subset_Icc_self hk)
    · exact pure_le_nhdsWithin x.2
    · exact nhdsWithin_le_nhds
    · exact @Filter.inf_isMeasurablyGenerated _ _ _ _ _
        (Set.OrdConnected.measurableSet ‹_›).principal_isMeasurablyGenerated
  intervalIntegral.integral_hasDerivWithinAt_right
    ((h.mono (Set.OrdConnected.uIcc_subset ‹_› x₀.2 x.2)).intervalIntegrable)
    (h.stronglyMeasurableAtFilter_nhdsWithin (Set.OrdConnected.measurableSet ‹_›) x)
    (h.continuousWithinAt x.2)

noncomputable section

variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (c : ℝ → E)

/-- Auxiliary definition, this is the reversed (inverse) parameter transformation
for the arclength reparametrization. -/
def arclengthParamTransformAux (t₀ : ℝ): ℝ → ℝ := fun t ↦ ∫ τ in t₀..t, ‖deriv c τ‖

--This is parameter transformation used to construct the arc-length reparametrization.
def arclengthParamTransform (t₀ : ℝ) :=
  letI ψ := arclengthParamTransformAux c t₀
  ψ⁻¹

--Unit speed / arclength reparametrization of a parametrized curve
def arclengthReparamFrom (t₀ : ℝ) : ℝ → E :=
  letI φ := arclengthParamTransform c t₀
  c ∘ φ

-- We now also assume c is a parametrized curve of class Cʳ from the interval I, r≥1.
variable (I : Set ℝ) [I.OrdConnected] (hI : IsOpen I) {r : WithTop ℕ∞}
  (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I) (t₀ : I)

--Auxilary definition, so we don't have to type the full long expression everytime
local notation3 "ψ" => arclengthParamTransformAux c t₀

/-- An auxiliary lemma giving us the derivitive of the reverse parameter transformation on I. -/
lemma rev_param_transform_deriv_eq_aux (t : I) (once_diff : 1 ≤ r) (hc : ContDiffOn ℝ r c I)
  (hI : IsOpen I) : HasDerivWithinAt ψ ‖deriv c t‖ I t := by
  have cont_speed : ContinuousOn (fun t ↦ ‖deriv c t‖) I :=
    Continuous.comp_continuousOn' continuous_norm (hc.continuousOn_deriv_of_isOpen hI once_diff)
  unfold arclengthParamTransformAux
  exact derivWithin_integral_of_continuousOn_interval cont_speed t₀ t

There are two issues that I wanted to ask about:
The first one is a bit weird - when I remove the assumptions once_diff, hc, hI from the statement of the last lemma, lean doesn't recognize these names inside the proof even though they already appear in the variable command above. Why is that? Is there some better way to do it which avoids repetition?
The second issue is about making a strategic decision about the use of intervals in the project. In the last lemma for example I assumed also that the interval I is open because I found a theorem on Mathlib that helped me get what I want which required I to be open. I might try to drop now the assumption that I is open and prove the lemma without it, but maybe it could be a good idea to just always assume that the interval is open to make life easier. Will that be acceptable if I want this code to eventually get into Mathlib? And do you think it will really be very helpful to assume the interval is open? Another option is to use a normal closed intervals as Michael Rothgang suggested previously, but it seems to me that this choice will still have the issue of dealing with edge points for which there isn't a neighborhood inside the interval.

[Aaron Liu]

The reason you need the interval to be open is you are using deriv, which looks at the neighborhood of whatever point you give it, and this neighborhood might go outside the interval if it is not open.

[Aaron Liu]

Michael Novak said:

The first one is a bit weird - when I remove the assumptions once_diff, hc, hI from the statement of the last lemma, lean doesn't recognize these names inside the proof even though they already appear in the variable command above. Why is that? Is there some better way to do it which avoids repetition?

This is because variables are not included into a theorem unless they are "relevant", messing appears in the statement or if a typeclass relating to a relevant variable. This is so that you don't accidentally change the statement of a theorem by messing around with its proof. You can get around it by doing include once_diff hc hI.

[Aaron Liu]

Surely you can get some derivative information from hc, so you don't have to use deriv?

[Michael Novak]

Aaron Liu said:

The reason you need the interval to be open is you are using deriv, which looks at the neighborhood of whatever point you give it, and this neighborhood might go outside the interval if it is not open.

Yes, I thought of using derivWithin, but then I will also need the original definition of arclengthParamTransformAux and the subsequent definitions to include the interval I, and I was told not to include it and also the theorem for the continuity of derivWithin require another assumption which is not completely clear to me, but if you think it's better to switch to derivWithin I'll look into it in more detail.

[Aaron Liu]

I don't think it should require another assumption

[Aaron Liu]

I'll take a look

[Aaron Liu]

oh it wants the derivative to be unique?

[Michael Novak]

Aaron Liu said:

I don't think it should require another assumption

The theorem I'm refering to is ContDiffOn.continuousOn_derivWithin, which also require this: (hs : UniqueDiffOn 𝕜 s₂). Do you think it's easy to show?

[Aaron Liu]

oh that why it wants the derivative to be unique

[Michael Novak]

Aaron Liu said:

oh it wants the derivative to be unique?

yes

[Aaron Liu]

I'll think about it

[Michael Novak]

Aaron Liu said:

Michael Novak said:

The first one is a bit weird - when I remove the assumptions once_diff, hc, hI from the statement of the last lemma, lean doesn't recognize these names inside the proof even though they already appear in the variable command above. Why is that? Is there some better way to do it which avoids repetition?

This is because variables are not included into a theorem unless they are "relevant", messing appears in the statement or if a typeclass relating to a relevant variable. This is so that you don't accidentally change the statement of a theorem by messing around with its proof. You can get around it by doing include once_diff hc hI.

I'm not sure I understand it completely. If these are assumptions about some variables like c and I which appear in the theorem statement, why are they not included?

[Aaron Liu]

They are not mentioned in the statement and they are not typeclass assumptions

[Michael Novak]

Why doesn't this HasDerivWithinAt ψ ‖deriv c t‖ I t count as a mention of c and I?

[Riccardo Brasca]

I didn't read everything, but mentioning I is not enough to have hI automatically included (it would work if the statement mention hI explicitly).

[Michael Novak]

Riccardo Brasca said:

I didn't read everything, but mentioning I is not enough to have hI automatically included (it would work if the statement mention hI explicitly).

Oh, that makes sense, thank you very much! And also thank you @Aaron Liu for trying to explain me that!

[Aaron Liu]

So the reason they want the derivative to be unique is that derivWithin picks out an arbitrary derivative and ContDiff only asserts the existence of a continuous derivative

[Aaron Liu]

so if the derivative isn't unique you can have the arbitrary derivative not the same as the continuous derivative

[Aaron Liu]

I claim you shouldn't be picking an arbitrary derivative with derivWithin and you should instead pick an arbitrary continuous derivative

[Michael Novak]

This sounds very weird to me. As far as I know the derivative is a limit and limits are unique. What do I miss?

[Aaron Liu]

for example, if your interval is a singleton point what's the derivative?

[Aaron Liu]

Michael Novak said:

As far as I know the derivative is a limit and limits are unique.

In mathlib a function f is said to have a derivative f' at x within a set s if f y - f x - f' * (y - x) as a function of y grows as little o of y - x at the neighborhood of x within s.

[Michael Novak]

I'm not sure, maybe it's not defined because there isn't an open subset (in the bigger normed space) of the point which is contained in the singleton. Now that I think of it, when I learned the general definition of the derivative of a multivariable function it was defined always when the domain of the function is an open set in the bigger normed space. Maybe Mathlib does something more general I'm not sure.

[Michael Rothgang]

Yes, that is what's happening: mathlib's definition docs#DifferentiableOn never requires the set to be open --- which is why considers docs#DifferentiableWithinAt. (For open sets, DifferentiableWithinAt and DifferentiableAt are equivalent.)

[Aaron Liu]

You can read docs#HasFDerivAtFilter

[Michael Novak]

Aaron Liu said:

Michael Novak said:

As far as I know the derivative is a limit and limits are unique.

In mathlib a function f is said to have a derivative f' at x within a set s if f y - f x - f' * (y - x) as a function of y grows as little o of y - x at the neighborhood of x within s.

I thought about it, it's a bit confusing, so I'm really not sure, but I think that according to this definition, the answer to your question about the case of a singleton is that any function f' would satisfy it vacuously (if we unfold the definition with epsilon and delta, then there isn't any point in any neighborhood of x without x itself within s). So if I understood this correctly I understand now the problem that the derivative could be not unique. But if we eliminate the case of a singleton is it still possible to get a non-unique derivative on an interval?

[Sébastien Gouëzel]

The singleton is the only problematic case. See docs#uniqueDiffOn_Icc and the lemmas around.

[Aaron Liu]

For a set of real numbera the derivative is always unique at non-isolated points

[Michael Novak]

So should I include an assumption that the interval I includes two different points and solve the issue in this way?

[Aaron Liu]

I think you should use something other than derivWithin that gets you a derivative which is automatically continuous

[Michael Novak]

Do you mean I should use docs#HasFDerivAtFilter ? If that's the best way to do it then I will try it. My main problem is that I barely understand what is a Filter (only read the definition in Wikipedia). Do you have a link for some information about using filters and related concepts in Mathlib?

[Aaron Liu]

not what I meant but I encourage you to learn about filters

[Michael Novak]

Could you elaborate what did you mean? (I will also try to lean about filters anyways :joy: ).

[Sébastien Gouëzel]

At a point x different from t0 you could use derivWithin (uIcc t0 x), and at t0 use deriv, for example.

[Aaron Liu]

ContDiffOn says there exists a sequence of multilinear maps whose first few terms form continuous derivatives for your given function within a certain set

[Aaron Liu]

so just take the derivative from there, and it's continuous by assumption

[Aaron Liu]

no need to use derivWithin that gives you a derivative not guaranteed to be continuous

[Michael Novak]

Thank you very much! I'll try this.

[Sébastien Gouëzel]

Aaron, inside intervals (different from a single point) the derivative is unique, and therefore continuous. The issue is not there. The issue is if you want something which works regardless of the interval I that you want to reparameterize.
@Michael Novak, thinking again about it, I think your life will be much easier if you allow yourself to let the reparam depend on the interval, or if you just take open intervals (in which case you can use the plain deriv). This really depends on the theorems you want to formalize, though.

[Michael Novak]

Sébastien Gouëzel said:

Aaron, inside intervals (different from a single point) the derivative is unique, and therefore continuous. The issue is not there. The issue is if you want something which works regardless of the interval I that you want to reparameterize.
Michael Novak, thinking again about it, I think your life will be much easier if you allow yourself to let the reparam depend on the interval, or if you just take open intervals (in which case you can use the plain deriv). This really depends on the theorems you want to formalize, though.

Your solution totally makes sense to me as well. The theorems I want to to formalize should work on any intervals, I'm not sure how much assuming the interval is open will help, certainly adding assumptions could not make life harder, but on the other hand as I understand it you want to be as general as you can in Mathlib, but I really don't have much experience with Mathlib as you, so I'm not sure. I'll wait to see what @Aaron Liu thinks.