Commit 2024-03-07 20:58 b6e4828f

View on Github →

feat: improper integration by parts (#10874)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

added theorem MeasureTheory.integral_Iic_deriv_mul_eq_sub

added theorem MeasureTheory.integral_Iic_mul_deriv_eq_deriv_mul

added theorem MeasureTheory.integral_Ioi_deriv_mul_eq_sub

added theorem MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul

added theorem MeasureTheory.integral_deriv_mul_eq_sub

added theorem MeasureTheory.integral_mul_deriv_eq_deriv_mul