parametrised curves

Stream: maths

[Kevin Buzzard]

i occasionally ask about differential geometry in Lean 3 because I run into people who ask me about it (Imperial has got a lot of geometers) and it's a part of the library which I know very little about. Here are the first two pages from an undergraduate course at Imperial:

cands1.png
cands2.png

An undergraduate asked me whether this sort of thing is in scope yet for a project for my course. I tried defining $\phi:[0,1]\to\R^2$ by $\phi(t)=(cos(t),sin(t))$ but then I couldn't take its derivative because the source wasn't a vector space. I thought I'd ask here before going any further. Should I just define the map on the whole of the reals? If I do that, will I (I say I but I mean @Ines Wright ) be able to get as far as defining the length $L$, or are there still missing pieces? PS I am assuming that this stuff isn't done already in mathlib? We seem to have an entire course studying the basic differential geometry of curves and surfaces in $\R^3$.

[Rémi Bottinelli]

I assume you knowbounded_variation has got length in terms of supremums? but I think it's not been shown equivalent to the "integral of abs of derivative" formulation

[Oliver Nash]

There are at least two issues here:

1. Derivatives of functions whose domain / codomain is a subset of a normed vector space
2. Definitions and results about arc length of curves

As to 1, we can absolutely do this. I believe the options are:
(a) Use manifold API
(b) Extend your domain (using junk values) as you suggest
(c) Create a special API for this situation (distantly related to https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Calculus.20on.20the.20circle)

As to 2, I think we don't really have anything yet, but it's not so far away. One part of the story is #18375 and the other part is the integral of the length of the tangent vector.

[Oliver Nash]

This is probably all "post port" work.

[Kevin Buzzard]

A mathematical question I have about extending the domain using junk values is that there's a claim that the function has to be smooth, and this seems to include smoothness at the endpoints. If we extend by junk and then ask for smoothness at the endpoints, presumably the junk values will affect this! I don't know how horrible a function on $[a,b)$ can be which is smooth on $(a,b)$ and continuous at $a$.

[Sebastien Gouezel]

We have a notion of smoothness within a set (see docs#differentiable_on or docs#deriv_within) designed precisely for this kind of situation.

[Sebastien Gouezel]

Using a function defined globally, but only caring about its values inside [a, b], is definitely the mathliby way to go here.

[Sebastien Gouezel]

I.e., the API is designed for that and should work out transparently.

[Kevin Buzzard]

I see, so I'm just exposing my ignorance of the API here. So just to be clear, if $f:\R\to\R$ is defined to be $0$ for $x<0$ and $1$ for $x\geq0$, then you're telling me that differentiable_on \R f [0,1] is true, because values outside $[0,1]$ are ignored.

[Kevin Buzzard]

Oh, I guess $x\sin(1/x)$ is a good example of the kind of thing I was worried about (differentiable away from 0, scary at 0)

[Kevin Buzzard]

OK here's a challenge question then: is this feasible, given what we have?

import analysis.calculus.parametric_integral

noncomputable def φ₁ : ℝ → ℝ × ℝ × ℝ :=
λ x, (real.sin x, x^4+37*x^2+1, abs x)

example : cont_diff_on ℝ ⊤ φ₁ (set.Icc 0 1) :=
begin
  sorry,
end

I don't know if we have API to break the question down into individual factors, and I don't know if I'm supposed to be proving real.sin is smooth by proving by induction on n that its n'th derivative is continuous or whether I'm supposed to be doing something else. Is there API for this? Is the API easily constructible if not?

[Heather Macbeth]

@Kevin Buzzard

import analysis.calculus.parametric_integral
import analysis.special_functions.trigonometric.deriv

open real

noncomputable def φ₁ : ℝ → ℝ × ℝ × ℝ :=
λ x, (real.sin x, x^4+37*x^2+1, abs x)

example : cont_diff_on ℝ ⊤ φ₁ (set.Icc 0 1) :=
cont_diff_sin.cont_diff_on.prod $
  (((cont_diff_id.pow 4).add (cont_diff_const.mul (cont_diff_id.pow 2))).add
  cont_diff_const).cont_diff_on.prod $
  cont_diff_on_id.congr (λ x hx, abs_of_nonneg hx.1)

There are tactics continuity, measurability but I don't think there is a smoothness yet.

[Kevin Buzzard]

Thanks so much! I'll digest and see if I can make it onto page 2 :-)

[Kevin Buzzard]

Now I've had the chance to look at this I'm quite annoyed with myself. The reason I asked the question was that I was stumped at the first line -- I had found cont_diff_on_prod but this was about finset.prod and after some looking and failing to notice cont_diff_on.prod I decided to post. Thanks a lot! This has been very instructive. Am I right in thinking that one (i.e. @Ines Wright ) could somehow use apply_rules to make a tactic which could auto-generate most of this argument? I have a very limited understanding of what apply_rules is/does.

[Moritz Doll]

It will be trivial to implement smoothness in Lean 4 using aesop, so we should just continue with the port.

[Kevin Buzzard]

Yes, this I completely understand, but this is specifically for a student who is doing my course so is contractually obliged to stick with Lean 3 and write me a project within the next few weeks.

[Kevin Buzzard]

My second and final mathematical question about these curves is about taking derivatives. What we'd want to do is get the linear map $D_x\phi$ corresponding to the derivative of a smooth $\phi:[a,b]\to\R^n$ at $x\in [a,b]$. Looking at the notes, one thing which we'd need would be that if $\alpha:[a,b]\to[c,d]$ is a smooth bijection and $D\alpha_x\ne0$ on $[a,b]$, then the inverse bijection $\alpha^{-1}$ is smooth and $D(\alpha^{-1})_{\alpha(x)}=1/(D\alpha_x)$ (assuming this is true, especially at the endpoints, where my understanding is poor). Is this also relatively straightforward given what we have in mathlib3?

[Kevin Buzzard]

Here's a formalisation. Is this true? If so, is it easy or hard given what we have?

import analysis.special_functions.trigonometric.deriv

open real

/- Let `a≤b` and `c≤d` be reals. Let φ : [a,b] → [c,d] and ψ : [c,d] → [a,b]
  be inverse bijections, and assume φ is smooth and φ' is nonvanishing
  on [a,b]. Then ψ is smooth and ψ' is nonvanishing on [c,d],
  and ψ'(y)*φ'(ψ(y))=1.
-/
example (φ : ℝ → ℝ) (ψ : ℝ → ℝ) (a b c d : ℝ)
  (hab : a ≤ b) (hcd : c ≤ d) (hφ : ∀ x, x ∈ set.Icc a b → φ x ∈ set.Icc c d)
  (hψ : ∀ y, y ∈ set.Icc c d → ψ y ∈ set.Icc a b)
  (left_inv : ∀ x, x ∈ set.Icc a b → ψ (φ x) = x)
  (right_inv : ∀ y, y ∈ set.Icc c d → φ (ψ y) = y)
  (hφdiff : cont_diff_on ℝ ⊤ φ (set.Icc a b))
  (hφregular : ∀ x, x ∈ set.Icc a b → fderiv ℝ φ x ≠ 0) :
  cont_diff_on ℝ ⊤ ψ (set.Icc c d) ∧
  ∀ y, y ∈ set.Icc c d → ∀ z, fderiv ℝ ψ y (fderiv ℝ φ (ψ(y)) z) = z :=
sorry

[Heather Macbeth]

@Kevin Buzzard This is a toy case of the inverse function theorem, but you might need to glue together several related results. Some starting points: docs#cont_diff_at.to_local_inverse, docs#has_strict_fderiv_at.local_inverse_unique

[Heather Macbeth]

If you want to construct the inverse, and you want to avoid invoking the inverse function theorem on Banach spaces, you can also route through order theory for a purely one-dimensional construction. Look at the construction of docs#real.arctan for a model; it uses docs#strict_mono_on.order_iso