Commit 2023-06-07 18:05 b9c988d4

View on Github →

feat: port MeasureTheory.Integral.FundThmCalculus (#4773)

Estimated changes

Modified Mathlib.lean

Created Mathlib/MeasureTheory/Integral/FundThmCalculus.lean

added theorem Continuous.deriv_integral

added theorem Continuous.integral_hasStrictDerivAt

added theorem intervalIntegral.FTCFilter.finite_at_inner

added theorem intervalIntegral.derivWithin_integral_left

added theorem intervalIntegral.derivWithin_integral_of_tendsto_ae_left

added theorem intervalIntegral.derivWithin_integral_of_tendsto_ae_right

added theorem intervalIntegral.derivWithin_integral_right

added theorem intervalIntegral.deriv_integral_left

added theorem intervalIntegral.deriv_integral_of_tendsto_ae_left

added theorem intervalIntegral.deriv_integral_of_tendsto_ae_right

added theorem intervalIntegral.deriv_integral_right

added theorem intervalIntegral.differentiableOn_integral_of_continuous

added theorem intervalIntegral.fderivWithin_integral_of_tendsto_ae

added theorem intervalIntegral.fderiv_integral

added theorem intervalIntegral.fderiv_integral_of_tendsto_ae

added theorem intervalIntegral.integrableOn_deriv_of_nonneg

added theorem intervalIntegral.integrableOn_deriv_right_of_nonneg

added theorem intervalIntegral.integral_comp_mul_deriv'''

added theorem intervalIntegral.integral_comp_mul_deriv''

added theorem intervalIntegral.integral_comp_mul_deriv'

added theorem intervalIntegral.integral_comp_mul_deriv

added theorem intervalIntegral.integral_comp_smul_deriv'''

added theorem intervalIntegral.integral_comp_smul_deriv''

added theorem intervalIntegral.integral_comp_smul_deriv'

added theorem intervalIntegral.integral_comp_smul_deriv

added theorem intervalIntegral.integral_deriv_comp_mul_deriv'

added theorem intervalIntegral.integral_deriv_comp_mul_deriv

added theorem intervalIntegral.integral_deriv_comp_smul_deriv'

added theorem intervalIntegral.integral_deriv_comp_smul_deriv

added theorem intervalIntegral.integral_deriv_eq_sub'

added theorem intervalIntegral.integral_deriv_eq_sub

added theorem intervalIntegral.integral_deriv_mul_eq_sub

added theorem intervalIntegral.integral_eq_sub_of_hasDerivAt

added theorem intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le

added theorem intervalIntegral.integral_eq_sub_of_hasDerivAt_of_tendsto

added theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right

added theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le

added theorem intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le_real

added theorem intervalIntegral.integral_hasDerivAt_left

added theorem intervalIntegral.integral_hasDerivAt_of_tendsto_ae_left

added theorem intervalIntegral.integral_hasDerivAt_of_tendsto_ae_right

added theorem intervalIntegral.integral_hasDerivAt_right

added theorem intervalIntegral.integral_hasDerivWithinAt_left

added theorem intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_left

added theorem intervalIntegral.integral_hasDerivWithinAt_of_tendsto_ae_right

added theorem intervalIntegral.integral_hasDerivWithinAt_right

added theorem intervalIntegral.integral_hasFDerivAt

added theorem intervalIntegral.integral_hasFDerivAt_of_tendsto_ae

added theorem intervalIntegral.integral_hasFDerivWithinAt

added theorem intervalIntegral.integral_hasFDerivWithinAt_of_tendsto_ae

added theorem intervalIntegral.integral_hasStrictDerivAt_left

added theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_left

added theorem intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right

added theorem intervalIntegral.integral_hasStrictDerivAt_right

added theorem intervalIntegral.integral_hasStrictFDerivAt

added theorem intervalIntegral.integral_hasStrictFDerivAt_of_tendsto_ae

added theorem intervalIntegral.integral_le_sub_of_hasDeriv_right_of_le

added theorem intervalIntegral.integral_mul_deriv_eq_deriv_mul

added theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae

added theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left

added theorem intervalIntegral.integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right

added theorem intervalIntegral.integral_sub_linear_isLittleO_of_tendsto_ae

added theorem intervalIntegral.intervalIntegrable_deriv_of_nonneg

added theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae

added theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left

added theorem intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_right

added theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae'

added theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae

added theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge'

added theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_ge

added theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le'

added theorem intervalIntegral.measure_integral_sub_linear_isLittleO_of_tendsto_ae_of_le

added theorem intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le

added theorem intervalIntegral.sub_le_integral_of_hasDeriv_right_of_le_Ico