Commit 2024-03-07 15:45 28b31c2b

View on Github →

feat(Analysis/Distribution/SchwartzSpace): Constructor for CLMs to normed space and integration (#10652)

We define a constructor for continuous linear maps from Schwartz space into normed spaces similar to mkCLM
Define the integral as a distribution on Schwartz space (moved to lemmas from Analysis/Distribution/FourierSchwartz to Analysis/Distribution/SchwartzSpace for that)
Golf a few definitions

Estimated changes

Modified Mathlib/Analysis/Distribution/FourierSchwartz.lean

deleted theorem SchwartzMap.integrable

deleted theorem SchwartzMap.integrable_pow_mul

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem SchwartzMap.integrable

added theorem SchwartzMap.integrable_pow_mul

added def SchwartzMap.integralCLM

added theorem SchwartzMap.integralCLM_apply

added def SchwartzMap.mkCLMtoNormedSpace

deleted def SchwartzMap.toBoundedContinuousFunctionLM

deleted theorem SchwartzMap.toBoundedContinuousFunctionLM_apply

deleted def SchwartzMap.toZeroAtInftyLM

deleted theorem SchwartzMap.toZeroAtInftyLM_apply