Commit 2025-12-09 18:53 c58c5dcb

View on Github →

feat(Analysis/Distribution): integration by parts for Schwartz functions (#31876)

Estimated changes

Modified Mathlib/Analysis/Distribution/SchwartzSpace.lean

added theorem SchwartzMap.integral_bilinear_lineDerivOp_right_eq_neg_left

added theorem SchwartzMap.integral_clm_comp_lineDerivOp_right_eq_neg_left

added theorem SchwartzMap.integral_mul_lineDerivOp_right_eq_neg_left

added theorem SchwartzMap.integral_smul_deriv_right_eq_neg_left

added theorem SchwartzMap.integral_smul_lineDerivOp_right_eq_neg_left