avewright/proofwiki-math huggingface dataset:
Theorem: Real Logarithm is Completely Additive

Let $\log_b: \R_{>0} \to \R$ be the real logarithm to base $b$.
Then $\log_b$ is completely additive.

Proof:
From Sum of General Logarithms:
:$\log_b x + \log_b y = \log_b \left({x y}\right)$
The result follows from the definition of complete additivity.
{{qed}}
Category:Logarithms
Category:Number Theory
8wryrdf91qouep0q87julzna5febp3i
Theorem: Sum over k of r-tk Choose k by s-t(n-k) Choose n-k by r over r-tk/Proof 1/Lemma

Let this hold for $\tuple {r, s, t, n}$:
:$\ds \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s - t \paren {n - k} } {n - k} \frac r {r - t k} = \binom {r + s - t n} n$
and also for $\tuple {r, s - t, t, n - 1}$.
Then it also holds for $\tuple {r, s + 1, t, n}$.

Proof:
Evaluating the equation for $\tuple {r, s - t, t, n - 1}$:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {\paren {s - t} - t \paren {\paren {n - 1} - k} } {\paren {n - 1} - k} \frac r {r - t k}
      | r = \binom {r + \paren {s - t} - t \paren {n - 1} } {n - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s - t - t n + t + t k} {n - k - 1} \frac r {r - t k}
      | r = \binom {r + s - t - t n + 1} {n - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s - t \paren {n - k} } {n - k - 1} \frac r {r - t k}
      | r = \binom {r + s - t n} {n - 1}
      | c = 
}}
{{end-eqn}}
Adding the equation in $\tuple {r, s, t, n}$:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop \ge 0} \binom {r - t k} k \paren {\binom {s - t \paren {n - k} } {n - k - 1} + \binom {s - t \paren {n - k} } {n - k} } \frac r {r - t k}
      | r = \binom {r + s - t n} {n - 1} + \binom {r + s - t n} n
      | c = 
}}
{{eqn | l = \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s + 1 - t \paren {n - k} } {n - k } \frac r {r - t k}
      | r = \binom {r + s + 1 - t n} n
      | c = Pascal's Rule
}}
{{end-eqn}}
Hence the equation holds for $\tuple {r, s + 1, t, n}$
{{qed}}
Theorem: Sum over k of r-kt choose k by r over r-kt by z^k

Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $\map {A_n} {x, t}$ be the polynomial of degree $n$ defined as:
:$\map {A_n} {x, t} := \dbinom {x - n t} n \dfrac x {x - n t}$
for $x \ne n t$.
Let $z = x^{t + 1} - x^t$.
Then:
:$\ds \sum_k \map {A_k} {r, t} z^k = x^r$
for sufficiently small $z$.

Proof:
From Sum over $k$ of $\paren {-1}^k$ by $\dbinom n k$ by $\dbinom {r - k t} n$ by $\dfrac r {r - k t}$ and renaming variables:
:$\ds \sum_j \paren {-1}^j \dbinom k j \dbinom {r - j t} k \dfrac r {r - j t} = \delta_{k 0}$
where $\delta_{k 0}$ is the Kronecker delta.
Thus:
:$\ds \sum_{j, k} \paren {-1}^j \dbinom k j \dbinom {r - j t} k \dfrac r {r - j t} w^k = 1$
We have:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{j, k} \paren {-1}^j \dbinom k j \dbinom {r - j t} k \dfrac r {r - j t} w^k
      | c = 
}}
{{eqn | r = \sum_j \paren {-1}^j \dfrac r {r - j t} \sum_k \dbinom k j \dbinom {r - j t} k w^k
      | c = 
}}
{{eqn | r = \sum_j \paren {-1}^j \dfrac r {r - j t} \sum_k \dbinom {r - j t} j \dbinom {r - j t - j} {k - j} w^k 
      | c = Product of $\dbinom r m$ with $\dbinom m k$
}}
{{eqn | r = \sum_j \paren {-1}^j \dfrac r {r - j t} \dbinom {r - j t} j \sum_k \dbinom {r - j t - j} {k - j} w^k  
      | c = 
}}
{{eqn | r = \sum_j \paren {-1}^j \map {A_j} {r, t} \sum_k \dbinom {r - j t - j} {k - j} w^k  
      | c = Definition of $\map {A_j} {r, t}$
}}
{{eqn | r = \sum_j \paren {-1}^j \map {A_j} {r, t} \paren {1 + w}^{r - j t - j} w^j
      | c = Binomial Theorem
}}
{{end-eqn}}
Now let:
:$x = \dfrac 1 {1 + w}$
{{begin-eqn}}
{{eqn | l = x
      | o = :=
      | r = \dfrac 1 {1 + w}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z
      | r = -\frac w {\paren {1 + w}^{1 + t} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {1 + w}^{r - j k - j} w^j \paren {-1}^j
      | r = z^r z^j
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \sum_j \map {A_j} {r, t} z^j \paren {1 + w}^r
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_j \map {A_j} {r, t} z^j
      | r = \paren {1 + w}^{- r}
      | c = 
}}
{{eqn | r = x^r
      | c = 
}}
{{end-eqn}}
{{finish|Establish the fact that we have convergence by ratio test and estimates for large $k$. Or use complex variable theory to establish that the function is analytic around $x {{=}} 1$.}}
{{qed}}
Theorem: Not Preceding implies Approximating Relation and not Preceding

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, y \in S$ such that
:$x \npreceq y$
Let $\RR$ be an approximating relation on $S$.
Then
:$\exists u \in S: \tuple {u, x} \in \RR \land u \npreceq y$

Proof:
By definition of approximating relation:
:$x = \map \sup {x^\RR}$
By definition of supremum:
:$y$ is upper bound for $x^\RR \implies x \preceq y$
By definition of upper bound:
:$\exists u \in S: u \in x^\RR \land u \npreceq y$
Thus by definition of $\RR$-segment:
:$\exists u \in S: \tuple {u, x} \in \RR \land u \npreceq y$
{{qed}}
Theorem: Auxiliary Approximating Relation has Quasi Interpolation Property

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a complete lattice.
Let $x, z \in S$.
Let $\RR$ be an auxiliary approximating relation on $S$ such that
:$\tuple {x, z} \in \RR \land x \ne z$
Then:
:$\exists y \in S: x \preceq y \land \tuple {y, z} \in \RR \land x \ne y$

Proof:
By definition of auxiliary relation:
:$x \preceq z$
By definition of $\prec$:
:$x \prec z$
By definition of antisymmetry:
:$z \nprec x$
Then:
:$z \npreceq x$
By Not Preceding implies Approximating Relation and not Preceding:
:$\exists u \in S: \tuple {u, z} \land u \npreceq x$
Define $y = x \vee u$.
Thus by Join Succeeds Operands:
:$x \preceq y$
Thus by definition of auxiliary relation:
:$\tuple {y, z} \in \RR$
Thus by Preceding iff Join equals Larger Operand:
:$x \ne y$
{{qed}}
Theorem: Preceding iff Join equals Larger Operand

Let $\left({S, \preceq}\right)$ be a join semilattice.
Let $x, y \in S$.
Then
:$x \preceq y$ {{iff}} $x \vee y = y$

Proof:
=== Sufficient Condition ===
Let
:$x \preceq y$
By definition of join:
:$x \vee y = \sup \left\{ {x, y}\right\}$
By definitions of upper bound and reflexivity:
:$y$ is upper bound for $\left\{ {x, y}\right\}$
and
:$\forall z \in S: z$ is upper bound for $\left\{ {x, y}\right\} \implies y \preceq z$
Thus by definition of supremum:
:$y = \sup \left\{ {x, y}\right\} = x \vee y$
{{qed|lemma}}
Theorem: Sum over k of -1^k by n choose k by r-kt choose n by r over r-kt

:$\ds \sum_k \paren {-1}^k \dbinom n k \dbinom {r - k t} n \dfrac r {r - k t} = \delta_{n 0}$
where $\delta_{n 0}$ is the Kronecker delta.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \sum_k \paren {-1}^k \dbinom n k \dbinom {r - k t} n \dfrac r {r - k t} = \delta_{n 0}$
=== Basis for the Induction ===
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \sum_k \paren {-1}^k \dbinom 0 k \dbinom {r - k t} 0 \dfrac r {r - k t}
      | r = \sum_k \paren {-1}^k \delta_{0 k} \dbinom {r - k t} 0 \dfrac r {r - k t}
      | c = Zero Choose n
}}
{{eqn | r = \dbinom r 0 \dfrac r r
      | c = All terms but for $k = 0$ vanish
}}
{{eqn | r = 1
      | c = Binomial Coefficient with Zero
}}
{{eqn | r = \delta_{0 0}
      | c = 
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P j$ is true, where $j \ge 0$, then it logically follows that $\map P {j + 1}$ is true.
So this is the induction hypothesis:
:$\ds \sum_k \paren {-1}^k \dbinom j k \dbinom {r - k t} j \dfrac r {r - k t} = \delta_{j 0}$
from which it is to be shown that:
:$\ds \sum_k \paren {-1}^k \dbinom {j + 1} k \dbinom {r - k t} {j + 1} \dfrac r {r - k t} = \delta_{\paren {j + 1} 0}$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_k \paren {-1}^k \dbinom {j + 1} k \dbinom {r - k t} {j + 1} \dfrac r {r - k t}
      | c = 
}}
{{eqn | r = \sum_k \paren {-1}^k \paren {\dbinom j k + \dbinom j {k - 1} } \dbinom {r - k t} {j + 1} \dfrac r {r - k t}
      | c = {{Defof|Binomial Coefficient}}
}}
{{end-eqn}}
{{finish|brain not working tonight. Ought to be able to split binomial coeffs and reduce but it didn't do what it should. Perhaps try to solve it by reducing to factorials.}}
So $\map P r \implies \map P {r + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds \forall n \in \Z_{\ge 0} \sum_k \paren {-1}^k \dbinom n k \dbinom {r - k t} n \dfrac r {r - k t} = \delta_{n 0}$
Theorem: Sum over k of r-kt choose k by z^k

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then:
:$\ds \sum_k \dbinom {r - t k} k z^k = \frac {x^{r + 1} } {\paren {t + 1} x - t}$
where $\dbinom {r - t k} k$ denotes a binomial coefficient.

Proof:
From  Sum over $k$ of $\dbinom r k$ by $\dbinom {s - k t} r$ by $\paren {-1}^k$ and renaming variables:
:$\ds \sum_j \paren {-1}^j \binom k j \binom {r - j t} k = t^k$
Thus:
{{begin-eqn}}
{{eqn | l = \sum_{j, k} \binom k j \binom {r - j t} k \paren {-1}^j
      | r = \sum_{k \mathop \ge 0} t^k
      | c = when $k < 0$ we have $\dbinom {r - j t} k = 0$
}}
{{eqn | ll= \leadsto
      | l = \sum_j \paren {-1}^j \sum_k \binom k j \binom {r - j t} k
      | r = \frac 1 {1 - t}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | ll= \leadsto
      | l = \sum_j \paren {-1}^j \sum_k \binom {r - j t} j \binom {r - j t - k} {j - k}
      | r = \frac 1 {1 - t}
      | c = Product of $\dbinom r m$ with $\dbinom m k$
}}
{{eqn | ll= \leadsto
      | l = \sum_j \paren {-1}^j \binom {r - j t} j \sum_k \binom {r - j t - k} {j - k}
      | r = \frac 1 {1 - t}
      | c = 
}}
{{end-eqn}}
{{finish|... and so on}}
Theorem: Sum over k of r-kt choose k by z^k

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then:
:$\ds \sum_k \dbinom {r - t k} k z^k = \frac {x^{r + 1} } {\paren {t + 1} x - t}$
where $\dbinom {r - t k} k$ denotes a binomial coefficient.

Proof:
From Sum over $k$ of $\dbinom {r - k t} k$ by $\dfrac r {r - k t}$ by $z^k$:
:$\ds (1): \quad \sum_k \map {A_k} {r, t} z^k = x^r$
where:
:$\map {A_n} {x, t}$ is the polynomial of degree $n$ defined as:
::$\map {A_n} {x, t} := \dbinom {x - n t} n \dfrac x {x - n t}$
:for $x \ne n t$
:$z = x^{t + 1} - x^t$.
Differentiating $(1)$ {{WRT|Differentiation}} $z$:
{{begin-eqn}}
{{eqn | l = \sum_k \map {A_k} {r, t} k z^{k - 1}
      | r = \frac \d {\d z} x^r
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \sum_k \map {A_k} {r, t} k z^k
      | r = z \frac \d {\d z} x^r
      | c = 
}}
{{eqn | r = \paren {x^{t + 1} - x^t} r x^{r - 1} \frac {\d x} {\d z}
      | c = Chain Rule for Derivatives
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = z
      | r = x^{t + 1} - x^t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d z} {\d x}
      | r = \paren {t + 1} x^t - t x^{t - 1}
      | c = Power Rule for Derivatives
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d z}
      | r = \frac 1 {\paren {t + 1} x^t - t x^{t - 1} }
      | c = Derivative of Inverse Function
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \sum_k k \map {A_k} {r, t} z^k
      | r = \frac {\paren {x^{t + 1} - x^t} r x^{r - 1} } {\paren {t + 1} x^t - t x^{t - 1} }
      | c = 
}}
{{eqn | r = \frac {\paren {x - 1} r x^r} {\paren {t + 1} x - t}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \sum_k \map {A_k} {r, t} z^k - \frac t r \sum_k k \map {A_k} {r, t} z^k
      | r = x^r - \frac t r \frac {\paren {x - 1} r x^r} {\paren {t + 1} x - t}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_k \paren {1 - \frac t r k} \map {A_k} {r, t} z^k 
      | r = \frac {\paren {\paren {t + 1} x - t} x^r - t \paren {x - 1} x^r} {\paren {t + 1} x - t}
      | c = 
}}
{{eqn | r = \frac {x^{r + 1} } {\paren {t + 1} x - t}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \sum_k \frac {r - t k} r \dbinom {r - k t} k \dfrac r {r - k t} z^k 
      | r = \frac {x^{r + 1} } {\paren {t + 1} x - t}
      | c = substituting for $\map {A_k} {r, t}$
}}
{{eqn | ll= \leadsto
      | l = \sum_k \dbinom {r - k t} k z^k 
      | r = \frac {x^{r + 1} } {\paren {t + 1} x - t}
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of r+tk choose k by s-tk choose n-k

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then:
:$\ds \sum_k \dbinom {r + t k} k \dbinom {s - t k} {n - k} = \sum_{k \mathop \ge 0} \dbinom {r + s - k} {n - k} t^k$
where $\dbinom {r + t k} k$ and so on denotes a binomial coefficient.

Proof:
Let $\map f {r, s, t, n}$ be the function defined as:
:$\ds \map f {r, s, t, n} := \sum_k \dbinom {r + t k} k \dbinom {s - t k} {n - k}$
We have:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_k \dbinom {r + t k} k \dbinom {s - t k} {n - k}
      | c = 
}}
{{eqn | r = \sum_k \dbinom {r + t k} k \dbinom {s - t k} {n - k} \frac {r + t k} {r + t k}
      | c = 
}}
{{eqn | r = \sum_k \dbinom {r + t k} k \dbinom {s - t k} {n - k} \frac r {r + t k} + \sum_k \dbinom {r + t k} k \dbinom {s - t k} {n - k} \frac {t k} {r + t k}
      | c = 
}}
{{end-eqn}}
{{proof wanted|in progress}}
Theorem: Way Below has Strong Interpolation Property

Let $L = \struct {S, \vee, \wedge, \preceq}$ be a bounded below continuous lattice.
Let $x, z \in S$ such that
:$x \ll z \land x \ne z$
Then
:$\exists y \in S: x \ll y \land y \ll z \land x \ne y$

Proof:
By Way Below is Approximating Relation and Way Below Relation is Auxiliary Relation:
:$\ll$ is an auxiliary approximating relation on $S$.
Thus by Auxiliary Approximating Relation has Interpolation Property:
:$\exists y \in S: x \ll y \land y \ll z \land x \ne y$
{{qed}}
Theorem: Way Below has Interpolation Property

Let $L = \left({S, \vee, \wedge, \preceq}\right)$ be a bounded below continuous lattice.
Let $x, z \in S$ such that
:$x \ll z$
Then
:$\exists y \in S: x \ll y \land y \ll z$

Proof:
Case $x \ne z$:
By Way Below has Strong Interpolation Property:
:$\exists y \in S: x \ll y \land y \ll z \land x \ne y$
Thus
:$\exists y \in S: x \ll y \land y \ll z$
Case $x = z$:
Define $y = x$
Thus
:$x \ll y \land y \ll z$
{{qed}}
Theorem: Left Coset Equals Subgroup iff Element in Subgroup

:$x H = H \iff x \in H$

Proof:
{{begin-eqn}}
{{eqn | l = x H
      | r = H
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = x H
      | r = e H
      | c = Left Coset by Identity: $e H = H$
}}
{{eqn | ll= \leadstoandfrom
      | l = x e^{-1}
      | o = \in
      | r = H
      | c = Left Cosets are Equal iff Product with Inverse in Subgroup
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = H
      | c = Group Properties
}}
{{end-eqn}}
{{Qed}}
Theorem: Right Coset Equals Subgroup iff Element in Subgroup

:$H x = H \iff x \in H$

Proof:
{{begin-eqn}}
{{eqn | l = H x
      | r = H
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = H x
      | r = H e
      | c = Right Coset by Identity: $H = H e$
}}
{{eqn | ll= \leadstoandfrom
      | l = x e^{-1}
      | o = \in
      | r = H
      | c = Right Cosets are Equal iff Product with Inverse in Subgroup
}}
{{eqn | ll= \leadstoandfrom
      | l = x
      | o = \in
      | r = H
      | c = Group Properties
}}
{{end-eqn}}
{{Qed}}
Theorem: Elements in Same Left Coset iff Product with Inverse in Subgroup

: $x, y$ are in the same left coset of $H$ {{iff}} $x^{-1} y \in H$.

Proof:
Let: $x H$ denote the left coset of $H$ by $x$
First we note that, from Congruence Class Modulo Subgroup is Coset, we have that the left cosets of $G$ form a partition of $G$.
Theorem: Elements in Same Right Coset iff Product with Inverse in Subgroup

: $x, y$ are in the same right coset of $H$ {{iff}} $x y^{-1} \in H$

Proof:
Let $H x$ denote the right coset of $H$ by $x$.
First we note that, from Congruence Class Modulo Subgroup is Coset, we have that the right cosets of $G$ form a partition of $G$.
Theorem: Sum over k of m+r+s Choose k by n+r-s Choose n-k by r+k Choose m+n

Let $m, n \in \Z_{\ge 0}$.
Then:
:$\ds \sum_{k \mathop \in \Z} \binom {m - r + s} k \binom {n + r - s} {n - k} \binom {r + k} {m + n} = \binom r m \binom s n$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{k \mathop \in \Z} \binom {m - r + s} k \binom {n + r - s} {n - k} \binom {r + k} {m + n}
      | c = 
}}
{{eqn | r = \sum_{k \mathop \in \Z} \binom {m - r + s} k \binom {n + r - s} {n - k} \paren { \sum_{j \mathop \in \Z} \binom r {m + n - j} \binom k j}
      | c = Chu-Vandermonde Identity
}}
{{eqn | r = \sum_{k \mathop \in \Z} \sum_{j \mathop \in \Z} \paren {\binom {m - r + s} k \binom k j } \binom {n + r - s} {n - k} \binom r {m + n - j}
      | c = rearranging
}}
{{eqn | r = \sum_{k \mathop \in \Z} \sum_{j \mathop \in \Z} \binom {m - r + s} j \binom {m - r + s - j} {k - j} \binom {n + r - s} {n - k} \binom r {m + n - j}
      | c = Product of $\dbinom r m$ with $\dbinom m k$
}}
{{eqn | r = \sum_{j \mathop \in \Z} \binom {m - r + s} j \binom r {m + n - j} \paren {\sum_{k \mathop \in \Z} \binom {m - r + s - j} {k - j} \binom {n + r - s} {n - k} }
      | c = grouping
}}
{{eqn | r = \sum_{j \mathop \in \Z} \binom {m - r + s} j \binom r {m + n - j} \binom {m + n - j} {n - j}
      | c = Chu-Vandermonde Identity
}}
{{eqn | r = \sum_{j \mathop \in \Z} \binom {m - r + s} j \binom r {m + n - j} \binom {m + n - j} m
      | c = Symmetry Rule for Binomial Coefficients
}}
{{eqn | r = \sum_{j \mathop \in \Z} \binom {m - r + s} j \binom r m \binom {r - m} {n - j}
      | c = Product of $\dbinom r m$ with $\dbinom m k$
}}
{{eqn | r = \binom r m \paren {\sum_{j \mathop \in \Z} \binom {m - r + s} j \binom {r - m} {n - j} }
      | c = 
}}
{{eqn | r = \binom r m \binom s n
      | c = Chu-Vandermonde Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of Unsigned Stirling Numbers of First Kind by x^k

:$\ds \sum_k {n \brack k} x^k = x^{\overline n}$
where:
:$\ds {n \brack k}$ denotes an unsigned Stirling number of the first kind
:$x^{\overline n}$ denotes $x$ to the $n$ rising.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_k \paren {-1}^{n - k} {n \brack k} x^k
      | r = x^{\underline n}
      | c = {{Defof|Unsigned Stirling Numbers of the First Kind}}
}}
{{eqn | ll= \leadsto
      | l = \sum_k \paren {-1}^{n - k} {n \brack k} \paren {-x}^k
      | r = \paren {-x}^{\underline n}
      | c = putting $-x$ for $x$
}}
{{eqn | ll= \leadsto
      | l = \paren {-1}^n \sum_k {n \brack k} x^k
      | r = \paren {-x}^{\underline n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_k {n \brack k} x^k
      | r = \paren {-1}^n \paren {-x}^{\underline n}
      | c = 
}}
{{eqn | r = x^{\overline n}
      | c = Rising Factorial in terms of Falling Factorial of Negative
}}
{{end-eqn}}
{{qed}}
Theorem: Capelli's Sum

:$\ds \paren {x + y}^{\overline n} = \sum_k \binom n k x^{\overline k} y^{\overline {n - k} }$
where:
:$\dbinom n k$ denotes a binomial coefficient
:$x^{\overline k}$ denotes $x$ to the $k$ rising.

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{> 0}$, let $\map P n$ be the proposition:
:$\ds \paren {x + y}^{\overline n} = \sum_k \binom n k x^{\overline k} y^{\overline {n - k} }$
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = \paren {x + y}^{\overline 1}
      | r = x^{\overline 1} + y^{\overline 1}
      | c = Number to Power of One Rising is Itself
}}
{{eqn | r = x^{\overline 0} y^{\overline 1} + x^{\overline 1} y^{\overline 0}
      | c = Number to Power of Zero Rising is One
}}
{{eqn | r = \binom 1 0 x^{\overline 0} y^{\overline 1} + \binom 1 1 x^{\overline 1} y^{\overline 0}
      | c = One Choose n
}}
{{eqn | r = \sum_k \binom 1 k x^{\overline k} y^{\overline {1 - k} }
      | c = 
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P m$ is true, where $m \ge 1$, then it logically follows that $\map P {m + 1}$ is true.
So this is the induction hypothesis:
:$\ds \paren {x + y}^{\overline m} = \sum_k \binom m k x^{\overline k} y^{\overline {m - k} }$
from which it is to be shown that:
:$\ds \paren {x + y}^{\overline {m + 1} } = \sum_k \binom {m + 1} k x^{\overline k} y^{\overline {m + 1 - k} }$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = \paren {x + y}^{\overline {m + 1} }
      | r = \paren {x + y}^{\overline m} \paren {x + y + m}
      | c = {{Defof|Rising Factorial}}
}}
{{eqn | r = \paren {\sum_k \binom m k x^{\overline k} y^{\overline {m - k} } } \paren {x + y + m}
      | c = Induction Hypothesis
}}
{{eqn | r = \paren {\sum_k \binom m k x^{\overline k} y^{\overline {m - k} } } \paren {x + k + y + m - k}
      | c = 
}}
{{eqn | r = \sum_k \binom m k x^{\overline k} \paren {x + k} y^{\overline {m - k} } + \sum_k \binom m k x^{\overline k} y^{\overline {m - k} } \paren {y + m - k}
      | c = 
}}
{{eqn | r = \sum_k \binom m k x^{\overline {k + 1} } y^{\overline {m - k} } + \sum_k \binom m k x^{\overline k} y^{\overline {m - k + 1} }
      | c = {{Defof|Rising Factorial}}
}}
{{eqn | r = \sum_k \binom m k x^{\overline {k + 1} } y^{\overline {m - k} } + \sum_k \binom m {k + 1} x^{\overline {k + 1} } y^{\overline {m - k} }
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_k \binom {m + 1} k x^{\overline {k + 1} } y^{\overline {m - k} }
      | c = Pascal's Rule
}}
{{end-eqn}}
So $\map P m \implies \map P {m + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds \forall n \in \Z_{> 0}: \paren {x + y}^{\overline n} = \sum_k \binom n k x^{\overline k} y^{\overline {n - k} }$
Theorem: Torelli's Sum

:$\ds \paren {x + y}^{\overline n} = \sum_k \binom n k x \paren {x - k z + 1}^{\overline {k - 1} } \paren {y + k z}^{\overline {n - k} }$
where:
:$\dbinom n k$ denotes a binomial coefficient
:$x^{\overline k}$ denotes $x$ to the $k$ rising.

Proof:
From Rising Factorial as Factorial by Binomial Coefficient:
:$\paren {x + y}^{\overline n} = n! \dbinom {x + y + n - 1} n$
Recall Sum over $k$ of $\dbinom {r - t k} k$ by $\dbinom {s - t \paren {n - k} } {n - k}$ by $\dfrac r {r - t k}$:
:$\ds \sum_{k \mathop \ge 0} \binom {r - t k} k \binom {s - t \paren {n - k} } {n - k} \frac r {r - t k} = \binom {r + s - t n} n$
Let the following substitutions be made:
:$r \gets x$
:$t \gets -\paren {1 - z}$
:$s \gets y - 1 + n z$
and so to obtain:
:$\ds \dbinom {x + y + n - 1} n = \sum_k \dbinom {x + \paren {1 - z} k} k \dbinom {y - 1 + n z + \paren {n - k} \paren {1 - z} } {n - k} \dfrac x {x + \paren {1 - z} k}$
Then:
{{begin-eqn}}
{{eqn | l = \dbinom {x + \paren {1 - z} k} k
      | r = \dfrac {\paren {x - k z + 1}^{\overline k} } {k!}
      | c = Rising Factorial as Factorial by Binomial Coefficient
}}
{{eqn | ll= \leadsto
      | l = \dfrac x {x + \paren {1 - z} k} \dbinom {x + \paren {1 - z} k} k
      | r = \dfrac {x \paren {x - k z + 1}^{\overline {k - 1} } } {k!}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \dbinom {y - 1 + n z + \paren {n - k} \paren {1 - z} } {n - k}
      | r = \dbinom {y - 1 + n z + n - k - n z + k z} {n - k}
      | c = 
}}
{{eqn | r = \dbinom {y + k z \paren {n - k} - 1} {n - k}
      | c = 
}}
{{eqn | r = \frac 1 {\paren {n - 1}!} \paren {y + k z}^{\overline {n - k} }
      | c = Rising Factorial as Factorial by Binomial Coefficient
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = n! \dbinom {x + y + n - 1} n
      | r = \sum_k \frac {n!} {k! \paren {n - k}!} x \paren {x - k z + 1}^{\overline {k - 1} } \paren {y + k z}^{\overline {n - k} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x + y}^{\overline n}
      | r = \sum_k \binom n k x \paren {x - k z + 1}^{\overline {k - 1} } \paren {y + k z}^{\overline {n - k} }
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Ruggiero Torelli|cat = Torelli}}