Zulip Chat Archive

Stream: maths

Topic: germs of functions


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 00:33):

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

view this post on Zulip 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?

view this post on Zulip 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) β.

view this post on Zulip David Wärn (May 17 2020 at 08:58):

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 08:58):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 17 2020 at 09:00):

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

view this post on Zulip Reid Barton (May 17 2020 at 09:00):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 09:05):

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

view this post on Zulip Yury G. Kudryashov (May 17 2020 at 09:09):

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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 17 2020 at 09:12):

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

view this post on Zulip Reid Barton (May 17 2020 at 09:15):

oh, maybe I'm wrong!

view this post on Zulip Reid Barton (May 17 2020 at 09:17):

Okay yes, I had misremembered.

view this post on Zulip Reid Barton (May 17 2020 at 09:18):

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

view this post on Zulip Reid Barton (May 17 2020 at 09:18):

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

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 17 2020 at 09:54):

But what you describe indeed seems useful.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 17 2020 at 10:03):

This definitely counts as germ to me

view this post on Zulip 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