# mathlib3documentation

analysis.box_integral.integrability

# McShane integrability vs Bochner integrability #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

## Tags #

integral, McShane integral, Bochner integral

theorem box_integral.has_integral_indicator_const {ι : Type u} {E : Type v} [fintype ι] [ E] (hl : l.bRiemann = bool.ff) {s : set )} (hs : measurable_set s) (I : box_integral.box ι) (y : E) (μ : measure_theory.measure ))  :
(s.indicator (λ (_x : ι ), y)) μ.to_box_additive.to_smul ((μ (s I)).to_real y)

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

theorem box_integral.has_integral_zero_of_ae_eq_zero {ι : Type u} {E : Type v} [fintype ι] [ E] {I : box_integral.box ι} {f : ) E} {μ : measure_theory.measure )} (hf : f =ᵐ[μ.restrict I] 0) (hl : l.bRiemann = bool.ff) :

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

theorem box_integral.has_integral.congr_ae {ι : Type u} {E : Type v} [fintype ι] [ E] {I : box_integral.box ι} {y : E} {f g : ) E} {μ : measure_theory.measure )} (hf : y) (hfg : f =ᵐ[μ.restrict I] g) (hl : l.bRiemann = bool.ff) :

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 measure_theory.simple_func.has_box_integral {ι : Type u} {E : Type v} [fintype ι] [ E] (f : E) (μ : measure_theory.measure )) (I : box_integral.box ι) (hl : l.bRiemann = bool.ff) :

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

theorem measure_theory.simple_func.box_integral_eq_integral {ι : Type u} {E : Type v} [fintype ι] [ E] (f : E) (μ : measure_theory.measure )) (I : box_integral.box ι) (hl : l.bRiemann = bool.ff) :

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

theorem measure_theory.integrable_on.has_box_integral {ι : Type u} {E : Type v} [fintype ι] [ E] {f : ) E} {μ : measure_theory.measure )} {I : box_integral.box ι} (hf : μ) (hl : l.bRiemann = bool.ff) :
( (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.