avewright/proofwiki-math huggingface dataset:
Theorem: Euler's Integral Representation of Hypergeometric Function

:$\ds \map F {a, b; c; x} = \dfrac {\map \Gamma c} {\map \Gamma b \map \Gamma {c - b} } \int_0^1 t^{b - 1} \paren {1 - t}^{c - b - 1} \paren {1 - x t}^{-a} \rd t$

Proof:
Letting $\size x < 1$ and expanding the product of $\paren {1 - x t}^{-a}$:
{{begin-eqn}}
{{eqn | l = \paren {1 - x t}^{-a}
      | r = \sum_{k \mathop = 0}^\infty \binom {-a} k \paren {-1}^k \paren {x t}^k
      | c = Extended Binomial Theorem
}}
{{eqn | ll= \leadsto
      | r = \sum_{k \mathop = 0}^\infty \paren {\binom {a + k - 1} k \paren {-1}^k} \paren {-1}^k \paren {x t}^k
      | c = Negated Upper Index of Binomial Coefficient
}}
{{eqn | ll= \leadsto
      | r = \sum_{k \mathop = 0}^\infty \binom {a + k - 1} k \paren {x t}^k
      | c = $\paren {-1}^{2 k} = 1$
}}
{{eqn | ll= \leadsto
      | r = \sum_{k \mathop = 0}^\infty \dfrac {\paren {a + k - 1}!} {k! \paren {a - 1}!} x^k t^k
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | ll= \leadsto
      | r = \sum_{k \mathop = 0}^\infty \dfrac {a^{\overline k} } {k!} x^k t^k
      | c = Rising Factorial as Quotient of Factorials
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \dfrac {\map \Gamma c} {\map \Gamma b \map \Gamma {c - b} } \int_0^1 t^{b - 1} \paren {1 - t}^{c - b - 1} \paren {1 - x t}^{-a} \rd t
      | r = \dfrac {\map \Gamma c} {\map \Gamma b \map \Gamma {c - b} } \int_0^1 t^{b - 1} \paren {1 - t}^{c - b - 1} \sum_{k \mathop = 0}^\infty \dfrac {a^{\overline k} } {k!} x^k t^k \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | r = \dfrac {\map \Gamma c} {\map \Gamma b \map \Gamma {c - b} } \sum_{k \mathop = 0}^\infty \dfrac {a^{\overline k} } {k!} x^k \int_0^1 t^{b - 1} \paren {1 - t}^{c - b - 1} t^k \rd t
      | c = 
}}
{{eqn | ll= \leadsto
      | r = \dfrac {\map \Gamma c} {\map \Gamma b \map \Gamma {c - b} } \sum_{k \mathop = 0}^\infty \dfrac {a^{\overline k} } {k!} x^k \int_0^1 t^{k + b - 1} \paren {1 - t}^{c - b - 1} \rd t
      | c = Product of Powers
}}
{{eqn | ll= \leadsto
      | r = \dfrac {\map \Gamma c} {\map \Gamma b \map \Gamma {c - b} } \sum_{k \mathop = 0}^\infty \dfrac {a^{\overline k} } {k!} x^k \dfrac {\map \Gamma {k + b} \map \Gamma {c - b} } {\map \Gamma {k + c} }
      | c = {{Defof|Beta Function}}
}}
{{eqn | ll= \leadsto
      | r = \sum_{k \mathop = 0}^\infty \dfrac {a^{\overline k} b^{\overline k} } {c^{\overline k} } \dfrac {x^k} {k!}
      | c = Rising Factorial as Quotient of Factorials and $\map \Gamma {c - b}$ cancels
}}
{{eqn | ll= \leadsto
      | r = \map F {a, b; c; x}
      | c = {{Defof|Hypergeometric Function}}
}}
{{end-eqn}}
Therefore:
:$\ds \map F {a, b; c; x} = \dfrac {\map \Gamma c} {\map \Gamma b \map \Gamma {c - b} } \int_0^1 t^{b - 1} \paren {1 - t}^{c - b - 1} \paren {1 - x t}^{-a} \rd t$
{{qed}}
Theorem: Right-Limits of Filtration of Sigma-Algebra form Filtration

Let $\struct {X, \Sigma}$ be a measurable space. 
Let $\family {\FF_t}_{t \mathop \ge 0}$ be a continuous-time filtration of $\Sigma$.
For each $t \in \hointr 0 \infty$, let $\FF_{t^+}$ be the right-limit of $\family {\FF_t}_{t \mathop \ge 0}$ at $t$.
Then $\family {\FF_{t^+} }_{t \ge 0}$ is a filtration of $\Sigma$.

Proof:
We need to show that $\FF_{t^+}$ is a sub-$\sigma$-algebra of $\Sigma$ for each $t \in \hointr 0 \infty$, and:
:$\FF_{t^+} \subseteq \FF_{q^+}$
for $t, q \in \hointr 0 \infty$ with $t \le q$.
From the definition of the right-limit, we have:
:$\ds \FF_{t^+} = \bigcap_{s \mathop > t} \FF_s$
for each $t \in \hointr 0 \infty$.
From Intersection of Sigma-Algebras, we have that $\FF_{t^+}$ is a sub-$\sigma$-algebra of $\Sigma$ for each $t \in \hointr 0 \infty$.
Let $t, q \in \hointr 0 \infty$ with $t \le q$.
Then, we have:
:$\set {s \in \R : s > q} \subseteq \set {s \in \R : s > t}$
and so from Intersection of Family is Subset of Intersection of Subset of Family:
:$\ds \bigcap_{s \mathop > t} \FF_s \subseteq \bigcap_{s \mathop > q} \FF_s$
so that:
:$\FF_{t^+} \subseteq \FF_{q^+}$
{{qed}}
Category:Filtrations of Sigma-Algebras
986tr1j8dewfnbdnyf1hjoyvragiq76
Theorem: Event of Stopping Time Equal to Infinity is Measurable in Limit of Filtration/Discrete Time

Let $\struct {X, \Sigma}$ be a measurable space. 
Let $\sequence {\FF_n}_{n \ge 0}$ be a discrete-time filtration of $\Sigma$.
Let $T$ be a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.
Let $\FF_\infty$ be the limit of the filtration $\sequence {\FF_n}_{n \ge 0}$.
Then:
:$\set {\omega \in \Omega : \map T \omega = \infty} \in \FF_\infty$

Proof:
Note that we have: 
{{begin-eqn}}
{{eqn	| l = \set {\omega \in \Omega : \map T \omega < \infty}
		| r = \set {\omega \in \Omega : \map T \omega \in \Z_{\ge 0} }
}}
{{eqn	| r = \bigcup_{t \in \Z_{\ge 0} } \set {\omega \in \Omega : \map T \omega = t}
}}
{{end-eqn}}
From the definition of a stopping time, we have:
:$\set {\omega \in \Omega : \map T \omega = t} \in \FF_t$
for each $t \in \Z_{\ge 0}$.
For each $t \in \Z_{\ge 0}$, we have:
:$\ds \FF_t \subseteq \bigcup_{s \in \Z_{\ge 0} } \FF_s$
from Set is Subset of Union, so that:
:$\FF_t \subseteq \FF_\infty$ 
from the definition of the $\sigma$-algebra generated by collection of subsets.
Then we have: 
:$\set {\omega \in \Omega : \map T \omega = t} \in \FF_\infty$
for each $t \in \Z_{\ge 0}$.
Now, since $\sigma$-algebras are closed under countable union, we have:
:$\ds \bigcup_{t \in \Z_{\ge 0} } \set {\omega \in \Omega : \map T \omega = t} \in \FF_\infty$ 
So: 
:$\set {\omega \in \Omega : \map T \omega < \infty} \in \FF_\infty$
Then since $\FF_\infty$ is closed under relative complement, we have: 
:$\set {\omega \in \Omega : \map T \omega = \infty} \in \FF_\infty$
{{qed}}
Category:Event of Stopping Time Equal to Infinity is Measurable in Limit of Filtration
icn8kt8vx8fwmlf813zvd0mgkrxp9rf
Theorem: Event of Stopping Time Equal to Infinity is Measurable in Limit of Filtration/Continuous Time

Let $\struct {X, \Sigma}$ be a measurable space. 
Let $\sequence {\FF_t}_{t \ge 0}$ be a continuous-time filtration of $\Sigma$.
Let $T$ be a stopping time with respect to $\sequence {\FF_n}_{n \ge 0}$.
Let $\FF_\infty$ be the limit of the filtration $\sequence {\FF_t}_{t \ge 0}$.
Then:
:$\set {\omega \in \Omega : \map T \omega = \infty} \in \FF_\infty$

Proof:
Note that we have $\map T \omega < \infty$ {{iff}} $\map T \omega \le N$ for some $N \in \N$. 
So, we have: 
:$\ds \set {\omega \in \Omega : \map T \omega < \infty} = \bigcup_{N \in \N} \set {\omega \in \Omega : \map T \omega \le N}$
Since $T$ is a stopping time, we have: 
:$\set {\omega \in \Omega : \map T \omega \le N} \in \FF_N$
For each $N \in \N$, we have: 
:$\ds \FF_N \subseteq \bigcup_{t \in \hointl 0 \infty} \FF_t$ 
from Set is Subset of Union, so that:
:$\FF_N \subseteq \FF_\infty$
from the definition of the $\sigma$-algebra generated by collection of subsets.
Now, since $\sigma$-algebras are closed under countable union, we have:
:$\ds \bigcup_{N \in \N} \set {\omega \in \Omega : \map T \omega \le N} \in \FF_\infty$ 
So:
:$\set {\omega \in \Omega : \map T \omega < \infty} \in \FF_\infty$
Then since $\FF_\infty$ is closed under relative complement, we have: 
:$\set {\omega \in \Omega : \map T \omega = \infty} \in \FF_\infty$
{{qed}}
Theorem: Convex Real Function is Pointwise Supremum of Affine Functions

Let $f : \R \to \R$ be a convex real function. 
Then there exists a set $\SS \subseteq \R^2$ such that: 
:$\ds \map f x = \sup_{\tuple {a, b} \in \SS} \paren {a x + b}$
for each $x \in \R$.

Proof:
Let $x \in \R$. 
We construct an affine function $\phi_x : \R \to \R$ such that: 
:$\map f y \ge \map {\phi_x} y$
and $\map {\phi_x} x = \map f x$.
We will then argue that: 
:$\map f x = \sup \set {\map {\phi_y} x : y \in \R}$
Define a function $g_x : \R \setminus \set x \to \R$ by: 
:$\map {g_x} y = \dfrac {\map f y - \map f x} {y - x}$
for each $y \in \R \setminus \set x$.
From definition 3 of a convex real function, we have that $g_x$ is increasing.
Then from Limit of Increasing Function, we have: 
:$\sup \set {\map {g_x} y : y < x} = c_x < \infty$
and from {{Corollary|Limit of Increasing Function}}: 
:$\map {g_x} y \ge c_x$
for $y > x$.
That is, for $y - x > 0$, we have: 
:$\dfrac {\map f y - \map f x} {y - x} \ge c_x$
and for $y - x < 0$, we have: 
:$\dfrac {\map f y - \map f x} {y - x} \le c_x$
So for all $x, y \in \R$ with $x \ne y$ we have:
:$\map f y - \map f x \ge c_x \paren {y - x}$
giving:
:$\map f y \ge \map f x + c_x \paren {y - x}$
Clearly this inequality also holds when $x = y$. 
Now set:
:$\map {\phi_x} y = \map f x + c_x \paren {y - x}$ 
for each $y \in \R$. 
Then we clearly have: 
:$\map {\phi_x} x = \map f x$
while: 
:$\map f x \ge \map {\phi_y} x$ 
for all $x, y \in \R$.
The latter gives that: 
:$\sup \set {\map {\phi_y} x : y \in \R} \le \map f x$
while the former assures that: 
:$\map f x \le \sup \set {\map {\phi_y} x : y \in \R}$ 
So we have: 
:$\map f x = \sup \set {\map {\phi_y} x : y \in \R}$
In particular, setting: 
:$\SS = \set {\tuple {c_y, \map f y - c_y y} : y \in \R}$
we obtain: 
:$\ds \map f x = \sup_{\tuple {a, b} \in \SS} \paren {a x + b}$
for each $x \in \R$.
{{qed}}
Category:Convex Real Functions
Category:Convex Real Function is Pointwise Supremum of Affine Functions
o913jahtg9f1uey1hfzn74emd24k7yi
Theorem: Orthogonal Set is Linearly Independent Set

Let $\struct {V, \innerprod \cdot \cdot}$ be an inner product space over a real or complex subfield $\mathbb F$.
Let $S \subseteq V$ be an orthogonal set.
Let $\mathbf 0 \notin S$, where $\mathbf 0$ denotes the zero vector of $V$.
Then $S$ is a linearly independent set.

Proof:
Let $n \in \N$.
Let $\lambda_1, \ldots, \lambda_n \in \mathbb F$, and let $u_1, \ldots, u_n \in S$ such that:
:$\ds \sum_{i \mathop= 1}^n \lambda_i u_1 = \mathbf 0$
To prove that $S$ is a linearly independent set, we must show that $\lambda_k = 0$ for all $k \in \set { 1, \ldots, n}$.
We calculate:
{{begin-eqn}}
{{eqn | l = \mathbf 0
      | r = \ds \sum_{i \mathop= 1}^n \lambda_i u_1 
}}
{{eqn | ll = \leadsto
      | l  = \innerprod {\mathbf 0}{u_k}
      | r  = \ds \innerprod {\sum_{i \mathop= 1}^n \lambda_i u_i }{u_k}
      | c  = take the inner product with $u_k$ on both sides
}}
{{eqn | ll = \leadsto
      | l  = 0
      | r  = \ds \innerprod {\sum_{i \mathop= 1}^n \lambda_i u_i }{u_k}
      | c  = Inner Product with Zero Vector
}}
{{eqn | r = \ds \sum_{i \mathop= 1}^n \lambda_i \innerprod {u_i}{u_k}
      | c = Inner Product Axiom $\text N 2$: Linearity in first argument
}}
{{eqn | r = \lambda_k \innerprod {u_k}{u_k}
      | c = as $\innerprod {u_i}{u_k} = 0$ for $i \ne k$
}}
{{end-eqn}}
As $u_k \ne \mathbf 0$ by assumption, it follows by Inner Product Axiom $\text N 3$: Non-Negative Definiteness that $\innerprod {u_k}{u_k} \ne 0$.
From Field has no Proper Zero Divisors, it follows that $0 = \lambda_k$ for all $k \in \set {1, \ldots, n}$.
{{qed}}
Theorem: Convex Real Function is Measurable

Let $f : \R \to \R$ be a convex real function.
Then $f$ is measurable.

Proof:
From Convex Real Function is Continuous, $f$ is continuous.
From Continuous Mapping is Measurable, $f$ is measurable.
{{qed}}
Theorem: Convex Real Function is Measurable

Let $f : \R \to \R$ be a convex real function.
Then $f$ is measurable.

Proof:
From Convex Real Function is Pointwise Supremum of Affine Functions: Corollary, there exists a countable set $\SS \subseteq \R^2$ such that: 
:$\ds \map f x = \sup_{\tuple {a, b} \mathop \in \SS} \paren {a x + b}$
for each $x \in \R$.
From Linear Function is Continuous, the map $x \mapsto a x + b$ is continuous for each $\tuple {a, b} \in \SS$. 
From Continuous Mapping is Measurable, the map $x \mapsto a x + b$ is measurable.
Since $\SS$ is countable, we can apply Pointwise Supremum of Measurable Functions is Measurable to obtain that $f$ is measurable.
{{qed}}
Theorem: Conditional Jensen's Inequality

Let $\struct {\Omega, \Sigma, \Pr}$ be a probability space.
Let $\GG$ be a sub-$\sigma$-algebra of $\Sigma$. 
Let $X$ be an integrable random variable.
Let $\expect {X \mid \GG}$ be a version of the conditional expectation of $X$ given $\GG$.
Let $f : \R \to \R$ be a convex function such that $\map f X$ is integrable.
Let $\expect {\map f X \mid \GG}$ be a version of the conditional expectation of $\map f X$ given $\GG$.
Then: 
:$\map f {\expect {X \mid \GG} } \le \expect {\map f X \mid \GG}$

Proof:
Note that from Convex Real Function is Measurable and Composition of Measurable Mappings is Measurable, $\map f X$ is $\Sigma$-measurable, so the hypotheses make sense. 
By Convex Real Function is Pointwise Supremum of Affine Functions: Corollary, there exists a countable set $\SS \subseteq \R^2$ such that: 
:$\ds \map f x = \sup_{\tuple {a, b} \mathop \in \SS} \paren {a x + b}$
so: 
:$\ds \map f X = \sup_{\tuple {a, b} \mathop \in \SS} \paren {a X + b}$
So for each $\tuple {a, b} \in \SS$, we have: 
:$a X + b \le \map f X$ 
From Conditional Expectation is Monotone and Conditional Expectation is Linear, we have: 
:$a \expect {X \mid \GG} + b \le \expect {\map f X \mid \GG}$ almost surely
for each $\tuple {a, b} \in \SS$. 
For each $\tuple {a, b} \in \SS$, let $A_{\tuple {a, b} }$ be the set of sample points $\omega \in \Omega$ such that this inequality fails.
Then for:
:$\ds \omega \in \Omega \setminus \bigcup_{\tuple {a, b} \mathop \in \SS} A_{\tuple {a, b} }$
we have: 
:$a \map {\expect {X \mid \GG} } \omega + b \le \map {\expect {\map f X \mid \GG} } \omega$ for all $\tuple {a, b} \in \SS$
From Null Sets Closed under Countable Union, we have: 
:$\ds \map \Pr {\bigcup_{\tuple {a, b} \mathop \in \SS} A_{\tuple {a, b} } } = 0$
So we have: 
:$a \expect {X \mid \GG} + b \le \expect {\map f X \mid \GG}$ for all $\tuple {a, b} \in \SS$ almost surely.
We therefore have: 
:$\ds \sup_{\tuple {a, b} \mathop \in \SS} \paren {a \expect {X \mid \GG} + b} \le \expect {\map f X \mid \GG}$ almost surely.
that is: 
:$\map f {\expect {X \mid \GG} } \le \expect {\map f X \mid \GG}$ almost surely.
{{qed}}
{{Namedfor|Johan Jensen|cat = Jensen}}
Theorem: Martingale Composed with Convex Function is Submartingale

Let $\struct {\Omega, \Sigma, \sequence {\FF_t}_{t \ge 0}, \Pr}$ be a continuous-time filtered probability space.
Let $\sequence {X_t}_{t \ge 0}$ be a $\sequence {\FF_t}_{t \ge 0}$-martingale.
Let $f : \R \to \R$ be a convex function such that $\map f {X_t}$ is integrable for each $t \in \hointr 0 \infty$. 
Then $\sequence {\map f {X_t} }_{t \ge 0}$ is a $\sequence {\FF_t}_{t \ge 0}$-submartingale.

Proof:
Since $\sequence {X_t}_{t \ge 0}$ is a martingale, we have: 
:$X_t$ is $\FF_t$-measurable
for each $t \in \hointr 0 \infty$. 
From Convex Real Function is Measurable and Composition of Measurable Mappings is Measurable:
:$\map f {X_t}$ is $\FF_t$-measurable
for each $t \in \hointr 0 \infty$.
So $\sequence {\map f {X_t} }_{t \ge 0}$ is $\sequence {\FF_t}_{t \ge 0}$-adapted. 
Now let $s, t \in \hointr 0 \infty$ be such that $0 \le s < t$. 
Let $\expect {\map f {X_t} \mid \FF_s}$ be a version of the conditional expectation of $\map f {X_t}$ given $\FF_s$.
We then have: 
{{begin-eqn}}
{{eqn	| l = \expect {\map f {X_t} \mid \FF_s}
		| o = \ge
		| r = \map f {\expect {X_t \mid \FF_s} }
		| c = almost surely, by Conditional Jensen's Inequality
}}
{{eqn	| r = \map f {X_s}
		| c = almost surely, {{Defof|Martingale}}
}}
{{end-eqn}}
So $\sequence {\map f {X_t} }_{t \ge 0}$ is a $\sequence {\FF_t}_{t \ge 0}$-submartingale.
{{qed}}
Theorem: Submartingale Composed with Increasing Convex Function is Submartingale

Let $\struct {\Omega, \Sigma, \sequence {\FF_t}_{t \ge 0}, \Pr}$ be a continuous-time filtered probability space.
Let $\sequence {X_t}_{t \ge 0}$ be a $\sequence {\FF_t}_{t \ge 0}$-submartingale.
Let $f : \R \to \R$ be an increasing convex function such that $\map f {X_t}$ is integrable for each $t \in \hointr 0 \infty$. 
Then $\sequence {\map f {X_t} }_{t \ge 0}$ is a $\sequence {\FF_t}_{t \ge 0}$-submartingale.

Proof:
Since $\sequence {X_t}_{t \ge 0}$ is a martingale, we have: 
:$X_t$ is $\FF_t$-measurable
for each $t \in \hointr 0 \infty$. 
From Convex Real Function is Measurable and Composition of Measurable Mappings is Measurable:
:$\map f {X_t}$ is $\FF_t$-measurable
for each $t \in \hointr 0 \infty$.
So $\sequence {\map f {X_t} }_{t \ge 0}$ is $\sequence {\FF_t}_{t \ge 0}$-adapted. 
Now let $s, t \in \hointr 0 \infty$ be such that $0 \le s < t$. 
Let $\expect {\map f {X_t} \mid \FF_s}$ be a version of the conditional expectation of $\map f {X_t}$ given $\FF_s$.
Since $\sequence {X_t}_{t \ge 0}$ is a submartingale, we have: 
:$\expect {X_t \mid \FF_s} \ge X_s$ almost surely. 
So, since $f$ is increasing, we have: 
:$\map f {\expect {X_t \mid \FF_s} } \ge \map f {X_s}$ almost surely.
We then have: 
{{begin-eqn}}
{{eqn | l = \expect {\map f {X_t} \mid \FF_s}
      | o = \ge
      | r = \map f {\expect {X_t \mid \FF_s} }
      | c = almost surely, by Conditional Jensen's Inequality
}}
{{eqn | o = \ge
      | r = \map f {X_s}
}}
{{end-eqn}}
So $\sequence {\map f {X_t} }_{t \ge 0}$ is a $\sequence {\FF_t}_{t \ge 0}$-submartingale.
{{qed}}
Theorem: Absolute Value of Martingale is Submartingale

Let $\struct {\Omega, \Sigma, \sequence {\FF_t}_{t \ge 0}, \Pr}$ be a continuous-time filtered probability space.
Let $\sequence {X_t}_{t \ge 0}$ be a $\sequence {\FF_t}_{t \ge 0}$-martingale.
Then $\sequence {\size {X_t} }_{t \ge 0}$ is a $\sequence {\FF_t}_{t \ge 0}$-submartingale.

Proof:
From Characterization of Integrable Functions:
:$\size {X_t}$ is integrable for each $t \in \hointr 0 \infty$. 
From Absolute Value Function is Convex, $x \mapsto \size x$ is a convex function.
From Martingale Composed with Convex Function is Submartingale, we have: 
:$\sequence {\size {X_t} }_{t \ge 0}$ is a $\sequence {\FF_t}_{t \ge 0}$-submartingale.
{{qed}}
Theorem: Euler's Transformation

:$\ds \map F {a, b; c; x} = \paren {1 - x}^{c - a - b} \map F {c - a, c - b; c; x}$

Proof:
First, we observe:
{{begin-eqn}}
{{eqn | l = \dfrac {\dfrac x {x - 1} } {\dfrac x {x - 1} - 1}
      | r = \dfrac {\dfrac x {x - 1} } {\dfrac x {x - 1} - 1} \times \dfrac {x - 1} {x - 1}
      | c = multiplying top and bottom by $x - 1$
}}
{{eqn | r = \dfrac x {x - \paren {x - 1} } 
      | c = 
}}
{{eqn | n = 1
      | r = x
      | c = 
}}
{{end-eqn}}
Applying Pfaff's Transformation twice, we obtain:
{{begin-eqn}}
{{eqn | l = \map F {a, b; c; x}
      | r = \paren {1 - x}^{-a} \map F {a, c - b; c; \dfrac x {x - 1} }
      | c = First application of Pfaff's Transformation
}}
{{eqn | r = \paren {1 - x}^{-a} \map F {c - b, a; c; \dfrac x {x - 1} }
      | c = symmetry in first two terms
}}
{{eqn | r = \paren {1 - x}^{-a} \paren {1 - x}^{c - b} \map F {c - b, c - a; c; \dfrac {\dfrac x {x - 1} } {\dfrac x {x - 1} - 1} }
      | c = Second application of Pfaff's Transformation 
}}
{{eqn | r = \paren {1 - x}^{-a} \paren {1 - x}^{c - b} \map F {c - a, c - b; c; x}
      | c = symmetry in first two terms and $(1)$ above
}}
{{eqn | r = \paren {1 - x}^{c - a - b} \map F {c - a, c - b; c; x}
      | c = Product of Powers
}}
{{end-eqn}}
Therefore, after two applications of Pfaff's Transformation, we have:
:$\map F {a, b; c; x} = \paren {1 - x}^{c - a - b} \map F {c - a, c - b; c; x}$
{{qed}}
Theorem: Conditional Expectation of Sum of Squared Increments of Square-Integrable Martingale

Let $\struct {\Omega, \Sigma, \sequence {\FF_t}_{t \ge 0}, \Pr}$ be a continuous-time filtered probability space.
Let $\sequence {X_t}_{t \ge 0}$ be a continuous-time martingale such that $\size {X_t}^2$ is integrable for each $t \in \hointr 0 \infty$.
Let $s, t \in \hointr 0 \infty$ be such that $0 \le s < t$. 
Let:
:$s = t_0 < t_1 < \ldots < t_n = t$
be a finite subdivision of $\closedint s t$. 
Then: 
:$\ds \expect {\sum_{i \mathop = 1}^n \paren {X_{t_i} - X_{t_{i - 1} } }^2 \mid \FF_s} = \expect {X_t^2 - X_s^2 \mid \FF_s} = \expect {\paren {X_t - X_s}^2 \mid \FF_s}$ almost surely.

Proof:
We have, for $i < j$: 
{{begin-eqn}}
{{eqn	| l = \expect {\paren {X_{t_j} - X_{t_i} }^2 \mid \FF_{t_i} }
		| r = \expect {X_{t_j}^2 - 2 X_{t_j} X_{t_i} + X_{t_i}^2 \mid \FF_{t_i} }
}}
{{eqn	| r = \expect {X_{t_j}^2 \mid \FF_{t_i} } - 2 \expect {X_{t_j} X_{t_i} \mid \FF_{t_i} } + \expect {X_{t_i}^2 \mid \FF_{t_i} }
		| c = Conditional Expectation is Linear
}}
{{end-eqn}}
Since $\sequence {X_t}_{t \ge 0}$ is a $\sequence {\FF_t}_{t \ge 0}$-martingale, we have: 
:$X_{t_i}$ is $\FF_{t_i}$-measurable
and so: 
:$2 \expect {X_{t_j} X_{t_i} \mid \FF_{t_i} } = 2 X_{t_i} \expect {X_{t_j} \mid \FF_{t_i} }$
from Rule for Extracting Random Variable from Conditional Expectation of Product.
Using the martingale property, we have: 
:$\expect {X_{t_j} \mid \FF_{t_i} } = X_{t_i}$ 
From Conditional Expectation of Measurable Random Variable, we have: 
:$\expect {X_{t_i}^2 \mid \FF_{t_i} } = X_{t_i}^2$
Putting this together we have: 
:$\expect {\paren {X_{t_j} - X_{t_i} }^2 \mid \FF_{t_i} } = \expect {X_{t_j}^2 \mid \FF_{t_i} } - 2 X_{t_i}^2 + X_{t_i}^2 = \expect {X_{t_j}^2 \mid \FF_{t_i} } - X_{t_i}^2$ 
Since $\expect {X_{t_i}^2 \mid \FF_{t_i} } = X_{t_i}^2$, we have: 
:$\expect {\paren {X_{t_j} - X_{t_i} }^2 \mid \FF_{t_i} } = \expect {X_{t_j}^2 - X_{t_i}^2 \mid \FF_{t_i} }$ 
from Conditional Expectation is Linear.
Setting $i = 0$, $j = n$, we have: 
:$\expect {X_t^2 - X_s^2 \mid \FF_s} = \expect {\paren {X_t - X_s}^2 \mid \FF_s}$
We can also compute:
{{begin-eqn}}
{{eqn	| l = \expect {\sum_{i \mathop = 1}^n \paren {X_{t_i} - X_{t_{i - 1} } }^2 \mid \FF_s}
		| r = \sum_{i \mathop = 1}^n \expect {\paren {X_{t_i} - X_{t_{i - 1} } }^2 \mid \FF_s}
		| c = Conditional Expectation is Linear
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \expect {\expect {\paren {X_{t_i} - X_{t_{i - 1} } }^2 \mid \FF_{t_{i - 1} } } \mid \FF_s}
		| c = Tower Property of Conditional Expectation
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \expect {\expect {X_{t_i}^2 - X_{t_{i - 1} }^2 \mid \FF_{t_{i - 1} } } \mid \FF_s}
		| c = by previous computation
}}
{{eqn	| r = \sum_{i \mathop = 1}^n \expect {X_{t_i}^2 - X_{t_{i - 1} }^2 \mid \FF_s}
		| c = Tower Property of Conditional Expectation
}}
{{eqn	| r = \expect {\sum_{i \mathop = 1}^n \paren {X_{t_i}^2 - X_{t_{i - 1} }^2} \mid \FF_s}
		| c = Conditional Expectation is Linear
}}
{{eqn	| r = \expect {X_{t_n}^2 - X_{t_0}^2 \mid \FF_s}
		| c = the sum telescopes
}}
{{eqn	| r = \expect {X_t^2 - X_s^2 \mid \FF_s}
}}
{{end-eqn}}
completing the proof.
{{qed}}
Theorem: Conditional Expectation of Sum of Squared Increments of Square-Integrable Martingale/Corollary

:$\ds \expect {\sum_{i \mathop = 1}^n \paren {X_{t_i} - X_{t_{i - 1} } }^2} = \expect {X_t^2 - X_s^2} = \expect {\paren {X_t - X_s}^2}$

Proof:
From Conditional Expectation of Sum of Squared Increments of Square-Integrable Martingale:
:$\ds \expect {\sum_{i \mathop = 1}^n \paren {X_{t_i} - X_{t_{i - 1} } }^2 \mid \FF_s} = \expect {X_t^2 - X_s^2 \mid \FF_s} = \expect {\paren {X_t - X_s}^2 \mid \FF_s}$ almost surely.
From Expectation of Conditional Expectation, we then obtain: 
:$\ds \expect {\sum_{i \mathop = 1}^n \paren {X_{t_i} - X_{t_{i - 1} } }^2} = \expect {X_t^2 - X_s^2} = \expect {\paren {X_t - X_s}^2}$
{{qed}}
Theorem: Expected Value of Martingale is Constant in Time/Continuous Time

Let $\struct {\Omega, \Sigma, \sequence {\FF_t}_{t \ge 0}, \Pr}$ be a continuous-time filtered probability space.
Let $\sequence {X_t}_{t \ge 0}$ be a $\sequence {\FF_t}_{t \ge 0}$-martingale.
Then: 
:$\expect {X_t} = \expect {X_0}$
for each $t \in \hointr 0 \infty$.

Proof:
From the definition of a continuous-time martingale, we have: 
:$\expect {X_t \mid \FF_0} = X_0$ almost surely
for each $t \in \hointr 0 \infty$. 
So:
:$\expect {\expect {X_t \mid \FF_0} } = \expect {X_0}$
From Expectation of Conditional Expectation, we have:
:$\expect {\expect {X_t \mid \FF_0} } = \expect {X_t}$
So we have: 
:$\expect {X_t} = \expect {X_0}$
for each $t \in \hointr 0 \infty$.
{{qed}}