mathlib

a968611b - feat(analysis/schwartz_space): lemmas for supremum of seminorms (#18648)

feat(analysis/schwartz_space): lemmas for supremum of seminorms (#18648) The main result is the bound `one_add_le_seminorm_sup_apply`, which is sometimes in the literature used as the definition of the Schwartz space. We don't really care about the `2^k` factor, since this result is usually used to prove that certain operators are bounded on Schwartz space and hence finiteness of the right hand side is all that matters. One application is to show that the product of a Schwartz function and a smooth polynomially growing function is again Schwartz. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>