Commit 2022-06-04 19:44 97492975

View on Github →

feat(measure_theory/integral/interval_integral): integrability of nonnegative derivatives on open intervals (#14147) Shows that derivatives of continuous functions are integrable when nonnegative.

Estimated changes

Modified src/analysis/special_functions/integrals.lean

modified theorem integral_rpow

added theorem interval_integral.interval_integrable_rpow'

Modified src/measure_theory/integral/integral_eq_improper.lean

added theorem measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded

added theorem measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_left

added theorem measure_theory.integrable_on_Ioc_of_interval_integral_norm_bounded_right

Modified src/measure_theory/integral/interval_integral.lean

added theorem integrable_on_Icc_iff_integrable_on_Ioc'

added theorem integrable_on_Icc_iff_integrable_on_Ioc

added theorem integrable_on_Icc_iff_integrable_on_Ioo

added theorem integrable_on_Ioc_iff_integrable_on_Ioo'

added theorem integrable_on_Ioc_iff_integrable_on_Ioo

added theorem interval_integrable.comp_mul_left

added theorem interval_integrable.iff_comp_neg

added theorem interval_integrable_iff'

added theorem interval_integrable_iff_integrable_Icc_of_le

deleted theorem interval_integral.integrable_on_Icc_iff_integrable_on_Ioc'

deleted theorem interval_integral.integrable_on_Icc_iff_integrable_on_Ioc

added theorem interval_integral.integrable_on_deriv_of_nonneg

added theorem interval_integral.integrable_on_deriv_right_of_nonneg

deleted theorem interval_integral.integral_eq_sub_of_has_deriv_right_of_le_real'

added theorem interval_integral.interval_integrable_deriv_of_nonneg

deleted theorem interval_integral.interval_integrable_iff_integrable_Icc_of_le

modified theorem interval_integral.sub_le_integral_of_has_deriv_right_of_le

added theorem interval_integral.sub_le_integral_of_has_deriv_right_of_le_Ico