Zulip Chat Archive

Stream: maths

Topic: Multiple differentiability

Sebastien Gouezel (Apr 28 2019 at 20:09):

I have a universe polymorphism question in the definition of multiple differentiability. The definition I have currently is

def times_cont_diff_on : ∀n : with_top ℕ, ∀{E:Type v}, ∀{F:Type v},
  ∀[hE:normed_space k E], ∀[hF:normed_space k F], ∀f : E→F, ∀s : set E, Prop
| (some 0)     := λE F hE hF f s, by { resetI, exact continuous_on f s }
| (some (n+1)) := λE F hE hF f s, by { resetI,
    exact fdifferentiable_on k f s ∧ times_cont_diff_on n (λx, fderiv_at_within k f x s) s }
| none         := λE F hE hF f s, by { resetI,
    exact (∀n:ℕ, times_cont_diff_on (n : with_top ℕ) f s) }
using_well_founded {
  rel_tac := λ_ _, `[exact ⟨_, with_top.well_founded_lt nat.lt_wf⟩],
  dec_tac := `[apply with_top.coe_lt_top <|> apply with_top.some_lt_some.2 (lt_add_one _)] }

In this definition, I define inductively what it means for a function f : E -> F to be n times continuously differentiable on a set s. For n=0, it is just continuous. For n+1, it means that f is differentiable, and its derivative is n times continuously differentiable (but now from the space E to the space E ->L[k] F of bounded linear maps from E to F). If E and F live in the same universe v, everything is fine. But if E lives in v and F in w, then E ->L[k] F lives in max v w and my induction is not correct any more. The options I see:
* keep E and F in the same universe and be content with it.
* have an auxiliary definition where E is in v and F in max v w. And use it for the inductive step of the general case. Inductions become much more cumbersome (statements should first be proved for the auxiliary definition, and then the main one).
* Or some better trick I don't know.

Comments welcome!

Kevin Buzzard (Apr 28 2019 at 20:13):

My comment is that I spent 25 years of my life doing mathematics in one universe and I never had any problems whatsover. I know they tell us to be universe polymorphic here but I would like to interpret that as "just use one universe u". I was encouraged by the CS people to have objects in one universe and morphisms in a different universe in category theory -- because why not? -- and I think it just makes a terrible mess of things. I hereby propose that if you're actually doing sensible mathematics then you just stick to one universe until someone gives you a really good reason not to. I am yet to see a convincing argument for using more than one universe in mathematics.

Sebastien Gouezel (Apr 28 2019 at 20:15):

My main problem with this is that, if someone starts a file with variables {E : Type*} {F : Type*} and tries to define a C^2 map from E to F, then Lean complains with a hard to understand error message. But from the mathematical point of view, I am also completely happy to do everything in one universe (or even in Type).

Kevin Buzzard (Apr 28 2019 at 20:16):

So they should be doing maths in one universe too!

Kevin Buzzard (Apr 28 2019 at 20:17):

When I made schemes I made them all in Type. But when Ramon made them, he switched to a universe polymorphic set-up.

Kevin Buzzard (Apr 28 2019 at 20:18):

I tried using the category theory library and I had universe identification nightmares. Every category I had was either a large category (like rings) or a small category (like some graph of a directed system coming from nhds x). I never needed more than one universe. I don't get why they always want us to use lots of universes. This is maths!

Sebastien Gouezel (Apr 28 2019 at 20:21):

OK, let's go for E and F in the same universe, unless someone complains.

Kevin Buzzard (Apr 28 2019 at 20:22):

It would be interesting to hear what the CS people have to say. For me, the fact that it causes you trouble being multiply universe polymorphic in a situation where there is mathematically no foundational issue at all, means that being multiply universe polymorphic is the wrong idea in mathematics. Sure use one universe. But the set theorists always ask me why I need more than one (this happened in Freiburg this week and it's not the first time).

Kevin Buzzard (Apr 28 2019 at 20:24):

One of my plans for later on is to refactor the schemes project using @Scott Morrison 's category theory library, and I would like to start with using only small and large categories, and one universe only. For me it will then be easy to do universe unification by hand because I know exactly which categories are small and which ones are large.

Kevin Buzzard (Apr 28 2019 at 20:28):

I had universe unification issues with perfectoid spaces when we tried using categories and it put me off to an extent that I decided not to use them, and instead try to import them into Ramon's scheme project later. I really want to see category theory being used more and next time I am absolutely sticking with one universe.

Johan Commelin (Apr 29 2019 at 03:08):

@Sebastien Gouezel Thanks for working on this. The last time there was discussion about this, I think you said you were using enat. Now I see that you are using with_top nat. Can you comment on the change? I was thinking enat might be easier for applications (because you avoid the infty-case).

Sebastien Gouezel (Apr 29 2019 at 06:09):

I tried first with enat, but since the definition and the proofs are really inductive, it turned out to be much more convenient in with_top nat. I wouldn't know how to write the definition in enat, in fact!

Johan Commelin (Apr 29 2019 at 06:49):

@Johannes Hölzl You said that a coinductive approach might be a good idea. Could you help us out?

Mario Carneiro (Apr 29 2019 at 06:51):

I think this definition should be done in two parts rather than using a messy recursion. Define what C^k means first for k : nat, and then define it for k : enat by extension

Sebastien Gouezel (Apr 29 2019 at 07:01):

That's what I had done first. But then it means that all proofs have to be done twice, first for finite differentiability using nat induction, and then for enat. With two different lemmas each time, the auxiliary one on nat and then the main one on enat. I got tired of this after ten identical repetitions of proofs, then I tried the inductive definition in with_top nat and it turned out to be completely smooth. Here is a random proof in this file:

lemma times_cont_diff_on.congr_mono {n : with_top ℕ} {s : set E} (H : times_cont_diff_on k n f s)
  (hs : unique_diff_on k s₁) (h : ∀x ∈ s₁, f₁ x = f x) (h₁ : s₁ ⊆ s) :
  times_cont_diff_on k n f₁ s₁ :=
begin
  tactic.unfreeze_local_instances,
  induction n using with_top_nat_induction with n IH Itop generalizing F,
  { exact continuous_on.congr_mono H h h₁ },
  { refine ⟨fdifferentiable_on.congr_mono H.1 h h₁, IH H.2 (λx hx, _)⟩,
    apply differentiable_at_within.fderiv_at_within_congr_mono
      (H.1 x (h₁ hx)) h (h x hx) (hs x hx) h₁, },
  { assume n, exact Itop n (H n) h }
end

It used to be much more tedious with nat induction and then enat extension.

Mario Carneiro (Apr 29 2019 at 07:05):

wouldn't it be the same with the appropriate induction lemma?

Sebastien Gouezel (Apr 29 2019 at 07:09):

I had more difficulties with the two definitions on nat and enat as things were less defeq, so I had to do more things by hand. But in retrospect I don't see why this was the case, so maybe I'll try again. In the end, both definitions, if well crafted, should give the same proofs!

Mario Carneiro (Apr 29 2019 at 07:09):

I think there are actually two definitions here, though, and mixing them is part of the problem for this question

Mario Carneiro (Apr 29 2019 at 07:10):

For your C^k universe problem, I think you want to define "L is the k times differential of f at x"

Mario Carneiro (Apr 29 2019 at 07:10):

which lives in some space like E^k ->l F

Mario Carneiro (Apr 29 2019 at 07:12):

You could either define that recursively or inductively. If you do it recursively then since you want that space to live in max u v, at k = 0 it's ulift F or something equivalent to it

Mario Carneiro (Apr 29 2019 at 07:14):

Actually, I guess a witness for C^k requires a whole list of different E^k' ->l F functions (for k' <= k)?

Sebastien Gouezel (Apr 29 2019 at 07:14):

No, the k-th derivative lives in a much more complicated space. Either E ->l (E ->l (E ->l ... F)))), or the space of k-linear maps from E^k to F (but the natural space from the inductive definition is the first one). In general, one never uses the k-th derivative beyond k=2, so I am really going for an existence result.

Mario Carneiro (Apr 29 2019 at 07:15):

Sure, but I still think being able to name the objects is useful

Mario Carneiro (Apr 29 2019 at 07:16):

When I say E^k ->l F I really mean what you said, it's a new definition like E ->l ... ->l F

Mario Carneiro (Apr 29 2019 at 07:16):

I think that can be expressed as a unary function though, from the tensor product space

Sebastien Gouezel (Apr 29 2019 at 07:17):

For instance, when you prove that the composition of C^k functions is C^k, you definitely don't want to exhibit the derivative!

Mario Carneiro (Apr 29 2019 at 07:17):

I'm not convinced that's true... we probably want the appropriate operators on tensors anyway

Sebastien Gouezel (Apr 29 2019 at 07:18):

With tensor products, there are difficulties here as we are really talking about normed spaces, and there are many possible norms on a tensor product, that are not equivalent in general.

Mario Carneiro (Apr 29 2019 at 07:19):

this new definition gives you the opportunity to pick the right one, though

Mario Carneiro (Apr 29 2019 at 07:19):

I admit it's not the approach that leads to the least additional work

Mario Carneiro (Apr 29 2019 at 07:20):

but I'm trying to gauge if this extra work is worth it for library building reasons

Sebastien Gouezel (Apr 29 2019 at 07:25):

There is no "right" norm on tensor products, unfortunately. I just checked https://en.wikipedia.org/wiki/Topological_tensor_product, which starts with the sentence "the theory is notoriously subtle" :)

Johan Commelin (Apr 29 2019 at 07:29):

We need the "dangerous bend" emoji of Bourbaki/Knuth

Mario Carneiro (Apr 29 2019 at 07:31):

The first questions that come to mind are: does it matter which of these norms we take? Apparently some norm is definable, and there is some space of them, but maybe they are all topologically equivalent or have the same little O sets

Mario Carneiro (Apr 29 2019 at 07:34):

Assuming these issues of the tensor product cannot be resolved, it is still possible to define the space E ^[n]->l F (or whatever notation) via iteration of E ->l on ulift F

Mario Carneiro (Apr 29 2019 at 07:35):

and then given f : E ^[n]->l F and x : E^n you can define f x : F

Mario Carneiro (Apr 29 2019 at 07:36):

That is, you can still treat it like the space E^n -> F but its norm is derived from E -> ... -> F

Johannes Hölzl (Apr 29 2019 at 19:54):

The coinductive definition would look like this:

coinductive C : enat → (ℝ → ℝ) → bool
| zero : ∀f, continuous f → C 0 f
| deriv : ∀n f f', C n f → derivative f f' → C (n + 1) f'

So we get the 0 case, the +1 case and by coinduction the infinite (ω) case.

Kevin Buzzard (Apr 29 2019 at 19:55):

@Johannes Hölzl what do you think about the claim that mathematicians may as well just work in Type u and not ever use more than one universe in their work?

Johannes Hölzl (Apr 29 2019 at 20:05):

You mean work in Type 0? I'm coming from a HOL background, and I see that everything can be done in Type 0 (AFAIK arithmetic even in second-order logic) . But it is a annoying restriction which is hard to work around.I would prefer two different universes for E and F. We have the problem already for dim, where many rules are restricted to be in one universe (saving some ulift etc.).

Kevin Buzzard (Apr 29 2019 at 20:10):

I know that you guys are not a fan of Type 0. I was proposing Type u as a way of meeting you in the middle. I don't want to ever consider a category with objects in some universe u and morphisms in some random unrelated universe v. These things do not even show up in mathematics -- there is always a relation between u and v (small categories or large ones). But the "maximally universe polymorphic" mantra coming from the CS people who know type theory says that this is how it should be done. Mathematicians are running into issues with this when more than one universe is involved.

Jesse Michael Han (Apr 29 2019 at 20:15):

a concrete example which came up in discussion is Lean's treatment of ordinals, which, being isomorphism classes of well-ordered types, live one universe level up. Johannes mentioned that it's not possible to do this in just Type 0, and that some workaround must be implemented.

i think mathematicians would prefer being able to rigorously think of ordinals as giant equivalence classes whenever it's convenient. (arguably this falls under the scope of kevin's argument---i haven't seen an example where more than two type universes are needed... yet)

Johannes Hölzl (Apr 29 2019 at 20:19):

Well as a computer scientist I also only want to work in Type u (or even better in Type 0). Or better: as a user I only want to work in Type 0 (and in the worst case in a fixed type universe u).

But as a library developer were other people should use and apply my theorems I know that for some cases different type universes are neccesary, and it is usually very hard to introduce them afterwards.

So this is not a question between CS and math. It is a question between easy but restricted and harder but in difficult cases easier to apply.

Kevin Buzzard (Apr 29 2019 at 20:20):

But if we did the entire corpus of mathematics with only one universe (I don't know if you realise this but this is what is done in practice) then no mathematician would ever notice if our maths libraries only had one universe in.

Johannes Hölzl (Apr 29 2019 at 20:36):

Kevin there is a difference between doing everything in one type universe from the perspective of not doing it in a formal way. and doing it in one type universe from the perspective of doing it formally in DTT.

Kevin Buzzard (Apr 29 2019 at 20:37):

I can believe you, but I don't really understand this difference properly.

Kevin Buzzard (Apr 29 2019 at 20:38):

All I know is that if Sebastien runs into issues like the above issue and then has to work hard to get around things, and there are no set-theoretic issues, then in my opinion he is being too universe-polymorphic for mathematics.

Johannes Hölzl (Apr 29 2019 at 20:41):

Or we need a better understanding / methods / tools / syntax to handle the universe polymorphism. This could also go in the direction that we write a constant with only one universe parameter, but have some "magical" tools which generalize this parameter into multiple different ones.

Johannes Hölzl (Apr 29 2019 at 20:44):

But currently I don't see a good solution here. A solution is surely to go with one parameter and when somebody runs into a problem with multiple parameters they need to deal with it (including rewriting the theory)