# Zulip Chat Archive

## Stream: maths

### Topic: has_sum / has_fderiv

#### Sebastien Gouezel (Apr 08 2019 at 14:22):

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 (Apr 08 2019 at 14:29):

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 (Apr 08 2019 at 14:31):

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 (Apr 08 2019 at 14:32):

you could use `enat`

for the type of `k`

#### Sebastien Gouezel (Apr 08 2019 at 14:33):

Yes, I am planning to use `enat`

.

#### Mario Carneiro (Apr 08 2019 at 14:33):

`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 (Apr 08 2019 at 14:33):

Does that give access to the goodies that `coinductive`

promises?

#### Mario Carneiro (Apr 08 2019 at 14:34):

`enat`

is a coinductive type

#### Mario Carneiro (Apr 08 2019 at 14:34):

`option nat`

is an inductive type

#### Sebastien Gouezel (Apr 08 2019 at 14:35):

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 (Apr 08 2019 at 14:35):

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

?

#### Mario Carneiro (Apr 08 2019 at 14:36):

i.e. `y \in f x`

to say `\ex h, f <x, h> = y`

#### Johan Commelin (Apr 08 2019 at 14:37):

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 (Apr 08 2019 at 14:38):

aren't locally ringed spaces a completely different thing?

#### Johan Commelin (Apr 08 2019 at 14:38):

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

#### Mario Carneiro (Apr 08 2019 at 14:38):

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

#### Johan Commelin (Apr 08 2019 at 14:38):

the converse is not true

#### Johan Commelin (Apr 08 2019 at 14:38):

But schemes are also LRS

#### Patrick Massot (Apr 08 2019 at 14:39):

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

#### Patrick Massot (Apr 08 2019 at 14:39):

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

#### Patrick Massot (Apr 08 2019 at 14:39):

But I'll still have a look

#### Johan Commelin (Apr 08 2019 at 14:40):

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 (Apr 08 2019 at 14:58):

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 (Apr 08 2019 at 14:59):

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 (Apr 08 2019 at 15:04):

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 (Apr 08 2019 at 15:06):

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 (Apr 08 2019 at 15:16):

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 (Apr 08 2019 at 15:20):

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 (Apr 08 2019 at 15:24):

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 (Apr 08 2019 at 16:05):

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 (Apr 08 2019 at 16:06):

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 (Apr 08 2019 at 16:15):

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_equiv`

s 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 (Apr 08 2019 at 16:18):

Hmm, I guess maybe the empty manifold actually is a `manifold`

, bu something still seems off

#### Reid Barton (Apr 08 2019 at 16:36):

Anyways, I suggest you also try replacing `to_fun`

, `inv_fun`

, `source`

, `target`

by a pair of `pfun`

s

#### Jeremy Avigad (Apr 08 2019 at 20:24):

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 (Apr 08 2019 at 20:59):

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 (Apr 08 2019 at 21:25):

In fact I changed my mind, and I think I prefer `summable / has_sum`

. Has anyone strong opinions on this?

#### Jeremy Avigad (Apr 08 2019 at 21:46):

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 (Apr 09 2019 at 08:44):

I PRed the switch to `summable/has_sum`

in #912

Last updated: May 09 2021 at 09:11 UTC