Commit 2025-06-16 06:44 ac10029d

View on Github →

feat: easier to use FTC-2 versions for C^1 functions (#25769)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Normed/Operator/LinearIsometry.lean

added theorem LinearIsometry.enorm_map

Created Mathlib/MeasureTheory/Integral/IntervalIntegral/ContDiff.lean

added theorem enorm_sub_le_lintegral_derivWithin_Icc_of_contDiffOn_Icc

added theorem enorm_sub_le_lintegral_deriv_of_contDiffOn_Icc

added theorem intervalIntegral.integral_derivWithin_Icc_of_contDiffOn_Icc

added theorem intervalIntegral.integral_derivWithin_uIcc_of_contDiffOn_uIcc

added theorem intervalIntegral.integral_deriv_of_contDiffOn_Icc

added theorem intervalIntegral.integral_deriv_of_contDiffOn_uIcc