Commit 2026-03-10 22:48 66eefd62

View on Github →

feat(Analysis/SchwartzMap): estimates for Lp and BCF norms (#35953)

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean

added theorem SchwartzMap.norm_toBoundedContinuousFunction_le

added theorem SchwartzMap.norm_toLp'

added theorem SchwartzMap.norm_toLp_one

added theorem SchwartzMap.norm_toLp_top_le

added theorem SchwartzMap.norm_toZeroAtInfty

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean

added theorem SchwartzMap.norm_fourier_Lp_top_leq_toLp_one

added theorem SchwartzMap.norm_fourier_apply_le_toLp_one

added theorem SchwartzMap.norm_fourier_toBoundedContinuousFunction_le_toLp_one