# Zulip Chat Archive

## 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:17):

Okay yes, I had misremembered.

#### 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