Theorem: Bochner Integral is Well-Defined

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,}_X}$ be a Banach space over $\GF$.
Let $I$ be a real interval.
Let $\lambda$ be the Lebesgue measure on $I$. 
Let $f : I \to X$ be a Bochner integrable function.
Then the Bochner integral of $f$ is well-defined.

Proof:
We have two aims. 
We first show that if $\sequence {s_n}_{n \mathop \in \N}$ is a sequence of simple functions such that:
:$\map {s_n} t \to \map f t$ for each $t \in I \setminus \Omega_0$, $\map \lambda {\Omega_0} = 0$
and:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {f - s_n}_X \rd \lambda = 0$
then:
:$\ds \lim_{n \mathop \to \infty} \int_I s_n \rd \lambda$ exists.
We then show that the value of this limit is independent of the sequence chosen.
Let $\sequence {s_n}_{n \mathop \in \N}$ be a sequence of simple functions such that:
:$\map {s_n} t \to \map f t$ for each $t \in I$
and:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {f - s_n}_X \rd \lambda = 0$
Then, we have:
{{begin-eqn}}
{{eqn	| l = \norm {\int_I s_n \rd \lambda - \int_I s_m \rd \lambda}_X 
		| r = \norm {\int_I \paren {s_n - s_m} \rd \lambda}_X 
		| c = Bochner Integral of Sum of Simple Functions and Bochner Integral of Scalar Multiple of Simple Function
}}
{{eqn	| o = \le 
		| r = \int_I \norm {s_n - s_m}_X \rd \lambda 
		| c = Norm of Bochner Integral of Simple Function
}}
{{eqn	| r = \int_I \norm {\paren {s_n - f} - \paren {s_m - f} }_X \rd \lambda 
}}
{{eqn	| o = \le
		| r = \int_I \norm {s_n - f}_X \rd \lambda + \int_I \norm {s_m - f}_X \rd \lambda 
		| c = Integral of Integrable Function is Monotone and Integral of Integrable Function is Additive
}}
{{end-eqn}}
Let $\epsilon > 0$.
Since:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {s_n - f}_X \rd \lambda$
there exists $N \in \N$ such that:
:$\ds \int_I \norm {s_n - f}_X \rd \lambda < \frac \epsilon 2$ for $n \ge N$.
Then, for $n, m \ge N$, we have:
:$\ds \norm {\int_I s_n \rd \lambda - \int_I s_m \rd \lambda}_X \le \int_I \norm {s_n - f}_X \rd \lambda + \int_I \norm {s_m - f}_X \rd \lambda < 2 \times \paren {\frac \epsilon 2} = \epsilon$
Hence:
:$\ds \sequence {\int_I s_n \rd \lambda}_{n \mathop \in \N}$ is a Cauchy sequence.
Hence, since $X$ is a Banach space:
:$\ds \lim_{n \mathop \to \infty} \int_I s_n \rd \lambda$ exists.
Now let $\sequence {s_n'}_{n \mathop \in \N}$ be another  sequence of simple functions such that:
:$\map {s_n'} t \to \map f t$ for each $t \in I \setminus \Omega_0'$, $\map \lambda {\Omega_0'} = 0$
and:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {f - s_n'}_X \rd \lambda = 0$
First, from Null Sets Closed under Countable Union, we have $\map \lambda {\Omega_0 \cup \Omega_0'} = 0$, and:
:$\map {s_n} t \to \map f t$ and $\map {s_n'} t \to \map f t$ for each $t \in I \setminus \paren {\Omega_0 \cup \Omega_0'}$. 
We have:
{{begin-eqn}}
{{eqn	| l = \norm {\int_I s_n \rd \lambda - \int_I s_n' \rd \lambda}_X
		| r = \norm {\int_I \paren {s_n - s_n'} \rd \lambda}_X
		| c = Bochner Integral of Sum of Simple Functions and Bochner Integral of Scalar Multiple of Simple Function
}}
{{eqn	| o = \le
		| r = \int_I \norm {s_n - s_n'}_X \rd \lambda 
		| c = Norm of Bochner Integral of Simple Function
}}
{{eqn	| r = \int_I \norm {\paren {s_n - f} - \paren {s_n' - f} }_X \rd \lambda 
}}
{{eqn	| o = \le 
		| r = \int_I \norm {s_n - f}_X \rd \lambda + \int_I \norm {s_n' - f}_X \rd \lambda 
		| c = Integral of Integrable Function is Monotone and Integral of Integrable Function is Additive
}}
{{eqn	| o = \to 
		| r = 0
}}
{{end-eqn}}
Since:
:$\ds \lim_{n \mathop \to \infty} \int_I s_n \rd \lambda$ exists
we have:
:$\ds \lim_{n \mathop \to \infty} \int_I s_n \rd \lambda = \lim_{n \mathop \to \infty} \int_I s_n' \rd \lambda$ 
{{qed}}
Category:Bochner Integrals
d9zao0rwzgn4963b4hwwyev2n93szt0