compactly supported functions

Stream: maths

[Floris van Doorn]

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]

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]

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]

I would do whatever is less work for you.

[Floris van Doorn]

I can live with that :-)

[Reid Barton]

Are these definitions really different?

[Reid Barton]

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

[Anatole Dedecker]

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 ?