Commit 2024-02-08 06:06 62126e3c

feat(Analysis/Distribution/SchwartzMap): projection to ZeroAtInfty and corresponding type class (#9987) Adds a characterization of ZeroAtInfty in terms of norms and uses one direction to show that every Schwartz function is zero at infinity. We also add a few lemmas that characterize elements of the cocompact filter in terms of norm estimates.