avewright/proofwiki-math huggingface dataset:
Theorem: Vertical Section of Cartesian Product

Let $X$ and $Y$ be sets.
Let $A \subseteq X$ and $B \subseteq Y$, so that $A \times B \subseteq X \times Y$. 
Let $x \in X$. 
Then: 
:$\paren {A \times B}_x = \begin{cases}B & x \in A \\ \O & x \not \in A\end{cases}$
where $\paren {A \times B}_x$ is the $x$-vertical section of $A \times B$.

Proof:
Let $x \in A$. 
From the definition of the horizontal section, we have: 
:$y \in \paren {A \times B}_x$
{{iff}}:
:$\tuple {x, y} \in A \times B$ 
Since $x \in A$, this equivalent to: 
:$y \in B$
So:
:$y \in \paren {A \times B}_x$ {{iff}} $y \in B$
giving:
:$\paren {A \times B}_x = B$ if $x \in A$.
Now let $x \in X \setminus A$.
So, by the definition of set difference, we have $x \in X$ and $x \not \in A$.
As before, we have:
:$y \in \paren {A \times B}_x$ 
{{iff}}:
:$\tuple {x, y} \in A \times B$
But this is equivalent to: 
:$x \in A$ and $y \in B$.
Since $x \not \in A$, there exists no $y \in \paren {A \times B}_x$.
So:
:$\paren {A \times B}_x = \O$ if $x \not \in A$.
{{qed}}
Category:Vertical Section of Sets
Category:Cartesian Product
e6n47i69p6t5pm0aenb0v2vdu26pisg
Theorem: Horizontal Section of Measurable Function is Measurable

Let $\struct {X, \Sigma_X}$ and $\struct {Y, \Sigma_Y}$ be measurable spaces.
Let $f : X \times Y \to \overline \R$ be a $\Sigma_X \otimes \Sigma_Y$-measurable function where $\Sigma_X \otimes \Sigma_Y$ is the product $\sigma$-algebra of $\Sigma_X$ and $\Sigma_Y$. 
Let $y \in Y$.
Then: 
:$f^y$ is $\Sigma_X$-measurable
where $f^y$ is the $y$-horizontal section of $f$.

Proof:
By the definition of a $\Sigma_X$-measurable function, we have that: 
:$f^{-1} \sqbrk D \in \Sigma_X \otimes \Sigma_Y$ for each Borel set $D \subseteq \R$.
We aim to show that: 
:$\paren {f^y}^{-1} \sqbrk D \in \Sigma_X$ for each Borel set $D \subseteq \R$.
Let $D \subseteq \R$ be a Borel set. 
From Preimage of Horizontal Section of Function is Horizontal Section of Preimage, we have: 
:$\paren {f^y}^{-1} \sqbrk D = \paren {f^{-1} \sqbrk D}^y$
From Horizontal Section of Measurable Set is Measurable, we have: 
:$\paren {f^{-1} \sqbrk D}^y \in \Sigma_X$
so:
:$\paren {f^y}^{-1} \sqbrk D \in \Sigma_X$
So:
:$\paren {f^y}^{-1} \sqbrk D \in \Sigma_X$ for each Borel set $D \subseteq \R$.
so:
:$f^y$ is $\Sigma_X$-measurable.
{{qed}}
Category:Horizontal Section of Functions
Category:Measurable Functions
am1ycaxa2liwj096padr8idp4awpas9
Theorem: Vertical Section of Measurable Function is Measurable

Let $\struct {X, \Sigma_X}$ and $\struct {Y, \Sigma_Y}$ be measurable spaces.
Let $f : X \times Y \to \overline \R$ be a $\Sigma_X \otimes \Sigma_Y$-measurable function where $\Sigma_X \otimes \Sigma_Y$ is the product $\sigma$-algebra of $\Sigma_X$ and $\Sigma_Y$. 
Let $x \in X$.
Then: 
:$f_x$ is $\Sigma_Y$-measurable
where $f_x$ is the $x$-vertical section of $f$.

Proof:
By the definition of a $\Sigma_X$-measurable function, we have that: 
:$f^{-1} \sqbrk D \in \Sigma_X \otimes \Sigma_Y$ for each Borel set $D \subseteq \R$.
We aim to show that: 
:$\paren {f_x}^{-1} \sqbrk D \in \Sigma_Y$ for each Borel set $D \subseteq \R$.
Let $D \subseteq \R$ be a Borel set. 
From Preimage of Vertical Section of Function is Vertical Section of Preimage, we have: 
:$\paren {f_x}^{-1} \sqbrk D = \paren {f^{-1} \sqbrk D}_x$
From Horizontal Section of Measurable Set is Measurable, we have: 
:$\paren {f^{-1} \sqbrk D}_x \in \Sigma_Y$
so:
:$\paren {f_x}^{-1} \sqbrk D \in \Sigma_Y$
So:
:$\paren {f_x}^{-1} \sqbrk D \in \Sigma_Y$ for each Borel set $D \subseteq \R$.
so:
:$f_x$ is $\Sigma_Y$-measurable.
{{qed}}
Category:Vertical Section of Functions
Category:Measurable Functions
e84babch4ajq61fbcubgdkm4ql85faz
Theorem: Preimage of Vertical Section of Function is Vertical Section of Preimage

Let $X$ and $Y$ be sets.
Let $f : X \times Y \to \overline \R$ be an extended real-valued function. 
Let $x \in X$.
Let $D \subseteq \R$. 
Then: 
:$\paren {f_x}^{-1} \sqbrk D = \paren {f^{-1} \sqbrk D}_x$
where:
:$f_x$ is the $x$-vertical section of $f$
:$\paren {f^{-1} \sqbrk D}_x$ is the $x$-vertical section of $f^{-1} \sqbrk D$.

Proof:
Note that:
:$y \in \paren {f_x}^{-1} \sqbrk D$
{{iff}}: 
:$\map {f_x} y \in D$
from the definition of preimage.
That is, by the definition of the $x$-vertical section: 
:$\map f {x, y} \in D$
From the definition of preimage, this is equivalent to: 
:$\paren {x, y} \in f^{-1} \sqbrk D$
Which in turn is equivalent to: 
:$y \in \paren {f^{-1} \sqbrk D}_x$
from the definition of the $x$-vertical section.
So:
:$y \in \paren {f_x}^{-1} \sqbrk D$ {{iff}} $y \in \paren {f^{-1} \sqbrk D}_x$.
giving:
:$\paren {f_x}^{-1} \sqbrk D = \paren {f^{-1} \sqbrk D}_x$
{{qed}}
Category:Vertical Section of Functions
Category:Vertical Section of Sets
Category:Preimages under Mappings
tcweoi8sjwyjp58mtew0pzz2tdw9xmp
Theorem: Measure of Vertical Section of Cartesian Product

Let $\struct {X, \Sigma_X, \mu}$ and $\struct {Y, \Sigma_Y, \nu}$ be measure spaces.
Let $S_1 \in \Sigma_X$ and $S_2 \in \Sigma_Y$. 
Let $x \in X$. 
Then: 
:$\map {\nu} {\paren {S_1 \times S_2}_x} = \map {\nu} {S_2} \map {\chi_{S_1} } x$
where:
:$\paren {S_1 \times S_2}_x$ is the $x$-vertical section of $S_1 \times S_2$
:$\chi_{S_1}$ is the characteristic function for $S_1$.

Proof:
From Vertical Section of Cartesian Product, we have: 
:$\paren {S_1 \times S_2}_x = \begin{cases}S_2 & x \in S_1 \\ \O & x \not \in S_1\end{cases}$
So:
:$\map {\nu} {\paren {S_1 \times S_2}_x} = \begin{cases}\map {\nu} {S_2} & x \in S_1 \\ 0 & x \not \in S_1\end{cases}$
That is: 
:$\map {\nu} {\paren {S_1 \times S_2}_x} = \map {\nu} {S_2} \times \begin{cases}1 & x \in S_1 \\ 0 & x \not \in S_1\end{cases}$
giving:
:$\map {\nu} {\paren {S_1 \times S_2}_x} = \map {\nu} {S_2} \map {\chi_{S_1} } x$
from the definition of a characteristic function.
{{qed}}
Category:Vertical Section of Sets
Category:Cartesian Product
cbtgc26xsnuw8987pcdjn8xvl4x03o7
Theorem: Measure of Horizontal Section of Cartesian Product

Let $\struct {X, \Sigma_X, \mu_X}$ and $\struct {Y, \Sigma_Y, \mu_Y}$ be measure spaces.
Let $S_1 \in \Sigma_X$ and $S_2 \in \Sigma_Y$. 
Let $y \in Y$. 
Then: 
:$\map {\mu_X} {\paren {S_1 \times S_2}^y} = \map {\mu_X} {S_1} \map {\chi_{S_2} } y$
where:
:$\paren {S_1 \times S_2}^y$ is the $y$-horizontal section of $S_1 \times S_2$
:$\chi_{S_2}$ is the characteristic function for $S_2$.

Proof:
From Horizontal Section of Cartesian Product, we have: 
:$\paren {S_1 \times S_2}^y = \begin{cases}S_1 & y \in S_2 \\ \O & y \not \in S_2\end{cases}$
So:
:$\map {\mu_X} {\paren {S_1 \times S_2}^y} = \begin{cases}\map {\mu_X} {S_1} & y \in S_2 \\ 0 & y \not \in S_2\end{cases}$
That is: 
:$\map {\mu_X} {\paren {S_1 \times S_2}^y} = \map {\mu_X} {S_1} \times \begin{cases}1 & y \in S_2 \\ 0 & y \not \in S_2\end{cases}$
giving:
:$\map {\mu_X} {\paren {S_1 \times S_2}^y} = \map {\mu_X} {S_1} \map {\chi_{S_2} } y$
from the definition of a characteristic function.
{{qed}}
Category:Horizontal Section of Sets
Category:Cartesian Product
8wrxy6emqzhi5jt6wqkeggkhrvwouia
Theorem: Intersection of Horizontal Sections is Horizontal Section of Intersection

Let $X$ and $Y$ be sets.
Let $\set {E_\alpha : \alpha \mathop \in A}$ be a set of subsets of $X \times Y$. 
Let $y \in Y$. 
Then: 
:$\ds \paren {\bigcap_{\alpha \mathop \in A} E_\alpha}^y = \bigcap_{\alpha \mathop \in A} \paren {E_\alpha}^y$
where:
:$\ds \paren {\bigcap_{\alpha \mathop \in A} E_\alpha}^y$ is the $y$-horizontal section of $\ds \bigcap_{\alpha \mathop \in A} E_\alpha$
:$\paren {E_\alpha}^y$ is the $y$-horizontal section of $E_\alpha$.

Proof:
Note that:
:$\ds x \in \bigcap_{\alpha \mathop \in A} \paren {E_\alpha}^y$
{{iff}}: 
:$x \in \paren {E_\alpha}^y$ for all $\alpha \in A$.
From the definition of the $x$-horizontal section, this is equivalent to:
:$\tuple {x, y} \in E_\alpha$ for all $\alpha \in A$. 
This in turn is equivalent to: 
:$\ds \tuple {x, y} \in \bigcap_{\alpha \mathop \in A} E_\alpha$
Again applying the definition of the $x$-horizontal section, this is equivalent to:
:$\ds x \in \paren {\bigcap_{\alpha \mathop \in A} E_\alpha}^y$
So:
:$\ds x \in \bigcap_{\alpha \mathop \in A} \paren {E_\alpha}^y$ {{iff}} $\ds x \in \paren {\bigcap_{\alpha \mathop \in A} E_\alpha}^y$
giving:
:$\ds \paren {\bigcap_{\alpha \mathop \in A} E_\alpha}^y = \bigcap_{\alpha \mathop \in A} \paren {E_\alpha}^y$
{{qed}}
Category:Set Intersection
Category:Horizontal Section of Sets
7ndfc42t4jrobqhvacnrguc7t95ze4d
Theorem: Vertical Section of Empty Set

Let $X$ and $Y$ be sets. 
Let $x \in X$. 
Then: 
:$\O_x = \O$
where $\O$ is the empty set and $\O_x$ is the $x$-vertical section of $\O$.

Proof:
{{AimForCont}} suppose that: 
:$y \in \O_x$
Then from the definition of the $x$-vertical section, we have: 
:$\tuple {x, y} \in \O$
This is impossible from the definition of the empty set.
So:
:there exists no $y \in \O_x$
giving:
:$\O_x = \O$
{{qed}}
Category:Vertical Section of Sets
lmoohqlk21jxeb460jwac7p71ynwtis
Theorem: Horizontal Section of Empty Set

Let $X$ and $Y$ be sets. 
Let $y \in Y$. 
Then: 
:$\O^y = \O$
where $\O$ is the empty set and $\O^y$ is the $y$-horizontal section of $\O$.

Proof:
{{AimForCont}} suppose that: 
:$x \in \O^y$
Then from the definition of the $x$-vertical section, we have: 
:$\tuple {x, y} \in \O$
This is impossible from the definition of the empty set.
So:
:there exists no $x \in \O^y$
giving:
:$\O_x = \O$
{{qed}}
Category:Horizontal Section of Sets
lwr8z5v192p5xwbd7io581o0wedbi81
Theorem: Pointwise Sum of Measurable Functions is Measurable/General Result

Let $\sequence {\alpha_n}_{n \mathop \in \N}$ be a sequence of real numbers.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence of $\Sigma$-measurable functions $f_n : X \to \overline \R$ such that: 
:for each $N \in \N$ and $x \in X$, the sum $\ds \sum_{n \mathop = 1}^N \alpha_n \map {f_n} x$ is well-defined.
Then: 
:$\ds \sum_{n \mathop = 1}^N \alpha_n f_n$ is $\Sigma$-measurable.

Proof:
We proceed by induction.
For all $N \in \N$ let $\map P N$ be the proposition:
:$\ds \sum_{n \mathop = 1}^N \alpha_n f_n$ is $\Sigma$-measurable.
Theorem: Vertical Section of Linear Combination of Functions is Linear Combination of Vertical Sections

Let $X$ and $Y$ be sets.
Let $f_1, f_2, \ldots, f_n : X \times Y \to \overline \R$ be functions. 
Let $\alpha_1, \alpha_2, \ldots, \alpha_n$ be real numbers.
Let $x \in X$. 
Then: 
:$\ds \paren {\sum_{k \mathop = 1}^n \alpha_k f_k}_x = \sum_{k \mathop = 1}^n \alpha_k \paren {f_k}_x$
where $f_x$ denotes the $x$-vertical section of the function $f$.

Proof:
Let $y \in Y$. 
We have:
{{begin-eqn}}
{{eqn	| l = \map {\paren {\sum_{k \mathop = 1}^n \alpha_k f_k}_x} y
		| r = \map {\paren {\sum_{k \mathop = 1}^n \alpha_k f_k} } {x, y}
		| c = {{Defof|Vertical Section of Function}}
}}
{{eqn	| r = \sum_{k \mathop = 1}^n \alpha_k \map {f_k} {x, y}
}}
{{eqn	| r = \sum_{k \mathop = 1}^n \alpha_k \map {\paren {f_k}_x} y
		| c = {{defof|Vertical Section of Function}}
}}
{{end-eqn}}
so:
:$\ds \paren {\sum_{k \mathop = 1}^n \alpha_k f_k}_x = \sum_{k \mathop = 1}^n \alpha_k \paren {f_k}_x$
{{qed}}
Category:Vertical Section of Functions
r07k0yej1we0yxf4h7axwrvs9phinbl
Theorem: Horizontal Section of Simple Function is Simple Function

Let $\struct {X, \Sigma_X}$ and $\struct {Y, \Sigma_Y}$ be measurable spaces.
Let $\struct {X \times Y, \Sigma_X \otimes \Sigma_Y}$ be the product measurable space of $\struct {X, \Sigma_X}$ and $\struct {Y, \Sigma_Y}$.
Let $f : X \times Y \to \R$ be a simple function.
Let $y \in Y$. 
Then $f^y : X \to \R$ is a simple function, where $f^y$ is the $y$-horizontal section of $f$.

Proof:
Write the standard representation of $f$ as: 
:$\ds f = \sum_{k \mathop = 1}^n a_k \chi_{E_k}$
with:
:$E_1, E_2, \ldots, E_n$ pairwise disjoint $\Sigma_X \otimes \Sigma_Y$-measurable sets
:$a_1, a_2, \ldots, a_n$ real numbers.
We have: 
{{begin-eqn}}
{{eqn	| l = f^y
		| r = \paren {\sum_{k \mathop = 1}^n a_k \chi_{E_k} }^y
}}
{{eqn	| r = \sum_{k \mathop = 1}^n a_k \paren {\chi_{E_k} }^y
		| c = Horizontal Section of Linear Combination of Functions is Linear Combination of Horizontal Sections
}}
{{eqn	| r = \sum_{k \mathop = 1}^n a_k \chi_{\paren {E_k}^y}
		| c = Horizontal Section of Characteristic Function is Characteristic Function of Horizontal Section
}}
{{end-eqn}}
From Intersection of Horizontal Sections is Horizontal Section of Intersection, we have that: 
:$\paren {E_1}^y, \paren {E_2}^y, \ldots, \paren {E_n}^y$ are pairwise disjoint.
From Horizontal Section of Measurable Set is Measurable, we have that: 
:$\paren {E_1}^y, \paren {E_2}^y, \ldots, \paren {E_n}^y$ are $\Sigma_X$-measurable.
So, we have: 
:$\ds f^y = \sum_{k \mathop = 1}^n a_k \chi_{\paren {E_k}^y}$
with:
:$\paren {E_1}^y, \paren {E_2}^y, \ldots, \paren {E_n}^y$ pairwise disjoint $\Sigma_X$-measurable sets
:$a_1, a_2, \ldots, a_n$ real numbers.
So $f^y$ is a simple function.
{{qed}}
Category:Horizontal Section of Functions
Category:Simple Functions
e29r2p8f9munc4hu6d5hvudegj7s9k2
Theorem: Vertical Section preserves Increasing Sequences of Functions

Let $X$ and $Y$ be sets.
Let $\sequence {f_n}_{n \mathop \in \N}$ be an increasing sequence of real-valued functions with $f_i : X \times Y \to \overline \R$ for each $i$. 
Let $x \in X$. 
Then the sequence $\sequence {\paren {f_n}_x}_{n \mathop \in \N}$ is increasing, where $\paren {f_n}_x$ denotes the $x$-vertical section of $f_n$.

Proof:
Since $\sequence {f_n}_{n \mathop \in \N}$ is an increasing sequence of real-valued functions, we have: 
:$\map {f_i} {x, y} \le \map {f_j} {x, y}$ for all $i, j$ with $i \le j$. 
for all $\tuple {x, y} \in X \times Y$.
In particular, for fixed $x \in X$, we have: 
:$\map {f_i} {x, y} \le \map {f_j} {x, y}$ for all $i, j$ with $i \le j$ and all $y \in Y$.
From the definition of the $x$-vertical section, we have: 
:$\map {\paren {f_i}_x} y \le \map {\paren {f_j}_x} y$ for all $i, j$ with $i \le j$ and all $y \in Y$.
So: 
:$\sequence {\paren {f_n}_x}_{n \mathop \in \N}$ is an increasing sequence of real-valued functions.
{{qed}}
Category:Vertical Section of Functions
rplv0vi4wwe5fyyflzyagv2vhqhe7ta
Theorem: Vertical Section preserves Pointwise Limits of Sequences of Functions

Let $X$ and $Y$ be sets. 
Let $f : X \times Y \to \overline \R$ be a function.
Let $\sequence {f_n}_{n \mathop \in \N}$ be a sequence of functions converging pointwise to $f$. 
Let $x \in X$. 
Then: 
:$\paren {f_n}_x \to f_x$
pointwise, where: 
:$\paren {f_n}_x$ denotes the $x$-vertical section of $f_n$
:$f_x$ denotes the $x$-vertical section of $f$.

Proof:
From the definition of pointwise convergence, we have: 
:$\ds \map f {x, y} = \lim_{n \mathop \to \infty} \map {f_n} {x, y}$
for each $x \in X$ and $y \in Y$. 
Fix $x \in X$. 
From the definition of the $x$-vertical section, we have: 
:$\map {f_n} {x, y} = \map {\paren {f_n}_x} y$
and:
:$\map f {x, y} = \map {f_x} y$
So:
:$\ds \map {f_x} y = \lim_{n \mathop \to \infty} \map {\paren {f_n}_x} y$
for each $y \in Y$. 
So:
:$\paren {f_n}_x \to f_x$
pointwise.
{{qed}}
Category:Vertical Section of Functions
8cq9qob98dyb6cmlqf2p3t5q5x64i67
Theorem: Gamma Function of 4

:$\map \Gamma 4 = 6$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Gamma 4
      | r = \map \Gamma {3 + 1}
      | c = 
}}
{{eqn | r = 3 \map \Gamma 3
      | c = Gamma Difference Equation
}}
{{eqn | r = 3 \times 2
      | c = Gamma Function of 3
}}
{{end-eqn}}
{{qed}}
Theorem: Characteristic Function of Disjoint Union

Let $X$ be a set. 
Let $\sequence {D_n}_{n \mathop \in \N}$ be a sequence of pairwise disjoint subsets of $X$. 
Let: 
:$\ds D = \bigcup_{n \mathop = 1}^\infty D_n$
Then: 
:$\ds \chi_D = \sum_{n \mathop = 1}^\infty \chi_{D_n}$
where:
:$\chi_D$ is the characteristic function of $D$
:$\chi_{D_n}$ is the characteristic function of $D_n$.

Proof:
We aim to show that: 
:$\ds \sum_{n \mathop = 1}^\infty \map {\chi_{D_n} } x = \begin{cases}1 & x \in D \\ 0 & x \in X \setminus D\end{cases}$
at which point we will have the demand from the definition of a characteristic function.
Let $x \in D$. 
Then: 
:$\ds x \in \bigcup_{n \mathop = 1}^\infty D_n$ 
From the definition of set union, we have: 
:$x \in D_n$ for some $n \in \N$. 
Since the sets $\sequence {D_n}_{n \mathop \in \N}$ are pairwise disjoint, we have: 
:$x \in D_n$ for precisely one $n \in \N$.
That is, form the definition of a characteristic function:
:$\map {\chi_{D_n} } x = 1$ for precisely one $n \in \N$. 
So that: 
:$\ds \sum_{n \mathop = 1}^\infty \map {\chi_{D_n} } x = 1$
as desired.
Let $x \in X \setminus D$.
Then: 
:$\ds x \in X \setminus \bigcup_{n \mathop = 1}^\infty D_n$ 
so from the set difference:
:$x \in X$ and $\ds x \not \in \bigcup_{n \mathop = 1}^\infty D_n$.
So, from the definition of set union:
:$x \not \in D_n$ for all $n \in \N$. 
That is, form the definition of a characteristic function:
:$\map {\chi_{D_n} } x = 0$ for all $n \in \N$. 
So that: 
:$\ds \sum_{n \mathop = 1}^\infty \map {\chi_{D_n} } x = 0$
as desired.
{{qed}}
Category:Characteristic Functions
Category:Set Union
Category:Characteristic Function of Disjoint Union
a4snwzxqa1rdds56q1562u2b6d11ji3
Theorem: Integral of Positive Measurable Function over Disjoint Union

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f : X \to \overline \R$ be a positive $\Sigma$-measurable function.
Let $\sequence {D_n}_{n \mathop \in \N}$ be a sequence of pairwise disjoint $\Sigma$-measurable sets.
Let: 
:$\ds D = \bigcup_{n \mathop = 1}^\infty D_n$
Then: 
:$\ds \int_D f \rd \mu = \sum_{n \mathop = 1}^\infty \int_{D_n} f \rd \mu$

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \int_D f \rd \mu 
		| r = \int \paren {f \times \chi_D} \rd \mu
		| c = {{Defof|Integral of Positive Measurable Function over Measurable Set}}
}}
{{eqn	| r = \int \paren {f \times \paren {\sum_{n \mathop = 1}^\infty \chi_{D_n} } } \rd \mu
		| c = Characteristic Function of Disjoint Union
}}
{{eqn	| r = \int \paren {\sum_{n \mathop = 1}^\infty \paren {f \times \chi_{D_n} } } \rd \mu
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \paren {\int \paren {f \times \chi_{D_n} } \rd \mu}
		| c = Integral of Series of Positive Measurable Functions
}}
{{eqn	| r = \sum_{n \mathop = 1}^\infty \int_{D_n} f_n \rd \mu
		| c = {{Defof|Integral of Positive Measurable Function over Measurable Set}}
}}
{{end-eqn}}
{{qed}}
Category:Integral of Positive Measurable Function over Measurable Set
0uqjymbgswvc81yl5in3le5zra3o9t0
Theorem: Integral of Positive Measurable Function over Measurable Set is Well-Defined

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $A \in \Sigma$. 
Let $f : X \to \overline \R$ be a positive $\Sigma$-measurable function.
Then the $\mu$-integral of $f$ over $A$ defined by: 
:$\ds \int_A f \rd \mu = \int \paren {\chi_A \cdot f} \rd \mu$
is well-defined.

Proof:
We simply need to show that: 
:$\chi_A \cdot f$ is a positive $\Sigma$-measurable function.
For $x \in A$, we have: 
{{begin-eqn}}
{{eqn	| l = \map {\paren {\chi_A \cdot f} } x
		| r = \map {\chi_A} x \map f x
		| c = {{Defof|Pointwise Multiplication}}
}}
{{eqn	| r = \map f x
		| c = {{Defof|Characteristic Function of Set}}
}}
{{eqn	| o = \ge
		| r = 0
}}
{{end-eqn}}
For $x \in X \setminus A$, we have:
{{begin-eqn}}
{{eqn	| l = \map {\paren {\chi_A \cdot f} } x
		| r = \map {\chi_A} x \map f x
		| c = {{Defof|Pointwise Multiplication}}
}}
{{eqn	| r = 0
		| c = {{Defof|Characteristic Function of Set}}
}}
{{end-eqn}}
so:
:$\chi_A \cdot f$ is non-negative. 
We now show that $\chi_A \cdot f$ is $\Sigma$-measurable.
From Characteristic Function Measurable iff Set Measurable, we have: 
:$\chi_A$ is $\Sigma$-measurable.
From Pointwise Product of Measurable Functions is Measurable, we then have: 
:$\chi_A \cdot f$ is $\Sigma$-measurable.
So:
:$\chi_A \cdot f$ is a positive $\Sigma$-measurable function.
So its $\mu$-integral is well-defined.
{{qed}}
Category:Integral of Positive Measurable Function over Measurable Set
iagvzzbpo03wwtcf0zkjhsuq73l2m3v
Theorem: Measurable Function is Integrable iff A.E. Equal to Real-Valued Integrable Function

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $f : X \to \overline \R$ be a $\Sigma$-measurable function.
Then $f$ is $\mu$-integrable {{iff}}:
:there exists a $\mu$-integrable function $g : X \to \R$ such that $g = f$ $\mu$-almost everywhere.

Proof:
=== Sufficient Condition ===
Suppose that: 
:there exists a $\mu$-integrable function $g : X \to \R$ such that $g = f$ $\mu$-almost everywhere.
Then, from A.E. Equal Positive Measurable Functions have Equal Integrals: Corollary 1, we have: 
:$f$ is $\mu$-integrable.
{{qed|lemma}}
Theorem: Integral of Positive Measurable Function is Additive/Corollary

Let $A \in \Sigma$. 
Then: 
:$\ds \int_A \paren {f + g} \rd \mu = \int_A f \rd \mu + \int_A g \rd \mu$
where:
:$f + g$ is the pointwise sum of $f$ and $g$
:the integral sign denotes $\mu$-integration over $A$.
This can be summarized by saying that $\ds \int_A \cdot \rd \mu$ is additive.

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \int_A \paren {f + g} \rd \mu
		| r = \int \paren {f + g} \times \chi_A \rd \mu
		| c = {{Defof|Integral of Positive Measurable Function over Measurable Set}}
}}
{{eqn	| r = \int \paren {f \times \chi_A + g \times \chi_A} \rd \mu
}}
{{eqn	| r = \int \paren {f \times \chi_A} \rd \mu + \int \paren {g \times \chi_A} \rd \mu
		| c = Integral of Positive Measurable Function is Additive
}}
{{eqn	| r = \int_A f \rd \mu + \int_A g \rd \mu
		| c = {{Defof|Integral of Positive Measurable Function over Measurable Set}}
}}
{{end-eqn}}
{{qed}}
Category:Integral of Positive Measurable Function is Additive
Category:Integral of Positive Measurable Function over Measurable Set
mfraihemkatctpmpvb1wetzww0s4lus
Theorem: Linear Combination of Signed Measures is Signed Measure

Let $\struct {X, \Sigma}$ be a measurable space.
Let $\mu$ and $\nu$ be signed measures on $\struct {X, \Sigma}$.
Let $\alpha, \beta \in \overline \R$. 
Suppose that the sum: 
:$\alpha \map \mu A + \beta \map \nu A$
is well-defined for each $A \in \Sigma$. 
Then: 
:$\xi = \alpha \mu + \beta \nu$ is a signed measure.

Proof:
We verify both of the conditions for a signed measure.
Theorem: Absolute Value of Signed Measure Bounded Above by Variation

Let $\struct {X, \Sigma}$ be a measurable space. 
Let $\mu$ be a signed measure on $\struct {X, \Sigma}$. 
Let $\size \mu$ be the variation of $\mu$. 
Then: 
:$\size {\map \mu A} \le \map {\size \mu} A$
for each $A \in \Sigma$.

Proof:
Let $\tuple {\mu^+, \mu^-}$ be the Jordan decomposition of $\mu$.
Then: 
:$\mu = \mu^+ - \mu^-$
and:
:$\size \mu = \mu^+ + \mu^-$
We have: 
{{begin-eqn}}
{{eqn	| l = \size {\map \mu A}
		| r = \size {\map {\mu^+} A - \map {\mu^-} A}
}}
{{eqn	| o = \le
		| r = \size {\map {\mu^+} A} + \size {\map {\mu^-} A}
		| c = Triangle Inequality
}}
{{eqn	| r = \map {\mu^+} A + \map {\mu^-} A
		| c = since $\mu^+ \ge 0$ and $\mu^- \ge 0$
}}
{{eqn	| r = \map {\size \mu} A
}}
{{end-eqn}}
{{qed}}