has_sum / has_fderiv

Stream: maths

[Sebastien Gouezel]

The relevant definitions for infinite series are the following: has_sum u means that u is summable, is_sum u s means that u is summable and its sum is s, and tsum u is the sum of u if it is summable, and something arbitrary otherwise. It turns out to be convenient to have these three different tools. Especially in calculations, one uses tsum u, and to apply theorems to them one checks has_sum ...

For derivatives, one has currently has_fderiv f f'to say that the function f has the derivative f' (with many variations: at a point, within a set, and so on, which is I think important and handy). But I am bothered by the discrepancy in terminology: wouldn't it be better to call this is_fderiv f f' to be coherent with sums, and to introduce has_fderiv and fderiv? @Jeremy Avigad, any thoughts about this?

[Sebastien Gouezel]

I am asking because I had a first go at manifolds (by the way, comments on https://github.com/sgouezel/mathlib/blob/9974cbcd20f6b4a8173d239a45d8bca0b0bd04c5/src/geometry/manifolds/basic.lean#L809 are very much welcome), and I would need to define C^k functions. For this, fderiv looks like the way to go.

[Johan Commelin]

Just for the record: @Johannes Hölzl suggested that C^k functions could be defined as a coinductive type.
I have no clue what this means, but it seems to be a good idea if we want to unify proofs for k < infty and k = infty.

[Mario Carneiro]

you could use enat for the type of k

[Sebastien Gouezel]

Yes, I am planning to use enat.

[Mario Carneiro]

local_equiv makes me nervous. I know that this is how Isabelle does it, but I'm not sure that subtypes wouldn't be better

[Johan Commelin]

Does that give access to the goodies that coinductive promises?

[Mario Carneiro]

enat is a coinductive type

[Mario Carneiro]

option nat is an inductive type

[Sebastien Gouezel]

The difficulty with subtypes is that you need all the time to provide proofs that your point belongs to the subtype. When you start intersecting domains (which happens all the time in this business), then this becomes a big mess for rewrites.

[Mario Carneiro]

why don't you use a relational interface for it, like roption?

[Mario Carneiro]

i.e. y \in f x to say \ex h, f <x, h> = y

[Johan Commelin]

I'm not an analytic geometer at all. But I would still like to know it if is a serious option to formalise manifolds as locally ringed spaces.

[Mario Carneiro]

aren't locally ringed spaces a completely different thing?

[Johan Commelin]

It means we could unify some of the basic theory with alg. geometry

[Mario Carneiro]

I know that manifolds are locally ringed but I doubt the converse holds

[Johan Commelin]

the converse is not true

[Johan Commelin]

But schemes are also LRS

[Patrick Massot]

Who thought Sébastien was doing nothing, waiting for us to merge Gromov-Hausdorff?

[Patrick Massot]

This is killing me because I have so much teaching, and perfectoid spaces to define

[Patrick Massot]

But I'll still have a look

[Johan Commelin]

This is killing me because I have so much teaching, and perfectoid spaces to define

Yes, I got very worried when I read @Sebastien Gouezels post. I feared that we might lose your precious time for perfectoids.

[Patrick Massot]

Sébastien, why are you putting an a priori topology on a manifold? You know you are planning pain for your future self building the tangent bundle, right?

[Patrick Massot]

Also, about the local equiv and Mario's question, you should really really discuss this with @Assia Mahboubi . She is aware of this specific question, and is a real dependent type theorist. This is a crucial question, and setting it up correctly is crucial.

[Sebastien Gouezel]

I'm not an analytic geometer at all. But I would still like to know it if is a serious option to formalise manifolds as locally ringed spaces.

Smooth manifolds can indeed be described as locally ringed space on which the ring is a ring of smooth functions on an open subset of R^n, say. But I don't know if there are such theorems for other kinds of structures (notably (G,X) structures, see https://en.wikipedia.org/wiki/(G,X)-manifold if you are not used to this notion), for which the groupoid description is the right one. And with the groupoid you can also go for any intermediate smoothness you like, or for manifolds with boundary, and so on. I am convinced this is precisely the right level of generality.

[Patrick Massot]

I forgot this question. I agree with Sébastien. And I add that nobody is serious about this ringed space approach. I've never seen anyone seriously develop even the very beginning of the story from this point of view. Some pretend to do that, but either prove nothing or first prove this definition is equivalent to the usual one, and then use the usual one

[Sebastien Gouezel]

Sébastien, why are you putting an a priori topology on a manifold? You know you are planning pain for your future self building the tangent bundle, right?

Think of the other option, where you start from an atlas and define the topology from it. Then there is absolutely no way that the topology coming from the atlas on M x N would be the defeq to the product topology. To avoid diamonds, it means that you would have to play the same trick as in the definition of metric space, embedding a topology in the definition of manifold and a proof of compatibility.

Another issue is that I want to consider several manifold structures on a manifold, say a C^1 structure and a compatible C^\infty structure. But I want them to share the same topology. Having an a priori given topology looks likes a good solution, and helps defining the manifold structure by requiring that all the charts are local homeomorphisms.

But I agree I will need a constructor, taking a family of local charts for which the change of coordinates are in my groupoid, and deducing a topology and a manifold structure from it. That's one of the infinitely many things that have to be done :)

[Sebastien Gouezel]

Also, about the local equiv and Mario's question, you should really really discuss this with Assia Mahboubi . She is aware of this specific question, and is a real dependent type theorist. This is a crucial question, and setting it up correctly is crucial.

Yes, getting this right is crucial, and it is a good idea that I should discuss this with Assia. I am completely ready to throw away what I've done until now and start over again (and I am pretty sure I will have to do it). But to get a good feeling of the difficulties I want to push this at least up to the definition of the tangent bundle (with automatically inherited smoothness) and differentials.

[Sebastien Gouezel]

why don't you use a relational interface for it, like roption?

I went this way because I don't see the advantages that other options would have (compared to using genuine functions and just remembering the source). But I am completely open to suggestions. I just need to walk this road long enough to see what goes well and what does not go so well.

[Mario Carneiro]

One problem with having total functions is that the functions are defined elsewhere, where the value doesn't matter. This is problematic for a few reasons: It makes equality weaker than it should be, since "irrelevant" information can make two functions unequal; it causes problems wrt inhabited types, because you may need to fill those values with something; it makes the theory less constructive (which isn't a major issue but is usually an indication that you are going against the grain of the prover). I agree that you should try it and see, though - I am a firm believer in evidence-based formalization decisions.

[Mario Carneiro]

There is some preparatory work towards using roption functions, as well as functional relations, for partiality in Jeremy's filter stuff, used in fderiv

[Reid Barton]

I was going to write something similar to what Mario just said. I would expect the following issues with this approach:

• You can't use continuous directly, you have to introduce continuous_on. I'm willing to believe this issue is illusory, since you would probably want to have continuous_on anyways (indeed it already exists) and using subtypes would produce a lot of "subtype of subtype" overhead instead.
• You have too much data in a local_equiv, namely the values of to_fun and inv_fun outside the source and target. It seems too easy to forget to include a field like eq_on_source in structure_groupoid. (Does manifold need one too?) Would taking a quotient help?
• There are issues with the empty type: if a is nonempty and b is empty there aren't any local_equivs at all between a and b, but there ought to be exactly one. As far as I can see the empty manifold isn't a manifold for this reason.

[Reid Barton]

Hmm, I guess maybe the empty manifold actually is a manifold, bu something still seems off

[Reid Barton]

Anyways, I suggest you also try replacing to_fun, inv_fun, source, target by a pair of pfuns

[Jeremy Avigad]

I still need to catch up on the conversation, but in response to @Sebastien Gouezel's original question: I find it easiest to use the library when the order of arguments matches what you would say verbally. E.g. has_fderiv_at f f' x reads "f has derivative f' at x." So I would prefer changing has_sum to summable and is_sum to has_sum. Or, if we have to use is_fderiv, I would prefer to write is_fderiv_at f' f x for "f' if the derivative of f at x and similarly changing the order of arguments to is_sum.

Anyhow, I am willing to yield to the opinion of the majority. I agree that it would be good if the naming schemes were uniform.

[Sebastien Gouezel]

I think I like the symmetry in the dichotomy has_sum/is_sum better than summable/ has_sum (and fderivable/has_fderiv?). I don't have a strong opinion on the order of arguments, so I would be ready to follow your suggestion of swapping the order of arguments for is_sum. @Johannes Hölzl, what do you think?

[Sebastien Gouezel]

In fact I changed my mind, and I think I prefer summable / has_sum. Has anyone strong opinions on this?

[Jeremy Avigad]

Note: the usual English is "differentiable" rather than "derivable". If we go that route, we have

summable / has_sum
differentiable / has_deriv
fdifferentiable / has_fderiv
integrable / has_integral
converges / tendsto

(Are there others?) Otherwise, we have

has_sum / is_sum
has_deriv / is_deriv
has_fderiv / is_fderiv
has_integral / is_integral
has_limit (?) / tendsto

[Sebastien Gouezel]

I PRed the switch to summable/has_sum in #912