avewright/proofwiki-math huggingface dataset:
Theorem: Way Below iff Second Operand Preceding Supremum of Directed Set There Exists Element of Directed Set First Operand Way Below Element

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.
Let $x, y$ be elements of $S$.
Then
:$x \ll y$
{{iff}}
:for every directed subset $D$ of $S$ such that $y \preceq \sup D$
::there exists an element $d$ of $D$: $x \ll d$

Proof:
=== Sufficient Condition ===
Let $x \ll y$.
Let $D$ be a directed subset of $S$ such that
:$y \preceq \sup D$
By Way Below has Interpolation Property:
:$\exists x' \in S: x \ll x' \land x' \ll y$
By definition of way below relation:
:$\exists d \in D: x' \preceq d$
Thus by Preceding and Way Below implies Way Below and definition of reflexivity:
:$x \ll d$
{{qed|lemma}}
Theorem: Continuous iff Way Below Closure is Ideal and Element Precedes Supremum

Let $L = \struct {S, \wedge, \preceq}$ be an up-complete meet semilattice.
Then
:$L$ is continuous
{{iff}}
:$\forall x \in S: x^\ll$ is an ideal in $L$ and $x \preceq \map \sup {x^\ll}$ and:
::for every ideal $I$ in $L$: $x \preceq \sup I \implies x^\ll \subseteq I$
where $x^\ll$ denotes the way below closure of $x$.

Proof:
=== Sufficient Condition ===
Let $L$ be continuous.
Let $x \in S$.
By definition of continuous:
:$x^\ll$ is directed.
By Way Below Closure is Lower Section:
:$x^\ll$ is a lower section.
Thus by definition:
:$x^\ll$ is an ideal in $L$.
By definition of continuous:
:$L$ satisfies the axiom of approximation.
By the axiom of approximation:
:$x = \map \sup {x^\ll}$
Thus by definition of reflexivity:
:$x \preceq \map \sup {x^\ll}$
Let $I$ be an ideal in $L$ such that
:$x \preceq \sup I$
We will prove that
:$x^\ll \subseteq I$
Let $y \in x^\ll$
By definition of way below closure:
:$y \ll x$
Thus by Way Below iff Second Operand Preceding Supremum of Ideal implies First Operand is Element of Ideal:
:$y \in I$
{{qed|lemma}}
Theorem: Characterization of Euclidean Borel Sigma-Algebra/Open equals Closed

Let $\OO^n$ and $\CC^n$ be the collections of open and closed subsets of the Euclidean space $\struct {\R^n, \tau}$, respectively.
Then:
:$\map \sigma {\OO^n} = \map \sigma {\CC^n}$
where $\sigma$ denotes generated $\sigma$-algebra.

Proof:
Recall that a closed set is by definition the relative complement of an open set.
Hence Sigma-Algebra Generated by Complements of Generators applies to yield:
:$\map \sigma {\OO^n} = \map \sigma {\CC^n}$
{{qed}}
Theorem: Characterization of Euclidean Borel Sigma-Algebra/Closed equals Compact

Let $\CC^n$ and $\KK^n$ be the collections of closed and compact subsets of the Euclidean space $\struct {\R^n, \tau}$, respectively.
Then:
:$\map \sigma {\CC^n} = \map \sigma {\KK^n}$
where $\sigma$ denotes generated $\sigma$-algebra.

Proof:
By the Heine-Borel Theorem:
:$\KK^n \subseteq \CC^n$.
Thus from Generated Sigma-Algebra Preserves Subset:
:$\map \sigma {\KK^n} \subseteq \map \sigma {\CC^n}$.
Next, let $\map {B_n^-} {\mathbf 0}$ be the closed ball of radius $n$ around $\mathbf 0$ in $\R^n$ for all $n \in \N$.
Observe that:
:$\R^n = \ds \bigcup_{n \mathop \in \N} \map {B_n^-} {\mathbf 0}$.
Now let $U \in \CC^n$ be a closed subset of $\R^n$.
Then from Intersection with Subset is Subset and Intersection Distributes over Union:
:$\ds U = U \cap \R^n = U \cap \bigcup_{n \mathop \in \N} \map {B_n^-} {\mathbf 0} = \bigcup_{n \mathop \in \N} \paren {U \cap \map {B_n^-} {\mathbf 0} }$
From Intersection of Closed Sets is Closed in Topological Space, $U \cap \map {B_n^-} {\mathbf 0}$ is closed for all $n \in \N$.
By definition, $\map {B_n^-} {\mathbf 0}$ is bounded.
Thus, by the Heine-Borel Theorem, $U \cap \map {B_n^-} {\mathbf 0}$ is compact.
Thus, any closed set is the countable union of compact sets.
By the third axiom for a $\sigma$-algebra, this means that:
:$\CC^n \subseteq \map \sigma {\KK^n}$
Now the definition of generated $\sigma$-algebra ensures that:
:$\map \sigma {\CC^n} \subseteq \map \sigma {\KK^n}$
Hence the result, by definition of set equality.
{{qed}}
Theorem: Characterization of Euclidean Borel Sigma-Algebra/Open equals Rectangle

Let $\OO^n$ be the collection of open subsets of the Euclidean space $\struct {\R^n, \tau}$.
Let $\JJ_{ho}^n$ be the collection of half-open rectangles in $\R^n$.
Then:
:$\map \sigma {\OO^n} = \map \sigma {\JJ_{ho}^n}$
where $\sigma$ denotes generated $\sigma$-algebra.

Proof:
Let $\horectr {\mathbf a} {\mathbf b} \in \JJ^n_{ho}$.
Then:
:$\horectr {\mathbf a} {\mathbf b} = \paren {\openint \gets {\mathbf b} } \cap \horectr {\mathbf a} \to$
provides a way of writing this half-open $n$-rectangle as an intersection of an open and a closed set.
By Characterization of Euclidean Borel Sigma-Algebra/Open equals Closed, these are both in $\map \BB {\R^n}$, and so Sigma-Algebra Closed under Intersection yields:
:$\horectr {\mathbf a} {\mathbf b} \in \map \sigma {\OO^n}$
Hence, by definition of generated $\sigma$-algebra:
:$\map \sigma {\JJ^n_{ho} } \subseteq \map \sigma {\OO^n}$
Denote $\mathbf 1 = \tuple {1, \ldots, 1} \in \R^n$.
Define, for all $k \in \N$, $\map \SS k$ by:
:$\map \SS k := \set {\horectr {2^{-k} \mathbf j} {2^{-k} \paren {\mathbf j + \mathbf 1} } : \mathbf j \in \Z^n}$
It is immediate that $\ds \bigcup \map \SS k = \R^n$ and $\map \SS k \subseteq \JJ^n_{ho}$.
Also, $\map \SS k$ is countable from Cartesian Product of Countable Sets is Countable.
Now define, again for all $k \in \N$, $U_k$ by:
:$\ds U_k := \bigcup \set {S \in \map \SS k: S \subseteq U}$
From Set Union Preserves Subsets:
:$U_k \subseteq U$
Also, $U_k \in \map \sigma {\JJ^n_{ho} }$ since the union is countable.
It follows that also $\ds \bigcup_{k \mathop \in \N} U_k \in \map \sigma {\JJ^n_{ho} }$.
Next, it is to be shown that $\ds \bigcup_{k \mathop \in \N} U_k = U$.
Note that Set Union Preserves Subsets ensures $\ds \bigcup_{k \mathop \in \N} U_k \subseteq U$.
For the converse, let $\mathbf x \in U$.
As $U$ is open, there exists an $\epsilon > 0$ such that the open ball $\map {B_\epsilon} {\mathbf x}$ is contained in $U$.
Fix $k \in \N$ such that $\sqrt n \, 2^{-k} < \epsilon$, and find $\mathbf j \in \Z^n$ such that:
:$\mathbf x \in \horectr {2^{-k} \mathbf j} {2^{-k} \paren {\mathbf j + \mathbf 1} }$
Now it is to be shown that:
:$\horectr {2^{-k} \mathbf j} {2^{-k} \paren {\mathbf j + \mathbf 1} } \subseteq \map {B_\epsilon} {\mathbf x}$
To this end, observe that for any $\mathbf y \in \horectr {2^{-k} \mathbf j} {2^{-k} \paren {\mathbf j + \mathbf 1} }$, it holds that:
:$\map d {\mathbf x, \mathbf y} \le \map \diam {\horectr {2^{-k} \mathbf j} {2^{-k} \paren {\mathbf j + \mathbf 1} } }$
by definition of diameter.
Now from Diameter of Rectangle, the {{RHS}} equals:
:$\norm {2^{-k} \paren {\mathbf j + \mathbf 1} - 2^{-k} \mathbf j} = \norm {2^{-k} \mathbf 1} = \sqrt n \, 2^{-k}$
which is smaller than $\epsilon$ by the way $k$ was chosen.
Hence:
:$\horectr {2^{-k} \mathbf j} {2^{-k} \paren {\mathbf j + \mathbf 1} } \subseteq \map {B_\epsilon} {\mathbf x}$
and so every $\mathbf x \in U$ is contained in some $U_k$.
Thus it follows that $U \subseteq \ds \bigcup_{k \mathop \in \N} U_k$.
Thereby we have shown that:
:$\map \sigma {\JJ^n_{ho} } = \map \sigma {\OO^n}$
{{qed}}
Theorem: Rising Factorial as Factorial by Binomial Coefficient

Let $x \in \R$ be a real number.
Let $n \in \Z_{\ge 0}$ be a positive integer.
:$x^{\overline n} = n! \dbinom {x + n - 1} n$
where:
:$x^{\overline n}$ denotes $x$ to the $n$ rising
:$n!$ denotes the factorial of $n$
:$\dbinom {x + n - 1} n$ denotes a binomial coefficient.

Proof:
By definition of $x$ to the $n$ rising:
:$x^{\overline n} = x \paren {x + 1} \cdots \paren {x + n - 1}$
By definition of the binomial coefficient of a real number:
:$\dbinom {x + n - 1} n = \dfrac {\paren {x + n - 1} \paren {x + n - 2} \cdots x} {n!}$
Hence the result.
{{qed}}
Category:Binomial Coefficients
Category:Factorials
Category:Rising Factorials
dvzltdgyaaatcwxni3r2jeitw1e8x0t
Theorem: Ramus's Identity

Let $k, m, n \in \Z_{\ge 0}$ be positive integers such that $0 \le k < m$.
Then:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop \ge 0} \binom n {j m + k}
      | r = \dbinom n k + \dbinom n {m + k} +  \dbinom n {2 m + k} + \cdots 
      | c = 
}}
{{eqn | r = \dfrac 1 m \sum_{0 \mathop \le j \mathop < m} \paren {2 \cos \dfrac {j \pi} m}^n \cos \dfrac {j \paren {n - 2 k} \pi} m
      | c = 
}}
{{end-eqn}}

Proof:
Let $\omega := e^{2 \pi i / m}$.
Then by the Binomial Theorem:
:$(1): \quad \ds \sum_{0 \mathop \le j \mathop < m} \paren {1 + \omega^j}^n \omega^{-j k} = \sum_t \sum_{0 \mathop \le j \mathop < m} \binom n t \omega^{j \paren {t - k} }$
By Sum of Geometric Sequence:
:$\ds \sum_{0 \mathop \ge j \mathop < m} \omega^{j \paren {t - k} } = \begin{cases} \dfrac {1 - \omega^{m \paren {t - k} } } {1 - \omega^{t - k} } & : t - k \not \equiv 0 \pmod m \\ m & : t \equiv k \pmod m \end{cases}$
We have that:
:$\omega = \exp \dfrac {2 \pi i} m \implies \omega^m = 1$
and so:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le j \mathop < m} \omega^{r j}
      | r = \frac {1 - \omega^{r m} } {1 - \omega^r}
      | c = Sum of Geometric Sequence
}}
{{eqn | r = m \sqbrk {r \equiv 0 \pmod m}
      | c = where $\sqbrk {\, \cdots \,}$ is Iverson's convention
}}
{{end-eqn}}
Thus the summation on the {{RHS}} of $(1)$ is:
:$m \ds \sum_{t \bmod m \mathop = k} \binom n t$
The summation on the {{LHS}} of $(1)$ is:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le j \mathop < m} \paren {1 + \omega^j}^n \omega^{-j k}
      | r = \sum_{0 \mathop \le j \mathop < m} \paren {\omega^{-j / 2} + \omega^{j / 2} }^n \omega^{j \paren {n / 2} - k}
      | c = 
}}
{{eqn | r = \sum_{0 \mathop \le j \mathop < m} \paren {2 \cos \dfrac {j \pi} m}^n \omega^{j \paren {n / 2} - k}
      | c = 
}}
{{end-eqn}}
Because the {{RHS}} is wholly real, so must the {{LHS}} be.
So, taking the real parts of the {{LHS}} and equating it to the {{RHS}} reveals the result.
{{qed}}
Theorem: Summation over Lower Index of Unsigned Stirling Numbers of the First Kind

Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\ds \sum_k {n \brack k} = n!$
where:
:$\ds {n \brack k}$ denotes an unsigned Stirling number of the first kind
:$n!$ denotes the factorial of $n$.

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P N$ be the proposition:
:$\ds \sum_k {n \brack k} = n!$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \sum_k {0 \brack k}
      | r = \sum_k \delta_{0 k}
      | c = Unsigned Stirling Number of the First Kind of 0
}}
{{eqn | r = 1
      | c = all terms vanish but for $k = 0$
}}
{{eqn | r = 0!
      | c = {{Defof|Factorial}}
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
Theorem: Summation over Lower Index of Unsigned Stirling Numbers of the First Kind with Alternating Signs

Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\ds \sum_k \paren {-1}^k {n \brack k} = \delta_{n 0} - \delta_{n 1}$
where:
:$\ds {n \brack k}$ denotes an unsigned Stirling number of the first kind
:$\delta_{n 0}$ denotes the Kronecker delta.

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \sum_k \paren {-1}^k {n \brack k} = \delta_{n 0} - \delta_{n 1}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \sum_k \paren {-1}^k {0 \brack k}
      | r = \sum_k \delta_{0 k}
      | c = Unsigned Stirling Number of the First Kind of 0
}}
{{eqn | r = 1
      | c = all terms vanish but for $k = 0$
}}
{{eqn | r = \delta_{0 0} - \delta_{0 1}
      | c = {{Defof|Kronecker Delta}}
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = \sum_k \paren {-1}^k {1 \brack k}
      | r = \sum_k \paren {-1}^k \delta_{1 k}
      | c = Unsigned Stirling Number of the First Kind of 1
}}
{{eqn | r = -1
      | c = all terms vanish but for $k = 1$
}}
{{eqn | r = \delta_{1 0} - \delta_{1 1}
      | c = {{Defof|Kronecker Delta}}
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
Theorem: Beta Function of Real Number with 1

:$\map \Beta {x, 1} = \map \Beta {1, x} = \dfrac 1 x$

Proof:
By definition:
{{begin-eqn}}
{{eqn | l = \map \Beta {x, 1}
      | r = \int_0^1 t^{x - 1} \paren {1 - t}^{1 - 1} \rd t
      | c = {{Defof|Beta Function}}
}}
{{eqn | r = \int_0^1 t^{x - 1} \rd t
      | c = 
}}
{{eqn | r = \int_0^1 t^{x - 1} \rd t
      | c = 
}}
{{eqn | r = \intlimits {\frac {t^x} x} 0 1
      | c = 
}}
{{eqn | r = \frac 1 x - \frac 0 x
      | c = 
}}
{{eqn | r = \frac 1 x
      | c = 
}}
{{end-eqn}}
{{qed|lemma}}
{{begin-eqn}}
{{eqn | l = \map \Beta {1, x}
      | r = \int_0^1 t^{1 - 1} \paren {1 - t}^{x - 1} \rd t
      | c = {{Defof|Beta Function}}
}}
{{eqn | r = \int_0^1 \paren {1 - t}^{x - 1} \rd t
      | c = 
}}
{{eqn | r = \int_1^0 -\paren z^{x - 1} \rd z
      | c = Integration by Substitution
}}
{{eqn | r = -\intlimits {\frac {z^x} x} 1 0
      | c = 
}}
{{eqn | r = -\frac 0 x + \frac 1 x
      | c = 
}}
{{eqn | r = \frac 1 x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Way Below Closure is Lower Section

Let $L = \struct {S, \vee, \preceq}$ be an ordered set.
Let $x \in S$.
Then
:$x^\ll$ is a lower section.

Proof:
Let $y \in x^\ll, z \in S$ such that:
:$z \preceq y$
By definition of way below closure:
:$y \ll x$
By definition of reflexivity:
:$x \preceq x$
By Preceding and Way Below implies Way Below:
:$z \ll x$
Thus by definition of way below closure:
:$z \in x^\ll$
Thus by definition:
:$x^\ll$ is a lower section.
{{qed}}
Theorem: Continuous iff For Every Element There Exists Ideal Element Precedes Supremum

Let $L = \struct {S, \wedge, \preceq}$ be an up-complete meet semilattice.
Then
:$L$ is continuous
{{iff}}
:for every element $x$ of $S$ there exists ideal $I$ in $L$:
::$x \preceq \sup I$ and for every ideal $J$ in $L: x \preceq \sup J \implies I \subseteq J$

Proof:
=== Sufficient Condition ===
Let $L$ be continuous.
By Continuous iff Way Below Closure is Ideal and Element Precedes Supremum:
:$\forall x \in S: x^\ll$ is an ideal in $L$ and $x \preceq \map \sup {x^\ll}$ and
::for every ideal $I$ in $L$: $x \preceq \sup I \implies x^\ll \subseteq I$
where $x^\ll$ denotes the way below closure of $x$.
Thus
:for every element $x$ of $S$ there exists ideal $I$ in $L$:
::$x \preceq \sup I$ and for every ideal $J$ in $L: x \preceq \sup J \implies I \subseteq J$
{{qed|lemma}}
Theorem: Beta Function of x+1 with y plus Beta Function of x with y+1

:$\map \Beta {x + 1, y} + \map \Beta {x, y + 1} = \map \Beta {x, y}$

Proof:
By definition:
{{begin-eqn}}
{{eqn | l = \map \Beta {x + 1, y} + \map \Beta {x, y + 1}
      | r = \int_0^1 t^x \paren {1 - t}^{y - 1} \rd t + \int_0^1 t^{x - 1} \paren {1 - t}^y \rd t
      | c = {{Defof|Beta Function}}
}}
{{eqn | r = \int_0^1 \paren {t^x \paren {1 - t}^{y - 1} + t^{x - 1} \paren {1 - t}^y} \rd t
}}
{{eqn | r = \int_0^1 t^{x - 1} \paren {1 - t}^{y - 1} \paren {t + 1 - t} \rd t
}}
{{eqn | r = \int_0^1 t^{x - 1} \paren {1 - t}^{y - 1} \rd t
}}
{{eqn | r = \map \Beta {x, y}
}}
{{end-eqn}}
{{qed}}
Theorem: Beta Function of x with y+1 by x+y over y

:$\map \Beta {x, y} = \dfrac {x + y} y \map \Beta {x, y + 1}$

Proof:
By definition of Beta function:
:$\ds \map \Beta {x + 1, y} = \int_0^1 t^x \paren {1 - t}^{y - 1} \rd t$
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d t} \rd t = u v - \int v \frac {\d u} {\d t} \rd t$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = t^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d t}
      | r = x t^{x - 1}
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d t}
      | r = \paren {1 - t}^{y - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = -\frac {\paren {1 - t}^y} y
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \map \Beta {x + 1, y}
      | r = \int_0^1 t^{x - 1} \paren {1 - t}^{y - 1} \rd t
      | c = 
}}
{{eqn | r = \sqbrk {t^x \frac {-\paren {1 - t}^y} y}_0^1 - \int_0^1 x t^{x - 1} \frac {-\paren {1 - t}^y} y \rd t
      | c = Integration by Parts
}}
{{eqn | r = \frac x y \int_0^1 t^{x - 1} \paren {1 - t}^y \rd t
      | c = as the left hand term vanishes
}}
{{eqn | r = \frac x y \map \Beta {x, y + 1}
      | c = {{Defof|Beta Function}}
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \map \Beta {x, y}
      | r = \map \Beta {x + 1, y} + \map \Beta {x, y + 1}
      | c = Beta Function of x+1 with y plus Beta Function of x with y+1
}}
{{eqn | r = \frac x y \map \Beta {x, y + 1} + \map \Beta {x, y + 1}
      | c = from above
}}
{{eqn | r = \frac {x + y} y \map \Beta {x, y + 1}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Partial Gamma Function expressed as Integral

Let $m \in \Z_{\ge 1}$.
Let $\map {\Gamma_m} x$ denote the partial Gamma function, defined as:
:$\map {\Gamma_m} x := \dfrac {m^x m!} {x \paren {x + 1} \paren {x + 2} \cdots \paren {x + m} }$
Then:
:$\ds \map {\Gamma_m} x = \int_0^m \paren {1 - \frac t m}^m t^{x - 1} \rd t$
for $x > 0$.

Proof:
=== Lemma ===
First we establish:
{{:Partial Gamma Function expressed as Integral/Lemma}}
The proof continues by induction on $m$.
For all $m \in \Z_{\ge 1}$, let $\map P m$ be the proposition:
:$\ds \map {\Gamma_m} x = m^x \int_0^1 \paren {1 - t}^m t^{x - 1} \rd t$
Theorem: Partial Gamma Function expressed as Integral/Lemma

:$(1): \quad \ds \int_0^m \paren {1 - \frac t m}^m t^{x - 1} \rd t = m^x \int_0^1 \paren {1 - t}^m t^{x - 1} \rd t$
for $x > 0$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = z
      | r = \frac t m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d t} {\d z}
      | r = m
      | c = 
}}
{{end-eqn}}
Recalculating the limits:
{{begin-eqn}}
{{eqn | l = t
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z
      | r = 0
      | c = 
}}
{{eqn | l = t
      | r = m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z
      | r = 1
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \paren {1 - \frac t m}^m
      | r = \paren {1 - z}^m
      | c = 
}}
{{eqn | l = t^{x - 1}
      | r = \paren {m z}^{x - 1}
      | c = 
}}
{{eqn | r = m^{x - 1} z^{x - 1}
      | c = 
}}
{{end-eqn}}
Thus $(1)$ can be written:
{{begin-eqn}}
{{eqn | l = \int_0^m \paren {1 - \frac t m}^m t^{x - 1} \rd t
      | r = m^x \int_0^1 \paren {1 - z}^m z^{x - 1} \rd z
      | c = Integration by Substitution
}}
{{eqn | r = m^x \int_0^1 \paren {1 - t}^m t^{x - 1} \rd t
      | c = changing the name of the dummy variable
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Composite Function/Second Derivative

:${D_x}^2 w = {D_u}^2 w \paren { {D_x}^1 u}^2 + {D_u}^1 w {D_x}^2 u$

Proof:
For ease of understanding, let Leibniz's notation be used:
:$\dfrac {\d^k u} {\d x^k} := {D_x}^k u$
Then we have:
{{begin-eqn}}
{{eqn | l = {D_x}^2 w
      | r = \map {\dfrac \d {\d x} } {\dfrac {\d w} {\d x} }
      | c = 
}}
{{eqn | r = \map {\dfrac \d {\d x} } {\dfrac {\d w} {\d u} \dfrac {\d u} {\d x} }
      | c = Derivative of Composite Function
}}
{{eqn | r = \dfrac {\d u} {\d x} \map {\dfrac {\d} {\d x} } {\dfrac {\d w} {\d u} } + \dfrac {\d w} {\d u} \dfrac {\d^2 u} {\d x^2}
      | c = Product Rule for Derivatives
}}
{{eqn | r = \dfrac {\d u} {\d x} \map {\dfrac {\d} {\d u} } {\dfrac {\d w} {\d u} } \dfrac {\d u} {\d x} + \dfrac {\d w} {\d u} \dfrac {\d^2 u} {\d x^2}
      | c = Derivative of Composite Function
}}
{{eqn | r = \map {\dfrac {\d^2 w} {\d u^2} } {\dfrac {\d u} {\d x} }^2 + \dfrac {\d w} {\d u} \dfrac {\d^2 u} {\d x^2}
      | c = 
}}
{{eqn | r = {D_u}^2 w \paren { {D_x}^1 u}^2 + {D_u}^1 w {D_x}^2 u
      | c = {{Defof|Leibniz's Notation for Derivatives}}
}}
{{end-eqn}}
{{qed}}
Theorem: Faà di Bruno's Formula

Let $D_x^k u$ denote the $k$th derivative of a function $u$ {{WRT|Differentiation}} $x$.
Then:
:$\ds D_x^n w = \sum_{j \mathop = 0}^n D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = n \\ \forall p \mathop \ge 1: k_p \mathop \ge 0} } n! \prod_{m \mathop = 1}^n \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$

Proof:
In the summation:
:$\ds \sum_{j \mathop = 0}^0 D_u^j w \sum_{\substack {\sum_{p \mathop \ge 0} k_p \mathop = j \\ \sum_{p \mathop \ge 0} p k_p \mathop = 0 \\ \forall p \ge 0: k_p \mathop \ge 0} } 0! \prod_{m \mathop = 0}^1 \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$
the only element appearing is for $j = 0$, and the continued product is vacuous.
Thus:
:$\ds \prod_{m \mathop = 0}^1 \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} } = 1$
and we are left with:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^0 D_u^j w
      | r = D_u^0 w
      | c = 
}}
{{eqn | r = w
      | c = {{Defof|Zeroth Derivative}}
}}
{{end-eqn}}
{{qed}}
Theorem: Faà di Bruno's Formula

Let $D_x^k u$ denote the $k$th derivative of a function $u$ {{WRT|Differentiation}} $x$.
Then:
:$\ds D_x^n w = \sum_{j \mathop = 0}^n D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = n \\ \forall p \mathop \ge 1: k_p \mathop \ge 0} } n! \prod_{m \mathop = 1}^n \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$

Proof:
In the summation:
:$\ds \sum_{j \mathop = 0}^1 D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = 1 \\ \forall p \ge 1: k_p \mathop \ge 0} } 1! \prod_{m \mathop = 1}^1 \dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} }$
we need to consider $j = 0$ and $j = 1$.
Let $j = 0$.
Consider the set of $k_p$ such that:
:$k_1 + k_2 + \cdots = 0$
:$1 \times k_1 + 2 k_2 + \cdots = 1$
:$k_1, k_2, \ldots \ge 0$
It is apparent by inspection that no set of $k_p$ can fulfil these conditions.
Therefore when $j = 0$ the summation is vacuous
Let $j = 1$.
Consider the set of $k_p$ such that:
:$k_1 + k_2 + \cdots = 1$
:$1 \times k_1 + 2 k_2 + \cdots = 1$
:$k_1, k_2, \ldots \ge 0$
By inspection, it is seen that these can be satisfied only by:
:$k_1 = 1$
and all other $k_p = 0$.
When $k_m = 0$:
:$\dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} } = 1$
by definition of zeroth derivative and factorial of $0$.
Thus any contribution to the summation where $k_m = 0$ can be disregarded.
Thus we have:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{j \mathop = 0}^1 \sum_{\substack {k_1 \mathop = j \\ k_1 \mathop = 1 \\ k_1 \mathop \ge 0} } D_u^j w \dfrac {1!} {k_1! \paren {1!}^{k_1} } \paren {D_x^1 u}^{k_1}
      | c = 
}}
{{eqn | r = \sum_{k_1 \mathop = 1} D_u^1 w \dfrac {1!} {k_1! \paren {1!}^{k_1} } \paren {D_x^1 u}^{k_1}
      | c = simplifying: $j = 0$ is vacuous
}}
{{eqn | r = D_u w D_x u
      | c = 
}}
{{end-eqn}}
{{qed}}