Documentation

Mathlib.Analysis.BoxIntegral.Integrability

McShane integrability vs Bochner integrability #

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

We deduce that the same is true for the Riemann integral for continuous functions.

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.

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