mathlib documentation

analysis.box_integral.integrability

McShane integrability vs Bochner integrability #

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.