Mathlib Changelog
v4
Changelog
About
Github
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