Commit 2025-09-29 20:43 a43dd5b1

View on Github →

feat(SchwartzSpace): integration by parts in 1d (#29846)

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem SchwartzMap.hasDerivAt

added theorem SchwartzMap.hasFDerivAt

added theorem SchwartzMap.hasTemperateGrowth

added theorem SchwartzMap.integral_bilinear_deriv_right_eq_neg_left

added theorem SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left

added theorem SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul

Modified Mathlib/MeasureTheory/Function/Holder.lean

added theorem ContinuousLinearMap.memLp_of_bilin