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

source

theorem box_integral.has_integral_indicator_const {ι : Type u} {E : Type v} [fintype ι] [normed_add_comm_group E] [normed_space ℝ E] (l : box_integral.integration_params) (hl : l.bRiemann = bool.ff) {s : set (ι → ℝ)} (hs : measurable_set s) (I : box_integral.box ι) (y : E) (μ : measure_theory.measure (ι → ℝ)) [measure_theory.is_locally_finite_measure μ] :

box_integral.has_integral I l (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.

source

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

box_integral.has_integral I l f μ.to_box_additive.to_smul 0

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

source

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

box_integral.has_integral I l g μ.to_box_additive.to_smul 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.

source

theorem measure_theory.simple_func.has_box_integral {ι : Type u} {E : Type v} [fintype ι] [normed_add_comm_group E] [normed_space ℝ E] (f : measure_theory.simple_func (ι → ℝ) E) (μ : measure_theory.measure (ι → ℝ)) [measure_theory.is_locally_finite_measure μ] (I : box_integral.box ι) (l : box_integral.integration_params) (hl : l.bRiemann = bool.ff) :

box_integral.has_integral I l ⇑f μ.to_box_additive.to_smul (measure_theory.simple_func.integral (μ.restrict ↑I) f)

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

source

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

box_integral.integral I l ⇑f μ.to_box_additive.to_smul = measure_theory.simple_func.integral (μ.restrict ↑I) f

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.

source

theorem measure_theory.integrable_on.has_box_integral {ι : Type u} {E : Type v} [fintype ι] [normed_add_comm_group E] [normed_space ℝ E] [complete_space E] {f : (ι → ℝ) → E} {μ : measure_theory.measure (ι → ℝ)} [measure_theory.is_locally_finite_measure μ] {I : box_integral.box ι} (hf : measure_theory.integrable_on f ↑I μ) (l : box_integral.integration_params) (hl : l.bRiemann = bool.ff) :

box_integral.has_integral I l f μ.to_box_additive.to_smul (∫ (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.