Theorem SchwartzMap.norm_toLp_one

Modification history

2026-03-10 22:48
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
feat(Analysis/SchwartzMap): estimates for `Lp` and `BCF` norms (#35953)
Added SchwartzMap.norm_toLp_oneView on Github →