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} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (l : BoxIntegral.IntegrationParams) (hl : l.bRiemann = false) {s : Set (ι → ℝ)} (hs : MeasurableSet s) (I : BoxIntegral.Box ι) (y : E) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] : 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} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {f : (ι → ℝ) → E} {μ : MeasureTheory.Measure (ι → ℝ)} [MeasureTheory.IsLocallyFiniteMeasure μ] (hf : f =ᵐ[μ.restrict ↑I] 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} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] {l : BoxIntegral.IntegrationParams} {I : BoxIntegral.Box ι} {y : E} {f g : (ι → ℝ) → E} {μ : MeasureTheory.Measure (ι → ℝ)} [MeasureTheory.IsLocallyFiniteMeasure μ] (hf : BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul y) (hfg : f =ᵐ[μ.restrict ↑I] 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} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : MeasureTheory.SimpleFunc (ι → ℝ) E) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams) (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} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] (f : MeasureTheory.SimpleFunc (ι → ℝ) E) (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] (I : BoxIntegral.Box ι) (l : BoxIntegral.IntegrationParams) (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} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : (ι → ℝ) → E} {μ : MeasureTheory.Measure (ι → ℝ)} [MeasureTheory.IsLocallyFiniteMeasure μ] {I : BoxIntegral.Box ι} (hf : MeasureTheory.IntegrableOn f (↑I) μ) (l : BoxIntegral.IntegrationParams) (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} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : (ι → ℝ) → E} (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] {I : BoxIntegral.Box ι} (hc : ContinuousOn f (BoxIntegral.Box.Icc I)) (l : BoxIntegral.IntegrationParams) : 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.

theorem MeasureTheory.AEContinuous.hasBoxIntegral {ι : Type u} {E : Type v} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : (ι → ℝ) → E} (μ : MeasureTheory.Measure (ι → ℝ)) [MeasureTheory.IsLocallyFiniteMeasure μ] {I : BoxIntegral.Box ι} (hb : ∃ (C : ℝ), ∀ x ∈ BoxIntegral.Box.Icc I, ‖f x‖ ≤ C) (hc : ∀ᵐ (x : ι → ℝ) ∂μ, ContinuousAt f x) (l : BoxIntegral.IntegrationParams) : BoxIntegral.HasIntegral I l f μ.toBoxAdditive.toSMul (∫ (x : ι → ℝ) in ↑I, f x ∂μ)

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