avewright/proofwiki-math huggingface dataset:
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}^2 D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = 2 \\ \forall p \ge 1: k_p \mathop \ge 0} } 2! \prod_{m \mathop = 1}^2 \dfrac {\left({D_x^m u}\right)^{k_m} } {k_m! \paren {m!}^{k_m} }$
we need to consider $j = 0, j = 1$ and $j = 2$.
Note that 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.
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 = 2$
:$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 = 2$
:$k_1, k_2, \ldots \ge 0$
By inspection, it is seen that these can be satisfied only by:
:$k_2 = 1$
and all other $k_p = 0$.
Let $j = 2$.
Consider the set of $k_p$ such that:
:$k_1 + k_2 + \cdots = 2$
:$1 \times k_1 + 2 k_2 + \cdots = 2$
:$k_1, k_2, \ldots \ge 0$
By inspection, it is seen that these can be satisfied only by:
:$k_1 = 2$
and all other $k_p = 0$.
Thus we have:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{j \mathop = 0}^2 D_u^j w \sum_{\substack {k_1 \mathop + k_2 \mathop = j \\ k_1 \mathop + 2 k_2 \mathop = 2 \\ k_1, k_2 \mathop \ge 0} } 2! \dfrac {\paren {D_x^1 u}^{k_1} \paren {D_x^2 u}^{k_2} } {k_1! \paren {1!}^{k_1} k_2! \paren {2!}^{k_2} } 
      | c = 
}}
{{eqn | r = D_u^1 w \dfrac {2! \paren {D_x^1 u}^0 \paren {D_x^2 u}^1} {0! \paren {1!}^0 1! 2^1} + D_u^2 w \dfrac {2! \paren {D_x^1 u}^2 \paren {D_x^2 u}^0} {2! \paren {1!}^2 0! \paren {2!}^0} 
      | c = substituting for $k_1$ and $k_2$ for each case
}}
{{eqn | r = D_u^1 w \paren {D_x^2 u} + D_u^2 w \paren {D_x^1 u}^2
      | c = simplifying
}}
{{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:
We have that:
:$\dfrac {D_x^k u} {k!}$ is the coefficient of $z^k$ in $\map u {x + z}$
:$\dfrac {D_u^j w} {j!}$ is the coefficient of $y^j$ in $\map w {u + y}$.
Hence the coefficient of $z^n$ in $\map w {\map u {x + z} }$ is:
:$\dfrac {D_x^n w} {n!} = \ds \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} } \dfrac {j!} {k_1! \, k_2! \cdots k_n!} \paren {\dfrac {D_x^1 u} {1!} }^{k_1} \paren {\dfrac {D_x^2 u} {2!} }^{k_2} \cdots \paren {\dfrac {D_x^n u} {n!} }^{k_n}$
{{finish|plenty of details to be filled in}}
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:
$D_x^n$ can be expressed as a determinant:
:$D_x^n = \begin{vmatrix}
\dbinom {n - 1} 0 u_1 & \dbinom {n - 1} 1 u_2 & \dbinom {n - 1} 2 u_3 & \cdots & \dbinom {n - 1} {n - 2} u_{n - 1} & \dbinom {n - 1} {n - 1} u_n       \\
                   -1 & \dbinom {n - 2} 0 u_1 & \dbinom {n - 2} 1 u_2 & \cdots & \dbinom {n - 2} {n - 3} u_{n - 2} & \dbinom {n - 2} {n - 2} u_{n - 1} \\
                    0 &                    -1 & \dbinom {n - 3} 0 u_1 & \cdots & \dbinom {n - 3} {n - 4} u_{n - 3} & \dbinom {n - 3} {n - 3} u_{n - 2} \\
               \vdots &                \vdots &                \vdots & \ddots &                            \vdots &                            \vdots \\
                    0 &                     0 &                     0 & \cdots &                                -1 &                   \dbinom 0 0 u_1
\end{vmatrix}$
where $u_j := \paren {D_x^j u} D_u$.
Both sides of this equation are differential operators which are to be applied to $w$.
{{finish|Fill in the details}}
Theorem: Cardinality of Reduced Residue System

Let $n \ge 2$.
Let $\Z'_n$ be the reduced residue system modulo $n$.
Then:
:$\card {\Z'_n} = \map \phi n$
where $\map \phi n$ is the Euler phi function.

Proof:
Recall the definition of $\Z'_n$:
:$\Z'_n = \set {\eqclass k n \in \Z_n: k \perp n}$
and the definition of $\map \phi n$:
:$\map \phi n = \card {\set {k: 1 \le k \le n, k \perp n} }$
The result follows from Integer is Congruent to Integer less than Modulus.
{{qed}}
Theorem: Equivalence of Definitions of Norm of Linear Functional/Corollary

For all $v \in V$, the following inequality holds:
:$\size {L v} \le \norm L \norm v$
{{explain|Define $\norm L$ and $\norm v$}}

Proof:
If $v = \mathbf 0$ there is nothing to prove.
Let $v \ne \mathbf 0$.
By the definition of the supremum:
:$\dfrac {\size {L v} } {\norm v} \le \norm L_3 = \norm L$
{{explain| What is this $\norm L_3$}}
whence:
:$\size {L v} \le \norm L \norm v$
{{qed}}
Theorem: Faà di Bruno's Formula/Example/0/Proof

Consider Faà di Bruno's Formula:
{{:Faà di Bruno's Formula}}
When $n = 0$ we have:
{{:Faà di Bruno's Formula/Example/0}}

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/Example/1/Proof

Consider Faà di Bruno's Formula:
{{:Faà di Bruno's Formula}}
When $n = 1$ we have:
{{:Faà di Bruno's Formula/Example/1}}

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}}
Theorem: Faà di Bruno's Formula/Example/2/Proof

Consider Faà di Bruno's Formula:
{{:Faà di Bruno's Formula}}
When $n = 2$ we have:
{{:Faà di Bruno's Formula/Example/2}}

Proof:
In the summation:
:$\ds \sum_{j \mathop = 0}^2 D_u^j w \sum_{\substack {\sum_{p \mathop \ge 1} k_p \mathop = j \\ \sum_{p \mathop \ge 1} p k_p \mathop = 2 \\ \forall p \ge 1: k_p \mathop \ge 0} } 2! \prod_{m \mathop = 1}^2 \dfrac {\left({D_x^m u}\right)^{k_m} } {k_m! \paren {m!}^{k_m} }$
we need to consider $j = 0, j = 1$ and $j = 2$.
Note that 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.
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 = 2$
:$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 = 2$
:$k_1, k_2, \ldots \ge 0$
By inspection, it is seen that these can be satisfied only by:
:$k_2 = 1$
and all other $k_p = 0$.
Let $j = 2$.
Consider the set of $k_p$ such that:
:$k_1 + k_2 + \cdots = 2$
:$1 \times k_1 + 2 k_2 + \cdots = 2$
:$k_1, k_2, \ldots \ge 0$
By inspection, it is seen that these can be satisfied only by:
:$k_1 = 2$
and all other $k_p = 0$.
Thus we have:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{j \mathop = 0}^2 D_u^j w \sum_{\substack {k_1 \mathop + k_2 \mathop = j \\ k_1 \mathop + 2 k_2 \mathop = 2 \\ k_1, k_2 \mathop \ge 0} } 2! \dfrac {\paren {D_x^1 u}^{k_1} \paren {D_x^2 u}^{k_2} } {k_1! \paren {1!}^{k_1} k_2! \paren {2!}^{k_2} } 
      | c = 
}}
{{eqn | r = D_u^1 w \dfrac {2! \paren {D_x^1 u}^0 \paren {D_x^2 u}^1} {0! \paren {1!}^0 1! 2^1} + D_u^2 w \dfrac {2! \paren {D_x^1 u}^2 \paren {D_x^2 u}^0} {2! \paren {1!}^2 0! \paren {2!}^0} 
      | c = substituting for $k_1$ and $k_2$ for each case
}}
{{eqn | r = D_u^1 w \paren {D_x^2 u} + D_u^2 w \paren {D_x^1 u}^2
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Faà di Bruno's Formula/Lemma 1

:$\map {D_x} {\paren {D_x^m u}^{k_m} } = k_m \paren {D_x^m u}^{k_m - 1} D_x^{m + 1} u$

Proof:
{{begin-eqn}}
{{eqn | l = \map {D_x} {\paren {D_x^m u}^{k_m} }
      | r = \paren {k_m \paren {D_x^m u}^{k_m - 1} } \map {D_x} {D_x^m u}
      | c = Derivative of Power of Function
}}
{{eqn | r = k_m \paren {\paren {D_x^m u}^{k_m - 1} } D_x^{m + 1} u
      | c = {{Defof|Higher Derivative}}
}}
{{end-eqn}}
{{qed}}
Category:Faà di Bruno's Formula
45h5bdeagyawukcj2afaz6ambszb0ol
Theorem: Faà di Bruno's Formula/Lemma 2

:$\ds \map {D_x} {\prod_{m \mathop = 1}^r \paren {\dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} } } } = \prod_{m \mathop = 1}^r \paren {\dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} } } \sum_{m \mathop = 1}^r k_m \dfrac {D_x^{m + 1} u} {D_x^m u}$

Proof:
{{begin-eqn}}
{{eqn | r = \map {D_x} {\prod_{m \mathop = 1}^r \paren {\dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} } } }
      | o = 
      | c = 
}}
{{eqn | r = \prod_{m \mathop = 1}^r \paren {\dfrac 1 {k_m! \paren {m!}^{k_m} } } \map {D_x} {\prod_{m \mathop = 1}^r \paren {\paren {D_x^m u}^{k_m} } }
      | c = 
}}
{{eqn | r = \prod_{m \mathop = 1}^r \paren {\dfrac 1 {k_m! \paren {m!}^{k_m} } } \sum_{m \mathop = 1}^r \paren {\map {D_x} {\paren {D_x^m u}^{k_m} } \prod_{s \mathop \ne m} \paren {\paren {D_x^s u}^{k_s} } }
      | c = Product Rule for Derivatives: General Result
}}
{{eqn | r = \prod_{m \mathop = 1}^r \paren {\dfrac 1 {k_m! \paren {m!}^{k_m} } } \sum_{m \mathop = 1}^r \paren {\paren {k_m \paren {D_x^m u}^{k_m - 1} D_x^{m + 1} u} \prod_{s \mathop \ne m} \paren {\paren {D_x^s u}^{k_s} } }
      | c = Faà di Bruno's Formula: Lemma 1
}}
{{eqn | r = \prod_{m \mathop = 1}^r \paren {\dfrac 1 {k_m! \paren {m!}^{k_m} } } \sum_{m \mathop = 1}^r k_m \dfrac {D_x^{m + 1} u} {D_x^m u} \prod_{m \mathop = 1}^r \paren {\paren {D_x^m u}^{k_m} }
      | c = 
}}
{{eqn | r = \prod_{m \mathop = 1}^r \paren {\dfrac {\paren {D_x^m u}^{k_m} } {k_m! \paren {m!}^{k_m} } } \sum_{m \mathop = 1}^r k_m \dfrac {D_x^{m + 1} u} {D_x^m u}
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Faà di Bruno's Formula
9kojp987m7flta4zczja8ba08d8u5yw
Theorem: Supremum of Ideals is Upper Adjoint

Let $L = \struct {S, \vee, \preceq}$ be a bounded below continuous join semilattice.
Let $\map {\mathit {Ids} } L$ be the set of all ideals in $L$.
Let $P = \struct {\map {\mathit {Ids} } L, \precsim}$ be an ordered set where $\mathord \precsim = \subseteq \restriction_{\map {\mathit {Ids} } L \times \map {\mathit {Ids} } L}$
Let $f: \map {\mathit {Ids} } L \to S$ be a mapping such that
:$\forall I \in \map {\mathit {Ids} } L: \map f I = \sup I$
Then $f$ is an upper adjoint of Galois connection.

Proof:
Define $d: S \to \map {\mathit {Ids} } L$
:$\forall t \in S: \map d t = \map \inf {f^{-1} \sqbrk {t^\succeq} }$
where
:$t^\succeq$ denotes the upper closure of $t$,
:$f^{-1} \sqbrk {t^\succeq} $ denotes the image of $t^\succeq$ over $f^{-1}$.
We will prove that
:$\forall t \in S: \map d t = \map \min {f^{-1} \sqbrk {t^\succeq} }$
Let $t \in S$.
By Continuous iff For Every Element There Exists Ideal Element Precedes Supremum:
:there exists an ideal $J$ in $L$ such that
::$t \preceq \sup J$ and for every ideal $K$ in $L$: $t \preceq \sup K \implies J \subseteq K$
We will prove that
:$\forall K \in \map {\mathit {Ids} } L: K$ is lower bound for $f^{-1} \sqbrk {t^\succeq} \implies K \precsim J$
Let $K \in \map {\mathit {Ids} } L$ such that
:$K$ is a lower bound for $f^{-1} \sqbrk {t^\succeq}$
By definition of $f$:
:$t \preceq \map f J$
By definition of upper closure of element:
:$\map f J \in t^\succeq$
By definition of image of set:
:$J \in f^{-1} \sqbrk {t^\succeq}$
Thus by definition of lower bound:
:$K \precsim J$
{{qed|lemma}}
We will prove that:
:$J$ is a lower bound for $f^{-1} \sqbrk {t^\succeq}$
Let $K \in \map {\mathit {Ids} } L$ such that:
:$K \in f^{-1} \sqbrk {t^\succeq}$
By definition of image of set:
:$\map f K \in t^\succeq$
By definition of upper closure of element:
:$t \preceq \map f K$
By definition of $f$:
:$t \preceq \sup K$
Then
:$J \subseteq K$
Thus by definition of $\precsim$:
:$J \precsim K$
{{qed|lemma}}
By definition of supremum:
:$t \preceq \map \sup {\map \inf {f^{-1} \sqbrk {t^\succeq} } }$
By definition of $f$:
:$t \preceq \map f {\map \inf {f^{-1} \sqbrk {t^\succeq} } }$
By definition of upper closure of element:
:$\map f {\map \inf {f^{-1} \sqbrk {t^\succeq} } } \in t^\succeq$
By definition of image of set:
:$\map \inf {f^{-1} \sqbrk {t^\succeq} } \in f^{-1} \sqbrk {t^\succeq}$
Thus by definition of smallest element:
:$\map d t = \map \min {f^{-1} \sqbrk {t^\succeq} }$
{{qed|lemma}}
By Supremum of Ideals is Increasing:
:$f$ is an increasing mapping.
By Galois Connection is Expressed by Minimum:
:$\struct {f, d}$ is a Galois connection.
Hence $f$ is an upper adjoint of Galois connection.
{{qed}}
Theorem: Supremum of Ideals is Increasing

Let $L = \struct {S, \preceq}$ be an up-complete ordered set.
Let $\map {\operatorname{Ids} } L$ be the set of all ideals in $L$.
Let $P = \struct {\map {\operatorname{Ids} } L, \precsim}$ be an ordered set where $\mathord \precsim = \subseteq\restriction_{\map {\operatorname{Ids} } L \times \map {\operatorname{Ids} } L}$
Let $f: \map {\operatorname{Ids} } L \to S$ be a mapping such that:
:$\forall I \in \map {\operatorname{Ids} } L: \map f I = \sup I$
Then $f$ is an increasing mapping.

Proof:
Let $I, J \in \map {\operatorname{Ids} } L$ such that
:$I \precsim J$
By definition of $\precsim$:
:$I \subseteq J$
By definition of up-complete:
:$I$ and $J$ admit suprema in $L$.
By Supremum of Subset:
:$\sup I \preceq \sup J$
Thus by definition of $f$:
:$\map f I \preceq \map f J$
Hence $f$ is an increasing mapping.
{{qed}}
Theorem: Derivative of Composite Function/Third Derivative

:${D_x}^3 w = {D_u}^3 w \paren { {D_x}^1 u}^3 + 3 {D_u}^2 w {D_x}^2 u {D_x}^1 u + {D_u}^1 w {D_x}^3 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}^3 w
      | r = \map {\dfrac \d {\d x} } {\dfrac {\d^2 w} {\d x^2} }
      | c = 
}}
{{eqn | r = \map {\dfrac \d {\d x} } {\dfrac {\d^2 w} {\d u^2} \paren {\dfrac {\d u} {\d x} }^2 + \dfrac {\d w} {\d u} \dfrac {\d^2 u} {\d x^2} }
      | c = Derivative of Composite Function: Second Derivative
}}
{{eqn | r = \map {\dfrac \d {\d x} } {\dfrac {\d^2 w} {\d u^2} } \paren {\dfrac {\d u} {\d x} }^2 + \dfrac {\d^2 w} {\d u^2} \map {\dfrac \d {\d x} } {\paren {\dfrac {\d u} {\d x} }^2}
      | c = Product Rule for Derivatives
}}
{{eqn | o = 
      | ro= +
      | r = \map {\dfrac \d {\d x} } {\dfrac {\d w} {\d u} } \dfrac {\d^2 u} {\d x^2} + \dfrac {\d w} {\d u} \map {\dfrac \d {\d x} } {\dfrac {\d^2 u} {\d x^2} }
      | c = 
}}
{{eqn | r = \dfrac {\d^3 w} {\d u^3} \dfrac {\d u} {\d x} \paren {\dfrac {\d u} {\d x} }^2 + \dfrac {\d^2 w} {\d u^2} 2 \dfrac {\d u} {\d x} \dfrac {\d^2 u} {\d x^2}
      | c = Derivative of Composite Function
}}
{{eqn | o = 
      | ro= +
      | r = \dfrac {\d^2 w} {\d u^2} \dfrac {\d u} {\d x} \dfrac {\d^2 u} {\d x^2} + \dfrac {\d w} {\d u} \paren {\dfrac {\d^3 u} {\d x^3} }
      | c = 
}}
{{eqn | r = \dfrac {\d^3 w} {\d u^3} \paren {\dfrac {\d u} {\d x} }^3 + 2 \dfrac {\d^2 w} {\d u^2} \dfrac {\d^2 u} {\d x^2} \dfrac {\d u} {\d x}
      | c = simplifying
}}
{{eqn | o = 
      | ro= +
      | r = \dfrac {\d^2 w} {\d u^2} \dfrac {\d^2 u} {\d x^2} \dfrac {\d u} {\d x} + \dfrac {\d w} {\d u} \paren {\dfrac {\d^3 u} {\d x^3} }
      | c = 
}}
{{eqn | r = \dfrac {\d^3 w} {\d u^3} \paren {\dfrac {\d u} {\d x} }^3 + 3 \dfrac {\d^2 w} {\d u^2} \dfrac {\d^2 u} {\d x^2} \dfrac {\d u} {\d x} + \dfrac {\d w} {\d u} \paren {\dfrac {\d^3 u} {\d x^3} }
      | c = simplifying
}}
{{eqn | r = D_u^3 w \paren {D_x^1 u}^3 + 3 D_u^2 w D_x^2 u D_x^1 u + D_u^1 w D_x^3 u
      | c = Leibniz's Notation
}}
{{end-eqn}}
{{qed}}
Category:Derivative of Composite Function
aun0uozw7drye8bbf8427tr8b1ufw29
Theorem: Number of Set Partitions by Number of Components

Let $S$ be a (finite) set whose cardinality is $n$.
Let $\map f {n, k}$ denote the number of different ways $S$ can be partitioned into $k$ components.
Then:
:$\ds \map f {n, k} = {n \brace k}$
where $\ds {n \brace k}$ denotes a Stirling number of the second kind.

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \map f {n, k} = {n \brace k}$
$\map P 0$ is the degenerate case:
:$\ds \map f {0, k} = \delta_{0 k} = {0 \brace k}$
That is: the empty set can be partitioned one and only one way: into $0$ subsets.
Thus $\map P 0$ is seen to hold.
The remainder of the proof considers $n \in \Z_{> 0}$.
First we note that when $k < 1$ or $k > n$:
:$\ds \map f {n, k} = 0 = {n \brace k}$
Hence, throughout, we consider only such $k$ as $1 \le k \le n$.
We define the representative set of cardinality $n$ to be:
:$S_n := \set {1, 2, \ldots, n}$
Theorem: Summation of Summation over Divisors of Function of Two Variables

Let $c, d, n \in \Z$.
Then:
:$\ds \sum_{d \mathop \divides n} \sum_{c \mathop \divides d} \map f {c, d} = \sum_{c \mathop \divides n} \sum_{d \mathop \divides \paren {n / c} } \map f {c, c d}$
where $c \divides d$ denotes that $c$ is a divisor of $d$.

Proof:
From Exchange of Order of Summation with Dependency on Both Indices:
{{:Exchange of Order of Summation with Dependency on Both Indices}}
We have that:
:$\map R d$ is the propositional function:
::$d \divides n$
:$\map S {d, c}$ is the propositional function:
::$c \divides d$
Thus $\map {R'} {d, c}$ is the propositional function:
::Both $d \divides n$ and $c \divides d$
This is the same as:
::$c \divides n$ and $\dfrac d c \divides \dfrac n c$
Similarly, $\map {S'} c$ is the propositional function:
::$\exists d$ such that both $d \divides n$ and $c \divides d$
This is the same as:
::$c \divides n$
This gives:
:$\ds \sum_{d \mathop \divides n} \sum_{c \mathop \divides d} \map f {c, d} = \sum_{c \mathop \divides n} \sum_{\paren {d / c} \mathrel \divides \paren {n / c} } \map f {c, d}$
Replacing $d / c$ with $d$:
:$\ds \sum_{d \mathop \divides n} \sum_{c \mathop \divides d} \map f {c, d} = \sum_{c \mathop \divides n} \sum_{d \mathop \divides \paren {n / c} } \map f {c, c d}$
{{qed}}
Theorem: Floor of Half of n+m plus Floor of Half of n-m+1

Let $n, m \in \Z$ be integers.
:$\floor {\dfrac {n + m} 2} + \floor {\dfrac {n - m + 1} 2} = n$
where $\floor x$ denotes the floor of $x$.

Proof:
Either $n + m$ or $n - m + 1$ is even.
Thus:
:$\dfrac {n + m} 2 \bmod 1 + \dfrac {n - m + 1} 2 \bmod 1 = \dfrac 1 2 < 1$
and so:
{{begin-eqn}}
{{eqn | l = \floor {\dfrac {n + m} 2} + \floor {\dfrac {n - m + 1} 2}
      | r = \floor {\dfrac {n + m} 2 + \dfrac {n - m + 1} 2}
      | c = Sum of Floors not greater than Floor of Sum
}}
{{eqn | r = \floor {\dfrac {n + m + n - m + 1} 2}
      | c = 
}}
{{eqn | r = \floor {n + \dfrac 1 2}
      | c = 
}}
{{eqn | r = n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Ceiling of Half of n+m plus Ceiling of Half of n-m+1

Let $n, m \in \Z$ be integers.
:$\ceiling {\dfrac {n + m} 2} + \ceiling {\dfrac {n - m + 1} 2} = n + 1$
where $\ceiling x$ denotes the ceiling of $x$.

Proof:
Either $n + m$ or $n - m + 1$ is even.
Thus either $\dfrac {n + m} 2$ or $\dfrac {n - m + 1} 2$ is an integer.
So:
{{begin-eqn}}
{{eqn | l = \ceiling {\dfrac {n + m} 2} + \ceiling {\dfrac {n - m + 1} 2}
      | r = \ceiling {\dfrac {n + m} 2 + \dfrac {n - m + 1} 2}
      | c = Sum of Ceilings not less than Ceiling of Sum
}}
{{eqn | r = \ceiling {\dfrac {n + m + n - m + 1} 2}
      | c = 
}}
{{eqn | r = \ceiling {n + \dfrac 1 2}
      | c = 
}}
{{eqn | r = n + 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Floor of Non-Integer

Let $x \in \R$ be a real number.
Let $x \notin \Z$.
Then:
:$\floor x < x$
where $\floor x$ denotes the floor of $x$.

Proof:
From Floor is between Number and One Less:
:$\floor x \le x$
From Real Number is Integer iff equals Floor:
:$x = \floor x \iff x \in \Z$
But we have $x \notin \Z$.
So:
:$\floor x \ne x$
and so:
:$\floor x < x$
{{qed}}
Theorem: Logarithm of Base

Let $b \in \R_{>0}$ such that $b \ne 1$.
Then:
:$\log_b b = 1$
where $\log_b$ denotes the logarithm to base $b$.

Proof:
Let $a \in \R_{>0}$ such that $a \ne 1$.
Then:
{{begin-eqn}}
{{eqn | l = \log_b b
      | r = \dfrac {\log_a b} {\log_a b}
      | c = Change of Base of Logarithm
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Logarithms
8p8v7a9h3w1b8jvsqgyq3scehh3d4y0