avewright/proofwiki-math huggingface dataset:
Theorem: Conditional Expectation Conditioned on Event of Non-Zero Probability

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ be an integrable random variable on $\struct {\Omega, \Sigma, \Pr}$.
Let $B \in \Sigma$ be an event with:
:$\map \Pr B > 0$
Let:
:$\GG = \map \sigma B = \set {\O, B, B^c, \Omega}$
where $\map \sigma B$ is the $\sigma$-algebra generated by $B$.
Let: 
:$\ds \alpha = \frac {\expect {X \cdot 1_B} } {\map \Pr B}$
and:
:$\ds \beta = \frac {\expect {X \cdot 1_{B^c} } } {\map \Pr {B^c} }$
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Then:
:$\ds \expect {X \mid \GG} = \alpha \cdot 1_B + \beta \cdot 1_{B^c}$ almost everywhere.

Proof:
We show that:
:$\ds Z = \alpha \cdot 1_B + \beta \cdot 1_{B^c}$ is a version of the conditional expectation of $X$ given $\GG$.
We will then be done by Existence and Essential Uniqueness of Conditional Expectation Conditioned on Sigma-Algebra.
From Characteristic Function Measurable iff Set Measurable, $1_B$ and $1_{B^c}$ are both measurable functions.
From Pointwise Product of Measurable Functions is Measurable and Pointwise Sum of Measurable Functions is Measurable, we therefore have that $Z$ is a random variable. 
So we now verify that the expectations take the correct values. 
From Integral of Integrable Function over Null Set, we have: 
:$\expect {Z \cdot 1_\O} = 0 = \expect {X \cdot 1_\O}$
We also have: 
{{begin-eqn}}
{{eqn	| l = \expect {Z \cdot 1_B}
		| r = \expect {\alpha \cdot 1_B + \beta \cdot 1_B \cdot 1_{B^c} }
}}
{{eqn	| r = \expect {\alpha \cdot 1_B}
		| c = Characteristic Function of Intersection
}}
{{eqn	| r = \alpha \map \Pr B
		| c = Expectation is Linear: General Case, Integral of Characteristic Function
}}
{{eqn	| r = \expect {X \cdot 1_B}
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn	| l = \expect {Z \cdot 1_{B^c} }
		| r = \expect {\alpha \cdot 1_B \cdot 1_{B^c} + \beta \cdot 1_{B^c} }
}}
{{eqn	| r = \expect {\beta \cdot 1_{B^c} }
		| c = Characteristic Function of Intersection
}}
{{eqn	| r = \beta \map \Pr {B^c}
		| c = Expectation is Linear: General Case, Integral of Characteristic Function
}}
{{eqn	| r = \expect {X \cdot 1_{B^c} }
}}
{{end-eqn}}
Finally, we have: 
{{begin-eqn}}
{{eqn	| l = \expect Z
		| r = \expect {\alpha \cdot 1_B + \beta \cdot 1_{B^c} }
}}
{{eqn	| r = \alpha \map \Pr B + \beta \map \Pr {B^c}
		| c = Expectation is Linear: General Case, Integral of Characteristic Function
}}
{{eqn	| r = \expect {X \cdot 1_B} + \expect {X \cdot 1_{B^c} }
}}
{{eqn	| r = \expect {X \cdot \paren {1_B + 1_{B^c} } }
		| c = Expectation is Linear: General Case
}}
{{eqn	| r = \expect X
		| c = Characteristic Function of Disjoint Union
}}
{{end-eqn}}
{{qed}}
Category:Conditional Expectation
lpwjliq2ho8h1mhgbzs5n9qx2hdim7q
Theorem: Triangle Inequality for Conditional Expectation

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
Let $X$ be an integrable random variable.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Let $\expect {\size X \mid \GG}$ be a version of the conditional expectation of $\size X$ given $\GG$.
Then we have: 
:$\size {\expect {X \mid \GG} } \le \expect {\size X \mid \GG}$ almost everywhere.

Proof:
From Conditional Expectation is Monotone, we have: 
:$\expect {X^+ \mid \GG} \ge 0$ almost everywhere
and:
:$\expect {X^- \mid \GG} \ge 0$ almost everywhere
where $X^+$ and $X^-$ are the positive and negative parts respectively. 
Now, almost everywhere we have:
{{begin-eqn}}
{{eqn	| l = \size {\expect {X \mid \GG} }
		| r = \size {\expect {X^+ - X^- \mid \GG} } 
}}
{{eqn	| r = \size {\expect {X^+ \mid \GG} - \expect {X^- \mid \GG} } 
		| c = Conditional Expectation is Linear
}}
{{eqn	| o = \le
		| r = \size {\expect {X^+ \mid \GG} } + \size {\expect {X^- \mid \GG} }
		| c = Triangle Inequality for Real Numbers
}}
{{eqn	| r = \expect {X^+ \mid \GG} + \expect {X^- \mid \GG}
}}
{{eqn	| r = \expect {X^+ + X^- \mid \GG}
		| c = Conditional Expectation is Linear
}}
{{eqn	| r = \expect {\size X \mid \GG}
		| c = Sum of Positive and Negative Parts
}}
{{end-eqn}}
{{qed}}
Category:Conditional Expectation
sghfugofzfjck75mmekrcuxsie8yy56
Theorem: Conditional Expectation of Constant

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
Let $c \in \R$.
Define $X : \Omega \to \R$ by $\map X \omega = c$ for each $\omega \in \Omega$.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Then:
:$\expect {X \mid \GG} = c$ almost everywhere.

Proof:
From Constant Function is Measurable, $X$ is a real-valued random variable.
The result then follows immediately from Conditional Expectation of Measurable Random Variable.
{{qed}}
Category:Conditional Expectation
7t34wd6gqauyohn7r6a2sr8ztllvgxz
Theorem: Conditional Expectation of Non-Negative Random Variable is Non-Negative

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
Let $X$ be an integrable random variable such that:
:$X \ge 0$ almost everywhere.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Then:
:$\expect {X \mid \GG} \ge 0$ almost everywhere.

Proof:
From Conditional Expectation is Monotone, we have:
:$\expect {X \mid \GG} \ge \expect {0 \mid \GG}$ almost everywhere.
From Conditional Expectation of Constant, we have:
:$\expect {0 \mid \GG} = 0$ almost everywhere.
So:
:$\expect {X \mid \GG} \ge 0$ almost everywhere.
{{qed}}
Theorem: Conditional Fatou's Lemma

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ be an non-negative integrable random variable.
Let $\sequence {X_n}_{n \in \N}$ be an sequence of non-negative integrable random variables.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
For each $n \in \N$, let $\expect {X_n \mid \GG}$ be a version of the conditional expectation of $X_n$ conditioned on $\GG$.
Let $\ds \expect {\liminf_{n \mathop \to \infty} X_n \mid \GG}$ be a version of the conditional expectation of $X$ conditioned on $\GG$.
Then we have: 
:$\ds \expect {\liminf_{n \mathop \to \infty} X_n \mid \GG} \le \liminf_{n \mathop \to \infty} \expect {X_n \mid \GG}$ almost everywhere.

Proof:
From Conditional Expectation of Measurable Random Variable, we have:
:$\expect {X_n \mid \GG} = \expect {\expect {X_n \mid \GG} \mid \GG}$
It therefore suffices to show, from Conditional Expectation is Linear:
:$\ds \expect {\liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} - \liminf_{n \mathop \to \infty} X_n \mid \GG} \ge 0$ almost everywhere.
From Condition for Conditional Expectation to be Almost Surely Non-Negative, we can show that:
:$\ds \expect {\paren {\liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} - \liminf_{n \mathop \to \infty} X_n} \cdot 1_A} \ge 0$
for $A \in \GG$.
We indeed have, for each $A \in \GG$: 
{{begin-eqn}}
{{eqn	| l = \expect {\paren {\liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} - \liminf_{n \mathop \to \infty} X_n} \cdot 1_A}
		| r = \int_A \paren {\liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} - \liminf_{n \mathop \to \infty} X_n} \rd \Pr
}}
{{eqn	| r = \int_A \paren {\liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} } \rd \Pr - \int_A \liminf_{n \mathop \to \infty} X_n \rd \Pr
		| c = Integral of Integrable Function is Additive: Corollary 2
}}
{{eqn	| o = \ge
		| r = \int_A \paren {\liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} } \rd \Pr - \liminf_{n \mathop \to \infty} \int_A X_n \rd \Pr
		| c = Fatou's Lemma for Integrals
}}
{{eqn	| r = \int_A \paren {\liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} } \rd \Pr - \liminf_{n \mathop \to \infty} \int_A \expect {X_n \mid \GG} \rd \Pr
		| c = {{Defof|Conditional Expectation on Sigma-Algebra}}
}}
{{eqn	| o = \ge
		| r = 0
		| c = Fatou's Lemma for Integrals
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Pierre Joseph Louis Fatou|cat = Fatou}}
Theorem: Conditional Dominated Convergence Theorem

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $X$ be an integrable random variable.
Let $\sequence {X_n}_{n \in \N}$ be an sequence of non-negative integrable random variables converging almost surely to $X$, such that: 
:there exists an integrable random variable $Y$ such that:
::$\size {X_n} \le Y$ almost surely.
Let $\GG \subseteq \Sigma$ be a sub-$\sigma$-algebra.
For each $n \in \N$, let $\expect {X_n \mid \GG}$ be a version of the conditional expectation of $X_n$ conditioned on $\GG$.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ conditioned on $\GG$.
Then, we have: 
:$\ds \lim_{n \mathop \to \infty} \expect {X_n \mid \GG} = \expect {X \mid \GG}$ almost surely.

Proof:
Let $\expect {Y \mid \GG}$ be a version of the conditional expectation of $Y$ conditioned on $\GG$.
For each $n \in \N$, let $\expect {X_n \mid \GG}$ be a version of the conditional expectation of $X_n$ conditioned on $\GG$.
Since we have: 
:$\size {X_n} \le Y$ almost surely.
and $Y$ is integrable, we have: 
:$\ds \limsup_{n \mathop \to \infty} \expect {X_n \mid \GG} \le \expect {\limsup_{n \mathop \to \infty} X_n \mid \GG} = \expect {X \mid \GG}$ almost surely
by Conditional Reverse Fatou's Lemma. 
From Conditional Fatou's Lemma, we have: 
:$\ds \expect {X \mid \GG} = \expect {\liminf_{n \mathop \to \infty} X_n \mid \GG} \le \liminf_{n \mathop \to \infty} \expect {X_n \mid \GG}$ almost surely.
So almost surely, we have: 
:$\ds \limsup_{n \mathop \to \infty} \expect {X_n \mid \GG} \le \expect {X \mid \GG} \le \liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} \le \limsup_{n \mathop \to \infty} \expect {X_n \mid \GG}$
So almost surely, we have:
:$\ds \liminf_{n \mathop \to \infty} \expect {X_n \mid \GG} = \limsup_{n \mathop \to \infty} \expect {X_n \mid \GG} = \expect {X \mid \GG}$
So, from Convergence of Limsup and Liminf, we have: 
:$\ds \lim_{n \mathop \to \infty} \expect {X_n \mid \GG}$ exists almost surely
and further:
:$\ds \expect {X \mid \GG} = \lim_{n \mathop \to \infty} \expect {X_n \mid \GG}$ almost surely.
{{qed}}
Theorem: Set Difference is Right Distributive over Set Intersection/General Case

Let $U$ be a collection of sets.
Let $T$ be a set.
Then:
:$\ds \bigcap_{X \mathop \in U} \paren {X \setminus T} = \paren {\bigcap_{X \mathop \in U} X} \setminus T$
That is, the difference with an intersection equals the intersection of the differences.

Proof:
{{begin-eqn}}
{{eqn | l = x
      | o = \in
      | r = \bigcap_{X \mathop \in U} \paren {X \setminus T}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall X \in U
      | l = x
      | o = \in
      | r = X \setminus T
      | c = {{Defof|Set Intersection}}
}}
{{eqn | ll= \leadstoandfrom
      | q = \forall X \in U
      | l = x
      | o = \in
      | r = X
      | c = {{Defof|Set Difference}}
}}
{{eqn | lo= \land
      | l = x
      | o = \not \in
      | r = T
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \bigcap_{X \mathop \in U}
      | c = {{Defof|Set Intersection}}
}}
{{eqn | lo= \land 
      | l = x
      | o = \not \in
      | r = T
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = \paren {\bigcap_{X \mathop \in U} X} \setminus T
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}
Theorem: Conditional Expectation Unchanged on Conditioning on Independent Sigma-Algebra/Corollary

Let $\HH \subseteq \Sigma$ be a sub-$\sigma$-algebra.
Let $X$ be a integrable random variable such that: 
:$\map \sigma X$ is independent of $\HH$
where $\map \sigma X$ is the $\sigma$-algebra generated by $X$. 
Let $\expect {X \mid \HH}$ be a version of the conditional expectation of $X$ given $\GG$.
Then: 
:$\expect {X \mid \HH} = \expect X$ almost surely.

Proof:
Note that: 
:$\map \sigma X = \map \sigma {\set {\O, \Omega}, \map \sigma X}$ 
So by Conditional Expectation Unchanged on Conditioning on Independent Sigma-Algebra, we have:
:$\expect {X \mid \map \sigma {\set {\O, \Omega}, \HH} } = \expect {X \mid \set {\O, \Omega} }$
From Conditional Expectation Conditioned on Trivial Sigma-Algebra, we have:
:$\expect {X \mid \set {\O, \Omega} } = \expect X$ almost surely.
Also, since: 
:$\set {\O, \Omega} \subseteq \HH$
we have that:
:$\map \sigma {\set {\O, \Omega}, \HH} = \HH$ 
giving:
:$\expect {X \mid \HH} = \expect X$ almost surely.
{{qed}}
Theorem: Sum of Independent Random Variables with Mean Zero is Martingale

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\sequence {X_n}_{n \mathop \ge 0}$ be a sequence of integrable independent random variables with:
:$\expect {X_n} = 0$ for each $n \in \N$
and: 
:$X_0 = 0$
For $n \ge 0$ define:
:$\ds S_n = \sum_{i \mathop = 0}^n X_i$
Let $\sequence {\FF_n^X}_{n \mathop \ge 0}$ be the natural filtration for $\sequence {X_n}_{n \mathop \ge 0}$. 
Then $\sequence {S_n}_{n \mathop \ge 0}$ is a $\sequence {\FF_n^X}_{n \mathop \ge 0}$-martingale.

Proof:
We first show that $\sequence {S_n}_{n \mathop \ge 0}$ is $\sequence {\FF_n^X}_{n \mathop \ge 0}$-adapted.
From the definition of the $\sigma$-algebra generated by a collection of mappings, we have:
:$X_i$ is $\map \sigma {X_0, \ldots, X_n}$-measurable for $0 \le i \le n$.
So from Pointwise Sum of Measurable Functions is Measurable: General Result, we have:
:$S_n$ is $\map \sigma {X_0, \ldots, X_n}$-measurable.
By the definition of the natural filtration, we have:
:$\map \sigma {X_0, \ldots, X_n} = \FF_n^X$
and hence $\sequence {S_n}_{n \mathop \ge 0}$ is $\sequence {\FF_n^X}_{n \mathop \ge 0}$-adapted.
Now let $n \ge 0$. 
We have:
{{begin-eqn}}
{{eqn	| l = \expect {S_{n + 1} \mid \FF_n^X}
		| r = \expect {X_{n + 1} + S_n \mid \FF_n^X}
}}
{{eqn	| r = \expect {X_{n + 1} \mid \FF_n^X} + \expect {S_n \mid \FF_n^X}
		| c = Conditional Expectation is Linear
}}
{{eqn	| r = \expect {X_{n + 1} \mid \FF_n^X} + S_n
		| c = Conditional Expectation of Measurable Random Variable
}}
{{end-eqn}}
almost surely.
From Random Variable Independent of Sigma-Algebra Generated by Independent Random Variables, we have: 
:$\map \sigma {X_{n + 1} }$ is independent from $\FF_n^X$. 
So, from Conditional Expectation Unchanged on Conditioning on Independent Sigma-Algebra: Corollary we have:
:$\expect {X_{n + 1} \mid \FF_n^X} = \expect {X_{n + 1} } = 0$ almost surely.
So we have:
:$\expect {S_{n + 1} \mid \FF_n^X} = S_n$ almost surely. 
So $\sequence {S_n}_{n \mathop \ge 0}$ is a $\sequence {\FF_n^X}_{n \mathop \ge 0}$-martingale.
{{qed}}
Theorem: Equivalence of Definitions of Stopping Time in Discrete Time

Let $\struct {\Omega, \Sigma, \sequence {\FF_n}_{n \ge 0}, \Pr}$ be a filtered probability space.
Let $T : \Omega \to \Z_{\ge 0} \cup \set {\infty}$ be a function.
{{TFAE|def = Stopping Time|stopping time}}

Proof:
=== Definition 1 implies Definition 2 ===
Suppose that:
:$\set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
for all $t \in \Z_{\ge 0}$.
Setting $t = 0$ this certainly implies:
:$\set {\omega \in \Omega : \map T \omega = t} \in \FF_t$
Now take $t \ge 1$ a positive integer.
We have: 
:$\set {\omega \in \Omega : \map T \omega = t} = \set {\omega \in \Omega : \map T \omega \le t} \setminus \set {\omega \in \Omega : \map T \omega \le t - 1}$
with:
:$\set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
and:
:$\set {\omega \in \Omega : \map T \omega \le t - 1} \in \FF_{t - 1}$
Since $\sequence {\FF_n}_{n \ge 0}$ is a filtration, we have:
:$\FF_{t - 1} \subseteq \FF_t$
and so:
:$\set {\omega \in \Omega : \map T \omega \le t - 1} \in \FF_t$
So from Sigma-Algebra Closed under Set Difference, we have:
:$\set {\omega \in \Omega : \map T \omega = t} \in \FF_t$ 
{{qed|lemma}}
Theorem: Pointwise Minimum of Stopping Times is Stopping Time

Let $\struct {\Omega, \Sigma, \sequence {\FF_n}_{n \ge 0}, \Pr}$ be a filtered probability space.
Let $T$ and $S$ be stopping times with respect to $\sequence {\FF_n}_{n \ge 0}$.
Let $S \wedge T$ be the pointwise minimum of $S$ and $T$.
Then $S \wedge T$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.

Proof:
We have, for $t \in \Z_{\ge 0}$ and $\omega \in \Omega$: 
:$\map {\paren {S \wedge T} } \omega \le t$ {{iff}} $\map S \omega \le t$ or $\map T \omega \le t$
That is: 
:$\set {\omega \in \Omega : \map {\paren {S \wedge T} } \omega \le t} = \set {\omega \in \Omega : \map S \omega \le t} \cup \set {\omega \in \Omega : \map T \omega \le t}$ 
Since $S$ and $T$ are stopping times with respect to $\sequence {\FF_n}_{n \ge 0}$, we have:
:$\set {\omega \in \Omega : \map S \omega \le t} \in \FF_t$
and:
:$\set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
So, since $\FF_t$ is closed under finite union, we have: 
:$\set {\omega \in \Omega : \map {\paren {S \wedge T} } \omega \le t} \in \FF_t$
{{qed}}
Category:Stopping Times
neck5sfvzdpgkmpw3jjf1y9metdzkiw
Theorem: Constant Function is Stopping Time

Let $\struct {\Omega, \Sigma, \sequence {\FF_n}_{n \ge 0}, \Pr}$ be a filtered probability space.
Let $T_\ast$ be an extended natural number.
Define $T : \Omega \to \Z_{\ge 0} \cup \set \infty$ by: 
:$\map T \omega = T_\ast$ 
for each $\omega \in \Omega$.
Then $T$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.

Proof:
First, if $T_\ast = \infty$, we have: 
:$\set {\omega \in \Omega : \map T \omega \le t} = \O$
for all $t \in \Z_{\ge 0}$.
Since each $\FF_t$ is a $\sigma$-algebra we therefore have: 
:$\set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
for all $t \in \Z_{\ge 0}$ in the case $T_\ast = \infty$. 
Now let $T_\ast < \infty$.
For $t < T_\ast$, we have: 
:$\set {\omega \in \Omega : \map T \omega \le t} = \O$
and so:
:$\set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
for all $t \in \Z_{\ge 0}$ again. 
For $t \ge T_\ast$, we have:
:$\set {\omega \in \Omega : \map T \omega \le t} = \Omega$
Since each $\FF_t$ is a $\sigma$-algebra we therefore have: 
:$\set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
for all $t \in \Z_{\ge 0}$.
So $T$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.
{{qed}}
Category:Stopping Times
o1haqxexlq78324rxppcrn2rtha4egz
Theorem: Pointwise Infimum of Stopping Times is Stopping Time

Let $\struct {\Omega, \Sigma, \sequence {\FF_n}_{n \ge 0}, \Pr}$ be a filtered probability space.
Let $\sequence {T_n}_{n \in \N}$ be a sequence of stopping times with respect to $\sequence {\FF_n}_{n \ge 0}$.
Let:
:$\ds T = \inf_{n \in \N} T_n$
be the pointwise infimum of the $\sequence {T_n}_{n \in \N}$.
Then $T$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.

Proof:
We have, for $t \in \Z_{\ge 0}$ and $\omega \in \Omega$: 
:$\map T \omega \le t$ {{iff}} $\map {T_n} \omega \le t$ for some $n \in \N$.
That is: 
:$\ds \set {\omega \in \Omega : \map T \omega \le t} = \bigcup_{n \in \N} \set {\omega \in \Omega : \map {T_n} \omega \le t}$
for each $t \in \Z_{\ge 0}$.
Now fix $t \in \Z_{\ge 0}$. 
Since each $T_n$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$, we have: 
:$\set {\omega \in \Omega : \map {T_n} \omega \le t} \in \FF_t$
for each $n \in \N$.
Then, since $\FF_t$ is a $\sigma$-algebra and $\sigma$-algebras are closed under countable union, we have: 
:$\ds \set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
So $T$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.
{{qed}}
Category:Stopping Times
tawex92yc5gtgejcpka4agt6qie3f2r
Theorem: Sum of Stopping Times is Stopping Time

Let $\struct {\Omega, \Sigma, \sequence {\FF_n}_{n \ge 0}, \Pr}$ be a filtered probability space.
Let $T$ and $S$ be stopping times with respect to $\sequence {\FF_n}_{n \ge 0}$.
Then the pointwise sum $T + S$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.

Proof:
Let $t \in \Z_{\ge 0}$. 
Then, if for $\omega \in \Omega$ we have $\map T \omega + \map S \omega = t$, we have: 
:$\map T \omega \le t$
and:
:$\map S \omega \le t$ 
If we have: 
:$\map S \omega = s \le t$ 
and:
:$\map S \omega + \map T \omega = t$ 
we have: 
:$\map T \omega = t - s$
So, we have: 
:$\ds \set {\omega \in \Omega : \map S \omega + \map T \omega \le t} = \bigcup_{s \in \Z_{\ge 0}, \, 0 \le s \le t} \set {\omega \in \Omega : \map S \omega = s} \cap \set {\omega \in \Omega : \map T \omega = t - s}$
Since $S$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$ we have:
:$\set {\omega \in \Omega : \map S \omega = s} \in \FF_s$
Since $s \le t$ and $\sequence {\FF_n}_{n \ge 0}$ is a filtration, we have: 
:$\FF_s \subseteq \FF_t$
and so:
:$\set {\omega \in \Omega : \map S \omega = s} \in \FF_t$
Similarly, we have:
:$\set {\omega \in \Omega : \map T \omega = t - s} \in \FF_{t - s}$
and so:
:$\set {\omega \in \Omega : \map T \omega = t - s} \in \FF_t$
Since $\FF_t$ is closed under finite union, we have: 
:$\ds \set {\omega \in \Omega : \map S \omega + \map T \omega \le t} \in \FF_t$
So $S + T$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.
{{qed}}
Category:Stopping Times
847mevs27iqv1l1zryth0lp516594hl
Theorem: Shift of Stopping Time is Stopping Time

Let $\struct {\Omega, \Sigma, \sequence {\FF_n}_{n \mathop \ge 0}, \Pr}$ be a filtered probability space.
Let $T$ be a stopping time {{WRT}} $\sequence {\FF_n}_{n \mathop \ge 0}$.
Let $t$ be a extended natural number.
Then $T + t$ is a stopping time {{WRT}} $\sequence {\FF_n}_{n \mathop \ge 0}$.

Proof:
By Constant Function is Stopping Time, $t$ is a stopping time {{WRT}} $\sequence {\FF_n}_{n \mathop \ge 0}$.
By Sum of Stopping Times is Stopping Time, $T + t$ is a stopping time {{WRT}} $\sequence {\FF_n}_{n \mathop \ge 0}$.
{{qed}}
Category:Stopping Times
1z3amfn8zilqrdlwhf6uhp4xj1pap34
Theorem: Stopped Sigma-Algebra preserves Inequality between Stopping Times

Let $\struct {\Omega, \Sigma, \sequence {\FF_n}_{n \ge 0}, \Pr}$ be a filtered probability space.
Let $T$ and $S$ be stopping times with respect to $\sequence {\FF_n}_{n \ge 0}$ such that: 
:$\map S \omega \le \map T \omega$
for each $\omega \in \Omega$.
Let $\FF_S$ and $\FF_T$ be the stopped $\sigma$-algebras associated with $S$ and $T$ respectively.
Then:
:$\FF_S \subseteq \FF_T$

Proof:
Let $A \in \FF_S$ and $t \in \Z_{\ge 0}$.
If $\omega \in \Omega$ is such that: 
:$\map T \omega \le t$
we have:
:$\map S \omega \le t$ 
So:
:$\set {\omega \in \Omega : \map T \omega \le t} \subseteq \set {\omega \in \Omega : \map S \omega \le t}$ 
for each $t \in \Z_{\ge 0}$.
So, from Intersection with Subset is Subset, we have:
:$\set {\omega \in \Omega : \map T \omega \le t} \cap \set {\omega \in \Omega : \map S \omega \le t} = \set {\omega \in \Omega : \map T \omega \le t}$
So, we have from Intersection is Associative:
:$A \cap \set {\omega \in \Omega : \map T \omega \le t} = \paren {A \cap \set {\omega \in \Omega : \map S \omega \le t} } \cap \set {\omega \in \Omega : \map T \omega \le t}$
Since $T$ is a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$ we have:
:$\set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
and since $A \in \FF_S$ we have:
:$A \cap \set {\omega \in \Omega : \map S \omega \le t} \in \FF_t$
Since $\FF_t$ is closed under finite intersection, we have:
:$A \cap \set {\omega \in \Omega : \map T \omega \le t} \in \FF_t$
for all $t \in \Z_{\ge 0}$. 
So $A \in \FF_T$, giving $\FF_S \subseteq \FF_T$.
{{qed}}