Theorem SchwartzMap.norm_fourier_toBoundedContinuousFunction_le_toLp_one

Modification history

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