Commit 2024-03-21 14:51 def6f030

View on Github →

feat(Analysis/Distribution/SchwartzSpace): generalize the integral (#11373)

Estimated changes

Modified Mathlib/Analysis/Distribution/FourierSchwartz.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

modified theorem SchwartzMap.integrable

modified theorem SchwartzMap.integrable_pow_mul

modified def SchwartzMap.integralCLM

modified theorem SchwartzMap.integralCLM_apply

added theorem SchwartzMap.integralCLM_dirac_eq_delta

Modified Mathlib/Analysis/SpecialFunctions/JapaneseBracket.lean

modified theorem finite_integral_one_add_norm

modified theorem integrable_one_add_norm

modified theorem integrable_rpow_neg_one_add_norm_sq