# 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

theorem BoxIntegral.hasIntegralIndicatorConst {ι : Type u} {E : Type v} [] [] (hl : l.bRiemann = false) {s : Set (ι)} (hs : ) (I : ) (y : E) (μ : MeasureTheory.Measure (ι)) :
BoxIntegral.HasIntegral I l (s.indicator fun (x : ι) => y) μ.toBoxAdditive.toSMul ((μ (s I)).toReal 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 : f =ᶠ[(μ.restrict I).ae] 0) (hl : l.bRiemann = false) :
BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul 0

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 (ι)} (hf : BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul y) (hfg : f =ᶠ[(μ.restrict I).ae] g) (hl : l.bRiemann = false) :
BoxIntegral.HasIntegral I l g μ.toBoxAdditive.toSMul y

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) :
BoxIntegral.HasIntegral I l (f) μ.toBoxAdditive.toSMul (MeasureTheory.SimpleFunc.integral (μ.restrict I) f)

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) :
BoxIntegral.integral I l (f) μ.toBoxAdditive.toSMul = MeasureTheory.SimpleFunc.integral (μ.restrict I) f

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 μ.toBoxAdditive.toSMul (∫ (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.

theorem MeasureTheory.ContinuousOn.hasBoxIntegral {ι : Type u} {E : Type v} [] [] [] {f : (ι)E} (μ : MeasureTheory.Measure (ι)) {I : } (hc : ContinuousOn f (BoxIntegral.Box.Icc I)) :
BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι) in I, f xμ)

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.