ZeroAtInftyContinuousMap

Stream: maths

[Yury G. Kudryashov]

Am I right that we have docs#ZeroAtInftyContinuousMap and docs#HasCompactSupport and no lemma relating the two notions?

[Yury G. Kudryashov]

Also, it seems that the condition in C₀(X, Y) is equivalent to ∃ K, support f ⊆ K ∧ IsCompact K, not IsCompact (tsupport f) (it matters only for non-Hausdorff spaces). Should we unify? If yes, which notion is more important for non-Hausdorff spaces?

[Yury G. Kudryashov]

And one more question: is there a name for the topology on C₀(X, Y) that demands not only uniform convergence of functions but also some convergence of supports? I want to define toLp : C₀(X, E) → Lp E p μ and it is not continuous w.r.t. the topology of uniform convergence.

[Junyan Xu]

There is docs#HasCompactSupport.is_zero_at_infty.

Yury G. Kudryashov said:

Also, it seems that the condition in C₀(X, Y) is equivalent to ∃ K, support f ⊆ K ∧ IsCompact K, not IsCompact (tsupport f) (it matters only for non-Hausdorff spaces).

Nope? 1/(x^2+1) on the real line is zero at infinity.

[Anatole Dedecker]

We don’t have a type for continuous functions with compact support yet

[Yury G. Kudryashov]

Ah, sorry. It's nhds 0, not pure 0

[Yury G. Kudryashov]

I don't know why I'm so bad at reading. Then I'm not sure if C₀(X, Y) is a good notation.

[Yury G. Kudryashov]

@Junyan Xu I've managed to misread nhds 0 as pure 0 in the definition. Twice.

[Jireh Loreaux]

Yury, the notation I am familiar with for compact support is a subscript c, not a subscript 0

[Yury G. Kudryashov]

I guess, I should take a break between doing taxes (today) and doing something new in Lean.

[Anatole Dedecker]

I’ve thought about it quite a lot since it’s really similar to what I’m (very slowly) doing for distributions. I’m busy right now, so I’ll comment later, but if someone wants to take care of all of the algebraic boilerplate then I’m happy to just fill in the topology and the seminorms

[Moritz Doll]

Jireh Loreaux said:

Yury, the notation I am familiar with for compact support is a subscript c, not a subscript 0

Subscript 0 for compact support is used sometimes (for instance in Hörmander 1-4 which is a standard reference for linear PDE), but when it is used it always causes confusion