# 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].

## Tags #

integral, McShane integral, Bochner integral

theorem BoxIntegral.hasIntegralIndicatorConst {ι : Type u} {E : Type v} [] [] (hl : l.bRiemann = false) {s : Set (ι)} (hs : ) (I : ) (y : E) (μ : MeasureTheory.Measure (ι)) :
BoxIntegral.HasIntegral I l (Set.indicator s fun x => y) () (ENNReal.toReal (μ (s I)) y)

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

theorem BoxIntegral.HasIntegral.of_aeEq_zero {ι : Type u} {E : Type v} [] [] {I : } {f : (ι) → E} {μ : MeasureTheory.Measure (ι)} (hf : ) (hl : l.bRiemann = false) :

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

theorem BoxIntegral.HasIntegral.congr_ae {ι : Type u} {E : Type v} [] [] {I : } {y : E} {f : (ι) → E} {g : (ι) → E} {μ : MeasureTheory.Measure (ι)} (hfg : ) (hl : l.bRiemann = false) :

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.

theorem MeasureTheory.SimpleFunc.hasBoxIntegral {ι : Type u} {E : Type v} [] [] (f : MeasureTheory.SimpleFunc (ι) E) (μ : MeasureTheory.Measure (ι)) (I : ) (hl : l.bRiemann = false) :

A simple function is McShane integrable w.r.t. any locally finite measure.

theorem MeasureTheory.SimpleFunc.box_integral_eq_integral {ι : Type u} {E : Type v} [] [] (f : MeasureTheory.SimpleFunc (ι) E) (μ : MeasureTheory.Measure (ι)) (I : ) (hl : l.bRiemann = false) :

For a simple function, its McShane (or Henstock, or ⊥) box integral is equal to its integral in the sense of MeasureTheory.SimpleFunc.integral.

theorem MeasureTheory.IntegrableOn.hasBoxIntegral {ι : Type u} {E : Type v} [] [] [] {f : (ι) → E} {μ : MeasureTheory.Measure (ι)} {I : } (hf : ) (hl : l.bRiemann = false) :
BoxIntegral.HasIntegral I l f () (∫ (x : ι) in I, f xμ)

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.