mathlib documentation

analysis.box_integral.integrability

McShane integrability vs Bochner integrability #

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 ι] [normed_group E] [normed_space E] (l : box_integral.integration_params) (hl : l.bRiemann = 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.

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

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 measure_theory.simple_func.integral.

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.