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

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 : (ι)E} {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.

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

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 : ), xBoxIntegral.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.