Commit 2023-04-22 06:00 d4817f88

View on Github →

feat(measure_theory/integral/integral_eq_improper): fundamental theorem of calculus on (a, +\infty) (#18844) It became apparent in several applications that we are missing API here. As an illustration, two existing proofs in the library are shortened with the new API.

Estimated changes

Modified src/analysis/special_functions/gaussian.lean

Modified src/analysis/special_functions/integrals.lean

Modified src/measure_theory/integral/exp_decay.lean

deleted theorem integral_exp_neg_le

Modified src/measure_theory/integral/integral_eq_improper.lean

added theorem measure_theory.integrable_on_Ioi_deriv_of_nonneg'

added theorem measure_theory.integrable_on_Ioi_deriv_of_nonneg

added theorem measure_theory.integrable_on_Ioi_deriv_of_nonpos'

added theorem measure_theory.integrable_on_Ioi_deriv_of_nonpos

added theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonneg'

added theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonneg

added theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonpos'

added theorem measure_theory.integral_Ioi_of_has_deriv_at_of_nonpos

added theorem measure_theory.integral_Ioi_of_has_deriv_at_of_tendsto'

added theorem measure_theory.integral_Ioi_of_has_deriv_at_of_tendsto

Modified src/measure_theory/integral/interval_integral.lean

modified theorem interval_integral.integrable_on_deriv_of_nonneg

modified theorem interval_integral.integrable_on_deriv_right_of_nonneg