Bochner-integrable function

Let $(\mathrm{\Omega },\mathcal{A},\mu )$ be a measure space and $X$ a real or complex Banach space. A strongly measurable function $f:\mathrm{\Omega }\to X$ is Bochner integrable if there is a sequence of integrable $X$-valued simple functions $(s_n)$ such that

${\lim }_{n\to \mathrm{\infty }}{\int }_{\mathrm{\Omega }}\mathrm{\parallel }f-s_n\mathrm{\parallel }d\mu =0.$

For such a sequence define

${\int }_{\mathrm{\Omega }}fd\mu :={\lim }_{n\to \mathrm{\infty }}{\int }_{\mathrm{\Omega }}{s}_{n}d\mu \mathrm{.}$

The displayed norm limit exists: the simple integral inequality gives

$\parallel \int s_n-\int s_m\parallel \le \int \mathrm{\parallel }{s}_n-s_m\mathrm{\parallel }\le \int \mathrm{\parallel }{s}_n-f\mathrm{\parallel }+\int \mathrm{\parallel }f-s_m\mathrm{\parallel },$

so the simple integrals form a Cauchy sequence, and $X$ is complete. The next theorem proves that the value is independent of the approximating sequence and characterizes existence by integrability of $\mathrm{\parallel }f\mathrm{\parallel }$.

For $E\in \mathcal{A}$, write ${\int }_{E}fd\mu :={\int }_{\mathrm{\Omega }}{\mathbf{1}}_{E}fd\mu$ whenever this function is Bochner integrable.

The zero function and every integrable simple function are Bochner integrable, witnessed by constant approximating sequences. No choice principle is used in this definition or in the Cauchy estimate.