Zulip Chat Archive

Stream: maths

Topic: compactly supported functions


Floris van Doorn (Feb 08 2022 at 11:57):

I'm working on putting compactly supported functions in mathlib.
Which of these should be the definition?
(1) is_compact (closure (support f)) -> easier to work with
(2) ∃ K : set α, is_compact K ∧ ∀ x ∉ K, f x = 0 -> probably nicer definition in a space that is not Hausdorff

I currently defined it as the first definition, but I think I should change it to the second one.

(or course, I will define a multiplicative version and additivize it)

Patrick Massot (Feb 08 2022 at 12:04):

I understand why the second definition can have better properties in non-Hausdorff spaces, but it shouldn't be called "compactly supported". I think it's bad that compactly supported doesn't mean "has compact support".

Floris van Doorn (Feb 08 2022 at 12:14):

Do we want a name for functions that are zero outside some compact set? This is a weaker condition that is sufficient for many theorems.
Or do we not care about spaces that are not Hausdorff, and just assume compactly supported in lemmas and that the space is Hausdorff in cases where we need the equivalence between the definitions?

Patrick Massot (Feb 08 2022 at 12:18):

I would do whatever is less work for you.

Floris van Doorn (Feb 08 2022 at 12:19):

I can live with that :-)

Reid Barton (Feb 08 2022 at 12:21):

Are these definitions really different?

Reid Barton (Feb 08 2022 at 12:23):

Oh I see, in 2 the closure of the support might go outside K?

Anatole Dedecker (Feb 08 2022 at 18:25):

Not answering the original question, but I just noticed that both definitions correspond to f being eventually equal to 0 along some filter (namely docs#filter.coclosed_compact for (1) and docs#filter.cocompact for (2)). This isn’t really mathematically interesting but it might give some stability properties for free ?


Last updated: Dec 20 2023 at 11:08 UTC