germs of functions

Stream: maths

[Yury G. Kudryashov]

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]

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

[Abhimanyu Pallavi Sudhir]

"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]

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]

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

[Yury G. Kudryashov]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[David Wärn]

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]

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

[Reid Barton]

oh, maybe I'm wrong!

[Reid Barton]

Okay yes, I had misremembered.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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]

But what you describe indeed seems useful.

[Patrick Massot]

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]

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]

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

[Patrick Massot]

This definitely counts as germ to me

[Yury G. Kudryashov]

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.