avewright/proofwiki-math huggingface dataset:
Theorem: Vector Equation of Straight Line in Space/Formulation 2

Let $\mathbf a$ and $\mathbf b$ denote the position vectors of two points in space.
Let $L$ be a straight line in space passing through $\mathbf a$ and $\mathbf b$.
Let $\mathbf r$ be the position vector of an arbitrary point on $L$.
Then:
:$\mathbf r = \mathbf a + t \paren {\mathbf b - \mathbf a}$
for some real number $t$, which may be positive or negative, or even $0$ if $\mathbf r = \mathbf a$.

Proof:
From {{Formulation|Vector Equation of Straight Line in Space|1}}:
{{:Vector Equation of Straight Line in Space/Formulation 1}}
{{qed|lemma}}
:420px
Let $a$ and $b$ be points as given, with their position vectors $\mathbf a$ and $\mathbf b$ respectively.
Let $P$ be an arbitrary point on the straight line $L$ passing through $a$ and $b$.
By definition of vector subtraction:
:$\vec {a b} = \mathbf b - \mathbf a$
and it follows that $\mathbf b - \mathbf a$ is a vector parallel to $L$.
The result follows.
{{qed}}
Theorem: Slice Category is Isomorphic to Identity Functor Over Object Comma Category/Lemma 1

:$I = J_2 \circ I_1$

Proof:
For each object $g$ in $\mathbf C / C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_2 \circ I_1} g
      | r = \map {J_2} {I_1 g}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_2 \tuple{\operatorname{dom} g,  *, g}
      | c = Definition of $I_1$
}}
{{eqn | r = \tuple{\operatorname{dom} g, g}
      | c = Definition of $J_2$
}}
{{eqn | r = I g
      | c = Definition of $I$
}}
{{end-eqn}}
For each morphism $k : g \to g'$ in $\mathbf C / C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_2 \circ I_1} k
      | r = \map {J_2} {I_1 k}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_2 \tuple{k, \operatorname{id}_*}
      | c = Definition of $I_1$
}}
{{eqn | r = k
      | c = Definition of $J_2$
}}
{{eqn | r = I k
      | c = Definition of $I$
}}
{{end-eqn}}
It follows that:
:$I = J_2 \circ I_1$
{{qed}}
Category:Slice Category is Isomorphic to Identity Functor Over Object Comma Category
i8fxut3a2x80mofndasslfqyjxp9a8u
Theorem: Slice Category is Isomorphic to Identity Functor Over Object Comma Category/Lemma 2

:$J = J_1 \circ I_2$

Proof:
For each object $\tuple{E, g}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow C }$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_1 \circ I_2} \tuple{E, g}
      | r = \map {J_1} {I_2 \tuple{E, g} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_1 \tuple{E, *, g}
      | c = Definition of $I_2$
}}
{{eqn | r = g
      | c = Definition of $J_2$
}}
{{eqn | r = J \tuple{E, g}
      | c = Definition of $J$
}}
{{end-eqn}}
For each morphism $k : \tuple{E, g} \to \tuple{E', g'}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow C }$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_1 \circ I_2} k
      | r = \map {J_1} {I_2 k}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_1 \tuple{k, \operatorname{id}_*}
      | c = Definition of $I_2$
}}
{{eqn | r = k
      | c = Definition of $J_1$
}}
{{eqn | r = J k
      | c = Definition of $J$
}}
{{end-eqn}}
It follows that:
:$J = J_1 \circ I_2$
{{qed}}
Category:Slice Category is Isomorphic to Identity Functor Over Object Comma Category
jzhozzogj4wirg5r2o6xeg02jr5druv
Theorem: Banach Space-Valued Simple Function takes Finitely Many Values

Let $\GF \in \set {\R, \C}$. 
Let $I$ be a real interval.
Let $X$ be a Banach space over $\GF$. 
Let $f : I \to X$ be a simple function.
Then $\Img f$ is a finite set.

Proof:
Since $f$ is a simple function, there exists: 
:Lebesgue measurable subsets $\Omega_1, \ldots, \Omega_n$ of $I$ with finite Lebesgue measure
:$x_1, \ldots, x_n \in X$ 
such that: 
:$\ds \map f t = \sum_{r \mathop = 1}^n x_r \map {\chi_{\Omega_r} } t$
for each $t \in I$.
Note that $\map {\chi_{\Omega_r} } t \in \set {0, 1}$ for each $t \in I$.
Hence we have:
:$\ds \Img f \subseteq \set {\sum_{r \mathop = 1}^n \epsilon_r x_r : \tuple {\epsilon_1, \ldots, \epsilon_n} \in \set {0, 1}^n}$
From Cardinality of Image of Set not greater than Cardinality of Set, we have:
:$\ds \size {\set {\sum_{r \mathop = 1}^n \epsilon_r x_r : \tuple {\epsilon_1, \ldots, \epsilon_n} \in \set {0, 1}^n} } \le \size {\set {0, 1}^n}$
Since $\set {0, 1}^n$ has $2^n$ elements, it is finite.
From Subset of Finite Set is Finite, $\Img f$ is finite.
{{qed}}
Category:Simple Functions
Category:Banach Spaces
opvf63esb884a5tafpy4yotoaof75xz
Theorem: Banach Space-Valued Simple Function has Standard Representation

Let $\GF \in \set {\R, \C}$. 
Let $I$ be a real interval.
Let $X$ be a Banach space over $\GF$. 
Let $f : I \to X$ be a simple function.
Then $f$ is a simple function {{iff}} there exists:
:disjoint Lebesgue measurable sets $\Omega_1, \ldots, \Omega_n \subseteq I$ of finite Lebesgue measure
:$x_1, \ldots, x_n \in X$
such that:
:$\ds \map f t = \sum_{r \mathop = 1}^n x_r \map {\chi_{\Omega_r} } t$ for each $t \in I$.

Proof:
From the definition of a simple function, there exists:
:real intervals $\Omega_1', \ldots, \Omega_n' \subseteq I$ of finite Lebesgue measure
:$x_1, \ldots, x_n \in X$
such that:
:$\ds \map f t = \sum_{r \mathop = 1}^n x_r \map {\chi_{\Omega_r} } t$ for each $t \in I$.
{{WLOG}} suppose that:
:$\ds \bigcup_{r \mathop = 1}^n \Omega_r' = X$ 
From Banach Space-Valued Simple Function takes Finitely Many Values, we have that $\Img f$ is finite.
Note that there are two ways that ${\mathbf 0}_X$ can enter $\Img f$: if one of the $x_r$ (or a sum thereof) is zero, or if $\ds \bigcup_{r \mathop = 1}^n \Omega_r' \ne X$. 
With that in mind, write:
:$\set {{\mathbf 0}_X, y_1, \ldots, y_m} = \Img f$ if $\ds {\mathbf 0}_X \in f \sqbrk {\bigcup_{r \mathop = 1}^n \Omega_r'}$
:$\set {y_1, \ldots, y_m} = \Img f$ otherwise
with each $y_r$ distinct. 
For each $1 \le i \le m$, there exists a non-empty finite set $F_i \subseteq \set {1, 2, \ldots, n}$ such that:
:$\ds \sum_{r \mathop \in F_i} x_r = y_i$
This value is taken by points in:
:$\ds \Omega_i = \bigcap_{r \mathop \in F_i} \Omega_r'$
Since each $y_i$ is distinct it follows that $\Omega_1, \ldots, \Omega_m$ are disjoint.
From Measurable Sets form Sigma-Algebra, we further have that all of $\Omega_1, \ldots, \Omega_m$ are Lebesgue measurable.
Finally, note that:
:$\Omega_i \subseteq \Omega_r'$ for any $r \in F_i$.
From Measure is Monotone, it follows that $\Omega_i$ has finite Lebesgue measure.
We can then write:
:$\ds \map f t = \sum_{r \mathop = 1}^m y_r \map {\chi_{\Omega_r} } t$ for each $t \in I$.
{{qed}}
Theorem: Sum of Banach Space-Valued Simple Functions is Simple Function

Let $\GF \in \set {\R, \C}$. 
Let $I$ be a real interval.
Let $X$ be a Banach space over $\GF$. 
Let $f, g : I \to X$ be a simple function.
Then $f + g$ is simple.

Proof:
From the definition of a simple function, there exists:
:Lebesgue measurable subsets $\II_1, \ldots, \II_n \subseteq I$ of finite Lebesgue measure
:$x_1, \ldots, x_n \in X$
such that:
:$\ds \map f t = \sum_{r \mathop = 1}^n x_r \map {\chi_{\II_r} } t$ for each $t \in I$.
From the definition of a simple function, there exists:
:Lebesgue measurable subsets $\JJ_1, \ldots, \JJ_m \subseteq I$ of finite Lebesgue measure
:$y_1, \ldots, y_m \in X$
such that:
:$\ds \map g t = \sum_{r \mathop = 1}^m y_r \map {\chi_{\JJ_r} } t$ for each $t \in I$.
Let:
:$z_r = x_r$ for $1 \le r \le n$
:$z_{n + r} = y_r$ for $1 \le r \le m$
:$\Omega_r = \II_r$ for $1 \le r \le n$
:$\Omega_{n + r} = \JJ_r$ for $1 \le r \le m$.
Then we have:
:$\ds \map {\paren {f + g} } t = \sum_{r \mathop = 1}^{n + m} z_r \map {\chi_{\Omega_r} } t$ for each $t \in I$.
Hence $f + g$ is a simple function.
{{qed}}
Category:Simple Functions
Category:Banach Spaces
oizxw1skq09j7qmfv8sbrtipdk4tjbg
Theorem: Sum of Bochner Measurable Functions is Bochner Measurable

Let $\GF \in \set {\R, \C}$. 
Let $I$ be a real interval.
Let $X$ be a Banach space over $\GF$. 
Let $f, g : I \to X$ be a Bochner measurable function.
Then $f + g$ is Bochner measurable.

Proof:
Since $f$ is Bochner measurable, there exists a sequence of simple functions $\sequence {\phi_n}_{n \mathop \in \N}$ such that:
:$\ds \map f t = \lim_{n \mathop \to \infty} \map {\phi_n} t$ for almost all $t \in I$.
Since $g$ is Bochner measurable, there exists a sequence of simple functions $\sequence {\psi_n}_{n \mathop \in \N}$ such that:
:$\ds \map g t = \lim_{n \mathop \to \infty} \map {\psi_n} t$ for almost all $t \in I$.
Let $J_1$ be a Lebesgue measurable set with Lebesgue measure $0$ such that:
:$\ds \map f t = \lim_{n \mathop \to \infty} \map {\phi_n} t$ for $t \in I \setminus J_1$
Let $J_2$ be a Lebesgue measurable set with Lebesgue measure $0$ such that:
:$\ds \map g t = \lim_{n \mathop \to \infty} \map {\psi_n} t$ for $t \in I \setminus J_2$
From Null Sets Closed under Countable Union:
:$J = J_1 \cup J_2$ has Lebesgue measure $0$.
Further:
:$\ds \map f t = \lim_{n \mathop \to \infty} \map {\phi_n} t$ and $\ds \map g t = \lim_{n \mathop \to \infty} \map {\psi_n} t$ for $t \in I \setminus J$.
From Linear Combination of Convergent Sequences in Topological Vector Space is Convergent, we then have:
:$\ds \map {\paren {f + g} } t = \lim_{n \mathop \to \infty} \map {\paren {\phi_n + \psi_n} } t$ for $t \in I \setminus J$.
From Sum of Banach Space-Valued Simple Functions is Simple Function, $\phi_n + \psi_n$ is a simple function for each $n \in \N$. 
Hence $f + g$ is Bochner measurable.
{{qed}}
Category:Bochner Measurable Functions
5jzgmtz1bcgsj2x5439cwbxsffam5ad
Theorem: Left Composition of Banach Space-Valued Simple Function with Function Fixing Origin is Simple Function

Let $\GF \in \set {\R, \C}$. 
Let $I$ be a real interval.
Let $X$ and $Y$ be Banach spaces over $\GF$. 
Let $f : I \to X$ be a simple function.
Let $g : X \to Y$ be a function such that $\map g { {\mathbf 0}_X} = {\mathbf 0}_Y$.
Then $g \circ f$ is a simple function.

Proof:
From Banach Space-Valued Simple Function has Standard Representation:
:disjoint Lebesgue measurable sets $\Omega_1, \ldots, \Omega_n \subseteq I$ of finite Lebesgue measure
:$x_1, \ldots, x_n \in X$
such that:
:$\ds \map f t = \sum_{r \mathop = 1}^n x_r \map {\chi_{\Omega_r} } t$ for each $t \in I$.
That is:
:$\map f t = x_r$ for $t \in \Omega_r$
and:
:$\map f t = {\mathbf 0}_X$ for $t \not in \Omega_r$.
Hence:
:$\map g {\map f t} = \map g {x_r}$ for $t \in \Omega_r$
and:
:$\map g t = {\mathbf 0}_Y$ for $t \not \in \Omega_r$.
Hence:
:$\ds \map g {\map f t} = \sum_{r \mathop = 1}^n \map g {x_r} \map {\chi_{\Omega_r} } t$ for each $t \in I$.
Hence $g \circ f$ is a simple function.
{{qed}}
Category:Simple Functions
Category:Banach Spaces
ejayklxy6uobd3618xz4my6mw40rf1b
Theorem: Subset of Set with Zero Outer Measure has Zero Outer Measure

Let $X$ be a set.
Let $\mu^\ast$ be an outer measure on $X$. 
Let $B \subseteq X$ be such that $\map {\mu^\ast} B = 0$.
Let $A \subseteq B$.
Then $\map {\mu^\ast} A = 0$.

Proof:
From condition $(2)$ in the definition of an outer measure, we have:
:$\map {\mu^\ast} A \le \map {\mu^\ast} B = 0$
Since $0 \le \map {\mu^\ast} A$, we have $\map {\mu^\ast} A = 0$.
{{qed}}
Category:Outer Measures
d09rwljzoak4xkbjrwx4mjr1ro2cfuz
Theorem: Measure Space arising from Outer Measure is Complete

Let $X$ be a set.
Let $\mu^\ast$ be an outer measure on $X$.
Let $\map {\mathfrak M} {\mu^*}$ be the collection of $\mu^*$-measurable sets.
Let $\mu$ be the restriction of $\mu^*$ to $\map {\mathfrak M} {\mu^*}$.
Then $\struct {X, \map {\mathfrak M} {\mu^\ast}, \mu}$ is a complete measure space.

Proof:
From Measure Space from Outer Measure, $\struct {X, \map {\mathfrak M} {\mu^\ast}, \mu}$ is a measure space.
Let $A \subseteq X$ be such that $\map {\mu^\ast} A = 0$.
We aim to show that $A \in \map {\mathfrak M} {\mu^\ast}$.
Let $S \subseteq X$.
We want to establish that:
:$\map {\mu^\ast} A = \map {\mu^\ast} {A \cap S} + \map {\mu^\ast} {A \cap S^c}$
From Intersection is Subset, we have:
:$A \cap S \subseteq A$
and:
:$A \cap S^c \subseteq A$
From Subset of Set with Zero Outer Measure has Zero Outer Measure, we have:
:$\map {\mu^\ast} {A \cap S} = 0$
and:
:$\map {\mu^\ast} {A \cap S^c} = 0$
Hence:
:$\map {\mu^\ast} {A \cap S} + \map {\mu^\ast} {A \cap S^c} = 0 = \map {\mu^\ast} A$
Hence $A \in \map {\mathfrak M} {\mu^\ast}$ and $\map \mu A = \map {\mu^\ast} A = 0$.
Now, suppose that $B \in \map {\mathfrak M} {\mu^\ast}$ has $\map \mu B = 0$.
Then, for each $A \subseteq B$, we have:
:$\map {\mu^\ast} A \le \map {\mu^\ast} B = \map \mu B = 0$
Hence:
:$\map {\mu^\ast} A = 0$
Hence $A \in \map {\mathfrak M} {\mu^\ast}$ and $\map \mu A = 0$.
Hence $\struct {X, \map {\mathfrak M} {\mu^\ast}, \mu}$ is a complete measure space.
{{qed}}
Category:Complete Measure Spaces
9ycirwwsotsqutk2xc0y3ll04advod8
Theorem: Lebesgue Measure Space is Complete

Let $\map {\operatorname {Leb} } {\R^n}$ be the Lebesgue $\sigma$-algebra on $\R^n$.
Let $\lambda$ be the Lebesgue measure on $\R^n$. 
Then $\struct {\R^n, \map {\operatorname {Leb} } {\R^n}, \lambda}$ is a complete measure space.

Proof:
By definition, $\struct {\R^n, \map {\operatorname {Leb} } {\R^n}, \lambda}$ is the measure space that arises from the Lebesgue outer measure as in Measure Space from Outer Measure.
From Measure Space arising from Outer Measure is Complete, $\struct {\R^n, \map {\operatorname {Leb} } {\R^n}, \lambda}$ is a complete measure space.
{{qed}}
Category:Lebesgue Measure
h6o01igod39gb59wcc80ajdi6580to0
Theorem: Norm of Bochner Measurable Function is Lebesgue Measurable

Let $\GF \in \set {\R, \C}$. 
Let $\struct {X, \norm {\, \cdot \,} }$ be a Banach space over $\GF$.
Let $I$ be a real interval.
Let $f : I \to X$ be a Bochner measurable function.
Then $\norm f : I \to \R$ is Lebesgue measurable.

Proof:
Since $f$ is a Bochner measurable function, there exists a sequence of simple functions $\sequence {s_n}_{n \mathop \in \N}$ with:
:$\ds \map f t = \lim_{n \mathop \to \infty} \map {s_n} t$ for almost all $t \in I$.
From Modulus of Limit: Normed Vector Space, we have:
:$\ds \norm {\map f t} = \lim_{n \mathop \to \infty} \norm {\map {s_n} t}$ for almost all $t \in I$.
From {{NormAxiomVector|1}}, we have $\norm { {\mathbf 0}_X} = 0$.
Hence, from Left Composition of Banach Space-Valued Simple Function with Function Fixing Origin is Simple Function, we have that $\norm {s_n}$ is a simple function for each $n \in \N$.
Hence $\norm f$ is Bochner measurable.
From Real-Valued Bochner Measurable Function is Lebesgue Measurable, $\norm f$ is Lebesgue measurable.
{{qed}}
Category:Bochner Measurable Functions
7g80o3otz3mc4c9s8e3p70akm7pq8of
Theorem: Pettis Measurability Theorem

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 $f : I \to X$ be a function.
Then $f$ is Bochner measurable {{iff}} it is both weakly measurable and almost separately valued.

Proof:
Let $\lambda$ be the Lebesgue measure.
Let $\struct {X^\ast, \norm {\, \cdot \,}_{X^\ast} }$ be the normed dual space of $\struct {X, \norm {\, \cdot \,}_X}$.
Theorem: Banach Space-Valued Function Constant on each Set in Countable Partition of Domain is Bochner Measurable

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 $\sequence {\Omega_n'}_{n \mathop \in \N}$ be a sequence of Lebesgue measurable subsets of $I$ such that:
:$\ds \bigcup_{n \mathop \in \N} \Omega_n' = I$
Let $f : I \to X$ be a function that is constant on each $\Omega_n'$.
Then $f$ is Bochner measurable.

Proof:
Let $\lambda$ be the Lebesgue measure on $I$. 
Define $c_n \in X$ by $f \sqbrk {\Omega_n'} = \set {c_n}$.
From Countable Union of Measurable Sets as Disjoint Union of Measurable Sets, there exists a pairwise disjoint sequence $\sequence {\Omega_n}_{n \mathop \in \N}$ of Lebesgue measurable subsets of $I$ such that:
:$\ds \bigcup_{n \mathop \in \N} \Omega_n = I$ 
Delete empty $\Omega_n$ and relabel accordingly. 
If only finitely many $\Omega_n$ remain, then we can apply Banach Space-Valued Simple Function is Bochner Measurable and conclude immediately.
Else suppose that countably many $\Omega_n$ remain. 
Define $s_n : I \to X$ by:
:$\ds \map {s_n} t = \sum_{j \mathop = 1}^n c_j \map {\chi_{\Omega_j \cap \closedint {-n} n} } t$ for each $t \in I$.
From Measure is Monotone, we have $\map \lambda {\Omega_j \cap \closedint {-n} n} \le \map \lambda {\closedint {-n} n}$.
From Measure of Interval is Length, we have $\map \lambda {\closedint {-n} n} = 2 n < \infty$.
Hence $s_n$ is simple function for each $n \in \N$. 
Let $t \in I$.
Then there exists a unique $N \in \N$ such that $t \in \Omega_N$ so that $\map f t = c_N$.
Then for $n \ge \max \set {\size t, N}$, we have $\map {s_n} t = c_N$. 
Hence we have shown that:
:$\ds \map f t = \lim_{n \mathop \to \infty} \map {s_n} t$ for each $t \in I$.
Since each $s_n$ is a simple function, we have that $f$ is Bochner measurable.
{{qed}}
Category:Simple Functions
Category:Banach Spaces
7whxsv5pcplnna9bcg1ulrpezfgdov0
Theorem: Coslice Category is Isomorphic to Identity Functor Under Object Comma Category/Lemma 1

:$I = J_2 \circ I_1$

Proof:
For each object $g$ in $\mathbf C / C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_2 \circ I_1} g
      | r = \map {J_2} {I_1 g}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_2 \tuple{\operatorname{dom} g,  *, g}
      | c = Definition of $I_1$
}}
{{eqn | r = \tuple{\operatorname{dom} g, g}
      | c = Definition of $J_2$
}}
{{eqn | r = I g
      | c = Definition of $I$
}}
{{end-eqn}}
For each morphism $k : g \to g'$ in $\mathbf C / C$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_2 \circ I_1} k
      | r = \map {J_2} {I_1 k}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_2 \tuple{k, \operatorname{id}_*}
      | c = Definition of $I_1$
}}
{{eqn | r = k
      | c = Definition of $J_2$
}}
{{eqn | r = I k
      | c = Definition of $I$
}}
{{end-eqn}}
It follows that:
:$I = J_2 \circ I_1$
{{qed}}
Category:Coslice Category is Isomorphic to Identity Functor Under Object Comma Category
qyf8hzulwah5v700kve8v6omkfxcqdk
Theorem: Coslice Category is Isomorphic to Identity Functor Under Object Comma Category/Lemma 2

:$J = J_1 \circ I_2$

Proof:
For each object $\tuple{D, f}$ in $\paren{C \downarrow \operatorname{id}_{\mathbf C} }$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_1 \circ I_2} \tuple{D, f}
      | r = \map {J_1} {I_2 \tuple{D, f} }
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_1 \tuple{*, D, f}
      | c = Definition of $I_2$
}}
{{eqn | r = f
      | c = Definition of $J_2$
}}
{{eqn | r = J \tuple{D, f}
      | c = Definition of $J$
}}
{{end-eqn}}
For each morphism $h : \tuple{D, f} \to \tuple{D', f'}$ in $\paren{C \downarrow \operatorname{id}_{\mathbf C} }$ we have:
{{begin-eqn}}
{{eqn | l = \paren{J_1 \circ I_2} h
      | r = \map {J_1} {I_2 h}
      | c = {{Defof|Composite Functor}}
}}
{{eqn | r = J_1 \tuple{\operatorname{id}_*, h}
      | c = Definition of $I_2$
}}
{{eqn | r = h
      | c = Definition of $J_1$
}}
{{eqn | r = J h
      | c = Definition of $J$
}}
{{end-eqn}}
It follows that:
:$J = J_1 \circ I_2$
{{qed}}
Category:Coslice Category is Isomorphic to Identity Functor Under Object Comma Category
eauwv5nju2kr3o3d1lzqheg82bew9dz
Theorem: Banach Space-Valued Simple Function is Bochner Measurable

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 $f : I \to X$ be a simple function.
Then $f$ is Bochner measurable.

Proof:
Define $s_n = f$ for each $n \in \N$.
Then we have:
:$\ds \map f t = \lim_{n \mathop \to \infty} \map {s_n} t$ for each $t \in I$.
Since $s_n$ is simple for each $n \in \N$, we have that $f$ is Bochner measurable.
{{qed}}
Category:Bochner Measurable Functions
cc0e5k9jop4to24z35vhhjw68g1qjbp
Theorem: Simple Function is Bochner Integrable

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 $f : I \to X$ be a simple function.
Then $f$ is Bochner integrable.

Proof:
Let $\lambda$ be the Lebesgue measure on $I$.
Define $s_n = f$ for each $n \in \N$.
Then $s_n$ is a simple function for each $n \in \N$.
We then have:
:$\ds \int_I \norm {\map f t - \map {s_n} t}_X \rd \map \lambda t = \int_I 0 \rd \map \lambda t = 0$
Hence:
:$\ds \lim_{n \mathop \to \infty} \int_I \norm {\map f t - \map {s_n} t}_X \rd \map \lambda t = 0$
Hence $f$ is Bochner integrable.
{{qed}}
Category:Bochner Integrals
122mqfhjcy6s6apevb5glxt9dijxtwg
Theorem: Mass of Earth

The mass $M$ of Earth is given as:
:$M \approx 5 \cdotp 976 \times 10^{24} \, \mathrm {kg}$

Proof:
From Kepler's Third Law of Planetary Motion:
:$T^2 = \dfrac {4 \pi^2} {G M} a^3$
where:
:$T$ is the period of the orbit
:$G$ is the universal gravitational constant
:$M$ is the mass of the body being orbited
:$a$ is the length of the semimajor axis of the orbital ellipse
Though this is a law named for planetary motion, it is a general law for any 2-body bounded motion governed by gravity, including the Earth and Moon.
Solving for $M$ gives
:$(1): \quad M = \dfrac {4 \pi^2} {G T^2} a^3$
We have the following known values:
{{begin-eqn}}
{{eqn | l = G
      | r = 6.674 \times 10^{-11} \, \mathrm N \, \mathrm m^2 \, \mathrm{kg}^{-2}
      | c = {{Defof|Universal Gravitational Constant}}
}}
{{eqn | l = T
      | r = 27.32166 \, \textrm {days}
      | c = Sidereal Period of Moon
}}
{{eqn | r = 2 \, 360 \, 591 \, \textrm s
}}
{{eqn | l = a
      | r = 384 \, 400 \, \textrm {km}
      | c = {{WP|Lunar_Laser_Ranging_experiments|Lunar Laser Ranging experiment}}
}}
{{end-eqn}}
Substituting these values into the $(1)$ yields:
:$M = 6.030 \times 10^{24} \, \textrm {km}$
{{qed}}
Theorem: Bochner Integral of Scalar Multiple of Simple Function

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 $\alpha \in \GF$.
Let $f : I \to X$ be a simple function.
Then:
:$\ds \int \paren {\alpha f} \rd \lambda = \alpha \int f \rd \lambda$
where $\int$ denotes the Bochner integral.

Proof:
From Banach Space-Valued Simple Function has Standard Representation, there exists:
:disjoint Lebesgue measurable sets $E_1, \ldots, E_n \subseteq I$ of finite Lebesgue measure
:$x_1, \ldots, x_n \in X$
such that:
:$\ds \map f t = \sum_{r \mathop = 1}^n x_r \map {\chi_{E_r} } t$ for each $t \in I$.
We then have:
:$\ds \alpha \map f t = \sum_{r \mathop = 1}^n \alpha x_r \map {\chi_{E_r} } t$ for each $t \in I$.
Then:
:$\ds \int \paren {\alpha f} \rd \lambda = \sum_{r \mathop = 1}^n \alpha x_r \map \lambda {E_r}$ 
We can then write:
:$\ds \sum_{r \mathop = 1}^n \alpha x_r \map \lambda {E_r} = \alpha \sum_{r \mathop = 1}^n x_r \map \lambda {E_r} = \alpha \int f \rd \lambda$ 
{{qed}}
Category:Bochner Integrals
i6r6pi9i1rp8soa3brqt1hjm80m41rl
Theorem: Norm of Bochner Integral of Simple Function

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 simple function.
Then:
:$\ds \norm {\int f \rd \lambda}_X \le \int \norm f_X \rd \lambda$
where the $\int$ on the {{LHS}} denotes the Bochner integral, and the $\int$ on the {{RHS}} denotes the Lebesgue integral.

Proof:
From Banach Space-Valued Simple Function has Standard Representation, there exists:
:disjoint Lebesgue measurable sets $E_1, \ldots, E_n \subseteq I$ of finite Lebesgue measure
:$x_1, \ldots, x_n \in X$
such that:
:$\ds \map f t = \sum_{r \mathop = 1}^n x_r \map {\chi_{E_r} } t$ for each $t \in I$.
Then:
:$\ds \int f \rd \lambda = \sum_{r \mathop = 1}^n x_r \map \lambda {E_r}$
By {{NormAxiomVector|3}}, we have:
:$\ds \norm {\int f \rd \lambda}_X \le \sum_{r \mathop = 1}^n \norm {x_r}_X \map \lambda {E_r}$
From Left Composition of Banach Space-Valued Simple Function with Function Fixing Origin is Simple Function, we have that:
:$\ds \norm {\map f t}_X = \sum_{r \mathop = 1}^n \norm {x_r}_X \map {\chi_{E_r} } t$ for each $t \in I$.
Hence:
:$\ds \int \norm f_X \rd \lambda = \sum_{r \mathop = 1}^n \norm {x_r}_X \map \lambda {E_r}$
We conclude that:
:$\ds \norm {\int f \rd \lambda}_X \le \int \norm f_X \rd \lambda$
{{qed}}
Category:Bochner Integrals
5yd9bfha4ztjo3xfge4o8ozn800g46y