Commit 2024-05-04 19:06 06b48c3f

View on Github →

feat: integration by parts for line derivatives and Frechet derivatives (#11937)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/LineDeriv/IntegrationByParts.lean

added theorem integral_bilinear_fderiv_right_eq_neg_left_of_integrable

added theorem integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable

added theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable

added theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux1

added theorem integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2

added theorem integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable

added theorem integral_smul_fderiv_eq_neg_fderiv_smul_of_integrable