Commit 2021-06-20 12:05 3a0f2822

View on Github →

feat(measure_theory/interval_integral): integral of a non-integrable function (#8011) The interval_integral of a non-interval_integrable function is 0.

Estimated changes

Modified src/measure_theory/interval_integral.lean

modified theorem interval_integral.integral_non_ae_measurable

modified theorem interval_integral.integral_non_ae_measurable_of_le

added theorem interval_integral.integral_undef