Commit 2023-04-30 20:09 8b8ba04e

View on Github →

feat (measure_theory/integral): lemmas integral_Ioi_eq_integral_Ici etc (#18899) We already have some lemmas relating integrals over open vs. closed intervals, but some were missing (notably half-infinite integrals). This should now be a full set.

Estimated changes

Modified src/measure_theory/integral/integrable_on.lean

added theorem integrable_on_Icc_iff_integrable_on_Ico'

added theorem integrable_on_Icc_iff_integrable_on_Ico

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_Icc_iff_integrable_on_Ioo

added theorem integrable_on_Ici_iff_integrable_on_Ioi'

added theorem integrable_on_Ici_iff_integrable_on_Ioi

added theorem integrable_on_Ico_iff_integrable_on_Ioo'

added theorem integrable_on_Ico_iff_integrable_on_Ioo

added theorem integrable_on_Iic_iff_integrable_on_Iio'

added theorem integrable_on_Iic_iff_integrable_on_Iio

added theorem integrable_on_Ioc_iff_integrable_on_Ioo'

added theorem integrable_on_Ioc_iff_integrable_on_Ioo

Modified src/measure_theory/integral/interval_integral.lean

deleted theorem integrable_on_Icc_iff_integrable_on_Ioc'

deleted theorem integrable_on_Icc_iff_integrable_on_Ioc

deleted theorem integrable_on_Icc_iff_integrable_on_Ioo

deleted theorem integrable_on_Ici_iff_integrable_on_Ioi'

deleted theorem integrable_on_Ici_iff_integrable_on_Ioi

deleted theorem integrable_on_Ioc_iff_integrable_on_Ioo'

deleted theorem integrable_on_Ioc_iff_integrable_on_Ioo

Modified src/measure_theory/integral/set_integral.lean

added theorem measure_theory.integral_Icc_eq_integral_Ico'

added theorem measure_theory.integral_Icc_eq_integral_Ico

modified theorem measure_theory.integral_Icc_eq_integral_Ioc'

modified theorem measure_theory.integral_Icc_eq_integral_Ioc

added theorem measure_theory.integral_Icc_eq_integral_Ioo'

added theorem measure_theory.integral_Icc_eq_integral_Ioo

added theorem measure_theory.integral_Ici_eq_integral_Ioi'

added theorem measure_theory.integral_Ici_eq_integral_Ioi

added theorem measure_theory.integral_Ico_eq_integral_Ioo'

added theorem measure_theory.integral_Ico_eq_integral_Ioo

added theorem measure_theory.integral_Iic_eq_integral_Iio'

added theorem measure_theory.integral_Iic_eq_integral_Iio

modified theorem measure_theory.integral_Ioc_eq_integral_Ioo'

modified theorem measure_theory.integral_Ioc_eq_integral_Ioo