Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-20 08:58 c99203f7

View on Github →

feat(measure_theory/integral/interval_integral): add lemmas (#16986)

Clean up some implicit arguments
Slightly generalize continuous_linear_map.interval_integral_comp_comm
From the sphere eversion project Co-authored by: Patrick Massot patrick.massot@u-psud.fr

Estimated changes

Modified src/measure_theory/function/strongly_measurable.lean

added theorem measure_theory.ae_strongly_measurable.ae_strongly_measurable_interval_oc_iff

Modified src/measure_theory/integral/interval_integral.lean

added theorem continuous_linear_map.interval_integral_apply

modified theorem integrable_on_Icc_iff_integrable_on_Ioc'

modified theorem integrable_on_Icc_iff_integrable_on_Ioc

modified theorem integrable_on_Icc_iff_integrable_on_Ioo

modified theorem integrable_on_Ici_iff_integrable_on_Ioi'

modified theorem integrable_on_Ici_iff_integrable_on_Ioi

modified theorem integrable_on_Ioc_iff_integrable_on_Ioo

added theorem interval_integrable.const_mul

added theorem interval_integrable.interval_integrable_norm_iff

added theorem interval_integrable.mono_set'

added theorem interval_integrable.mul_const

modified def interval_integrable

modified theorem interval_integrable_iff_integrable_Icc_of_le

added theorem interval_integral.abs_interval_integral_eq

added theorem interval_integral.interval_integrable_of_integral_ne_zero

added theorem interval_integral.norm_integral_le_of_norm_le

added theorem interval_integral.norm_interval_integral_eq

modified def interval_integral