How to use R^n ?

Stream: new members

[Michael Novak]

I tried using this notation

variable {n : \N} (x  :  \R\^n)

and I got some error. I'm not sure if the error was because of a different mistake or because this is not an excepted notation. If it is not an excepted notation, then what is the excepted notation? should I maybe write instead:

variable {n : \N} (x  : Fin n \to \R)

?

[Jihoon Hyun]

Are you looking for docs#EuclideanSpace ?

[Michael Novak]

Technically I do use it as a euclidean space, but is it necessary to write EuclideanSpace R (Fin n)? Couldn't I use class inference when I need to use the fact that it is also an instance of a euclidean space?

[Moritz Doll]

The answer to this question is surprisingly complicated: depending on what you really want to do, you might want to phrase things for an abstract normed or inner product space). So the real question is what do you want to do?

[Michael Novak]

I want to make variable of a parametrized curve that I will use in the next few theorems. I began writing this line (I still didn't add the fact that c is continuous):

variable  {I : Set ℝ}  [I.OrdConnected]  {n : ℕ}  (c : I → Fin n → ℝ)

Is that a good way of doing it?

[Michael Rothgang]

Short answer, as on my phone:
You probably want EuclideanSpace as codomain (its norm is the you want, unlike Fin n -> R).
Usually, I would expect Set.ICC, Set.Ioo or similar as domain. (Mathlib knows that order-connected sets in R are precisely intervals.)

[Michael Rothgang]

However, you should do something yet different: make the domain R and assume ContinuousOn c (Set.Icc a b) instead

[Michael Rothgang]

Basically, assign an arbitrary value to your curve outside the interval (the keyword to search for is "junk value pattern", we do this a lot in formalisation).

[Michael Rothgang]

Having the domain a normed space will make speaking about differentiability a lot easier to work with!

[Michael Novak]

Why should I restrict the "real values" of c to be only on a closed interval? In the book I'm using, parametrized curves are defined on any interval

[Michael Rothgang]

I'm talking about extending the domain of definition (not restricting).Sorry, misread: you can also use Set.Ioo, etc; that's fine.

[Michael Rothgang]

(deleted)

[Michael Rothgang]

(deleted)

[Michael Novak]

So is this a good way to do it?

 variable {I : Set ℝ} [I.OrdConnected] {n : ℕ} (c : ℝ → EuclideanSpace ℝ (Fin n)){ContinuousOn c I}

[Aaron Liu]

You need to name your ContinuousOn hypothesis

[Michael Novak]

Your are right, thank you! Now that I think about it, is it a good way have so much assumptions? Because I would also want to add that c is of class C^r for r >=2, so it's getting a bit long. Maybe I should define a structure / class of a parametrized curve?

[Aaron Liu]

docs#ContDiffOn

[Michael Novak]

O.k, I think you are right there's probably no need to define a new structure. Thank you very much! So, I changed the line to this now:

variable {I : Set ℝ}[I.OrdConnected]{n : ℕ}(c : ℝ → EuclideanSpace ℝ (Fin n)){r : WithTop ℕ∞}{hc : ContDiffOn ℝ r c I}

[Michael Rothgang]

Purely in terms of style, I'd write this as follows:

variable {I : Set ℝ} [I.OrdConnected] {ι : Type*} [Fintype ι] {r : WithTop ℕ∞}
  {c : ℝ → EuclideanSpace ℝ ι} (hc : ContDiffOn ℝ r c I)

Instead of using Fin n, you can equally well use any finite type (and this should not make your formalisation much harder). Mathlib would do this anyway. I've also broken your long line, and changed the variable explicitness. You probably want c to be implicit and hc to be explicit, not the other way around: in applications, you may need to prove differentiability (and c can be inferred from such a hypothesis).

[Michael Rothgang]

Using any OrdConnected set as domain still feels unusual to me: indeed, this is quite rare in mathlib. You will many more lemmas formulated for e.g. Set.Ioo or Set.Icc (or both). (This includes the existence and uniqueness of ODE solutions, for example --- if I remember correctly, those feature in the proof of Frenet's formulas.)

I understand your wish to be fully general, but I'm not sure if this is premature optimisation. Do you really use curves defined on e.g. intervals [1, 2) for what you'll be working on? (For e.g. Frénet's formula, I believe you mostly don't.)

[Michael Rothgang]

I'm not sure if there's a good solution yet to avoid duplicating one theorem 9 times (once for each kind of interval). For now, just proving the version(s) you actually need can get you a long way. Proving it once and adding a comment that further versions would be easy to add sounds totally fine to me.

[Michael Novak]

Thank you very much for the corrected line and for the other comments! Actually there isn't any use of differential equations in the proof of Frenet equations, at least not for plane curves, which I start with and I don't really understand why do you think it could be problematic to work with a general interval, for example in Frenet equations we are just talking about very simple equations involving the first and second derivative of the parametrized curve, the curvature and the derivative of the normal vector field - all of which are functions defined in each point of the interval and it doesn't really matter what sort of interval it is. Am I'm missing something? Could we be talking about different formulations? I'm following the book "Elementary Differential Geometry" by Christian Bar, I could send you a pdf if you want to see.

[Michael Rothgang]

I was thinking of theorems of the kind "there is a unique parametrised curve in R³ with prescribed initial point, velocity, curvature and torsion" --- which use Frenet's equations and the uniqueness of solutions of ODEs. Sure, mathematically all of this should work over any interval. I'm talking about how are things set up in mathlib.

[Michael Rothgang]

That said, I don't mind seeing a .pdf of Bär's book to double-check; the last time I saw this particular material has been a while ago.

[Michael Novak]

Michael Rothgang said:

I was thinking of theorems of the kind "there is a unique parametrised curve in R³ with prescribed initial point, velocity, curvature and torsion" --- which use Frenet's equations and the uniqueness of solutions of ODEs. Sure, mathematically all of this should work over any interval. I'm talking about how are things set up in mathlib.

Oh, we saw this theorem for plane curves, I think it's called the fundamental theorem of plane curves, although this specific theorem wasn't on Bär's book, it was on a different book which only deals with plane curves, and they didn't justified the uniqueness by a theorems about differential equations, but they basically presented the argument for uniqueness you would see in a course on differential equations. I would probably also want to prove this theorem as well later.

[Michael Novak]

Michael Rothgang said:

That said, I don't mind seeing a .pdf of Bär's book to double-check; the last time I saw this particular material has been a while ago.

This is Bär's book:
elementary-differential-geometry-chrisitian-bar.pdf
and this is the other book only on plane curves:
differential-geometry-of-plane-curves.pdf