mathlib3 documentation


McShane integrability vs Bochner integrability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove that any Bochner integrable function is McShane integrable (hence, it is Henstock and integrable) with the same integral. The proof is based on Russel A. Gordon, The integrals of Lebesgue, Denjoy, Perron, and Henstock.

Tags #

integral, McShane integral, Bochner integral

The indicator function of a measurable set is McShane integrable with respect to any locally-finite measure.

If f is a.e. equal to zero on a rectangular box, then it has McShane integral zero on this box.

If f has integral y on a box I with respect to a locally finite measure μ and g is a.e. equal to f on I, then g has the same integral on I.

If f : ℝⁿ → E is Bochner integrable w.r.t. a locally finite measure μ on a rectangular box I, then it is McShane integrable on I with the same integral.