## Stream: maths

### Topic: germs of functions

#### Yury G. Kudryashov (May 17 2020 at 00:33):

I've just noticed that we have order/filter/filter_product. If I read the definitions correctly,

• local notation ∀* binders ,  r:(scoped p, filter.eventually p φ) := r is the same as ∀ᶠ but with a fixed filter.
• filter.bigly_equal means that two functions are eventually equal. We have this assumption in many lemmas, probably it deserves a notation (=ᶠ[at_top]?); this notation can be also useful to implement calc syntax for is_O/is_o;
• filter.filterprod is what I know as the germ of a function at a point (if filter is nhds).

What do you think about me making the following changes:

• drop local notation, use ∀ᶠ instead;
• rename bigly_equal to eventually_equal, introduce a notation (possibly localized);
• rename filter.filterprod to filter.germ; or should germ take two filters and assume tendsto so that we can compose them?

#### Yury G. Kudryashov (May 17 2020 at 00:33):

@Abhimanyu Pallavi Sudhir @Patrick Massot @Sebastien Gouezel :up:

#### Abhimanyu Pallavi Sudhir (May 17 2020 at 08:49):

"filter.filterprod is what I know as the germ of a function at a point (if filter is nhds)." -- What's the function?

#### Yury G. Kudryashov (May 17 2020 at 08:53):

Looking at function names, it seems that you had sequences in mind. However we can apply the same definition to look at the quotient space of functions f : α → β by bigly_equal (nhds x) β.

#### David Wärn (May 17 2020 at 08:58):

So filter.filterprod is the "space of germs", right? The elements are germs of functions

#### Yury G. Kudryashov (May 17 2020 at 08:58):

Yes, in the sense of https://en.wikipedia.org/wiki/Germ_(mathematics)

#### Reid Barton (May 17 2020 at 08:59):

I sort of think this is the wrong way to think about it, though. I know this is the approach used for manifolds, but in more general settings you might have a section defined on a neighborhood of a point that doesn't extend to the whole space.

#### Yury G. Kudryashov (May 17 2020 at 09:00):

If we have f : α → β not f : Π x, β x, then what's wrong with extending f to a total function?

#### Reid Barton (May 17 2020 at 09:00):

Like, it works in this one specific case of non-dependent functions with no conditions.

#### Reid Barton (May 17 2020 at 09:00):

In this case, nothing is really wrong (but you still need some ugly if to extend).

#### Reid Barton (May 17 2020 at 09:03):

Surely you'll want a germ of a section of a bundle or something eventually anyways, and a germ of a function is just a special case of that

#### Yury G. Kudryashov (May 17 2020 at 09:05):

I think that it makes sense to use eventually_equal in more lemmas anyway.

#### Yury G. Kudryashov (May 17 2020 at 09:09):

I don't want to think about dependent germs right now.

#### Yury G. Kudryashov (May 17 2020 at 09:10):

They should come with some tactics that will allow us to write proofs with rw/simp without starting with filter_upwards.

#### David Wärn (May 17 2020 at 09:11):

But even for non-dependent functions, you might want germs of "partial functions that are eventually defined"? Wouldn't it make sense to use this definition also for filter.filterprod?

#### Reid Barton (May 17 2020 at 09:12):

For some reason the ultraproduct traditionally isn't defined this way, I think.

#### Reid Barton (May 17 2020 at 09:15):

oh, maybe I'm wrong!

#### Reid Barton (May 17 2020 at 09:18):

It doesn't make a difference up to isomorphism if the object is nonempty.

#### Reid Barton (May 17 2020 at 09:18):

But Lean doesn't work up to isomorphism, so...

#### Reid Barton (May 17 2020 at 09:19):

Thanks Yury for pointing out the connection to germs, by the way. This is something I "knew, but didn't know I knew".

#### David Wärn (May 17 2020 at 09:37):

This sort of thing should show up also in measure theory. The statement of Fubini already needs "partial functions defined almost everywhere", I think

#### Patrick Massot (May 17 2020 at 09:54):

Yury G. Kudryashov said:

I've just noticed that we have order/filter/filter_product. If I read the definitions correctly,

• local notation ∀* binders ,  r:(scoped p, filter.eventually p φ) := r is the same as ∀ᶠ but with a fixed filter.
• filter.bigly_equal means that two functions are eventually equal. We have this assumption in many lemmas, probably it deserves a notation (=ᶠ[at_top]?); this notation can be also useful to implement calc syntax for is_O/is_o;
• filter.filterprod is what I know as the germ of a function at a point (if filter is nhds).

What do you think about me making the following changes:

• drop local notation, use ∀ᶠ instead;
• rename bigly_equal to eventually_equal, introduce a notation (possibly localized);
• rename filter.filterprod to filter.germ; or should germ take two filters and assume tendsto so that we can compose them?

I was pinged here, but have nothing to do with this file. This is all about non-standard analysis non-sense. I don't think this is used anywhere else. And leanproject confirm this file is imported only by data.real.hyperreal which is not imported anywhere.

#### Patrick Massot (May 17 2020 at 09:54):

But what you describe indeed seems useful.

#### Patrick Massot (May 17 2020 at 09:57):

David Wärn said:

So filter.filterprod is the "space of germs", right? The elements are germs of functions

If this is true then the name we currently use is very unfortunate.

#### Reid Barton (May 17 2020 at 10:00):

They aren't literally germs in the usual sense in general-- a filter on nat is usually not a neighborhood filter of any point of nat.

#### Reid Barton (May 17 2020 at 10:01):

They are more like germs at points of the Stone-Cech compactification, at least if the filter is an ultrafilter.

#### Patrick Massot (May 17 2020 at 10:03):

This definitely counts as germ to me

#### Yury G. Kudryashov (May 17 2020 at 10:33):

Germs at infinity is a good object. I pinged @Patrick Massot to get feedback on the proposed changes, not on the current contents of the file.

Last updated: May 06 2021 at 18:20 UTC