avewright/proofwiki-math huggingface dataset:
Theorem: Zeckendorf Representation of Integer shifted Left

Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \floor {x + \phi^{-1} }$
where:
:$\floor {\, \cdot \,}$ denotes the floor function
:$\phi$ denotes the golden mean.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $n$ be expressed in Zeckendorf representation:
:$n = F_{k_1} + F_{k_2} + \cdots + F_{k_r}$
with the appropriate restrictions on $k_1, k_2, \ldots, k_r$.
Then:
:$F_{k_1 + 1} + F_{k_2 + 1} + \cdots + F_{k_r + 1} = \map f {\phi n}$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = F_{k_j + 1} \hat \phi + F_{k_j}
      | r = \hat \phi^{k_j + 1}
      | c = Fibonacci Number by One Minus Golden Mean plus Fibonacci Number of Index One Less
}}
{{eqn | ll= \leadsto
      | l = F_{k_j + 1}
      | r = \hat \phi^{k_j} - \frac {F_{k_j} } {\hat \phi}
      | c = 
}}
{{eqn | r = \hat \phi^{k_j} + \phi F_{k_j}
      | c = Reciprocal Form of One Minus Golden Mean
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = F_{k_1 + 1} + F_{k_2 + 1} + \cdots + F_{k_r + 1}
      | r = \phi \paren {F_{k_1} + F_{k_2} + \cdots + F_{k_r} } + \paren {\hat \phi^{k_1} + \hat \phi^{k_2} + \cdots + \hat \phi^{k_r} }
      | c = 
}}
{{eqn | r = \phi n + \paren {\hat \phi^{k_1} + \hat \phi^{k_2} + \cdots + \hat \phi^{k_r} }
      | c = 
}}
{{end-eqn}}
We have that:
:$\hat \phi^3 + \hat \phi^5 + \hat \phi^7 + \cdots \le \hat \phi^{k_1} + \hat \phi^{k_2} + \cdots + \hat \phi^{k_r} \le \hat \phi^2 + \hat \phi^4 + \hat \phi^6 + \cdots$
Then:
{{begin-eqn}}
{{eqn | l = \hat \phi^3 + \hat \phi^5 + \hat \phi^7 + \cdots
      | r = \hat \phi^3 \paren {1 + \hat \phi^2 + \hat \phi^4 + \cdots}
      | c = 
}}
{{eqn | r = \dfrac {\hat \phi^3} {1 - \hat \phi^2}
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \dfrac {\phi^2 \hat \phi^3} {\phi^2  - \phi^2 \hat \phi^2}
      | c = 
}}
{{eqn | r = \dfrac {\paren {-1}^2 \hat \phi} {\phi^2 - \paren {-1}^2}
      | c = Golden Mean by One Minus Golden Mean equals Minus 1
}}
{{eqn | r = \dfrac {\hat \phi} {\phi^2 - 1}
      | c = 
}}
{{eqn | r = \dfrac {1 - \phi} {\phi^2 - 1}
      | c = {{Defof|One Minus Golden Mean}}
}}
{{eqn | r = \dfrac {1 - \phi} {1 + \phi - 1}
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{eqn | r = \phi^{-1} - 1
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \hat \phi^2 + \hat \phi^4 + \hat \phi^6 + \cdots
      | r = \frac 1 {\hat \phi} \paren {\hat \phi^3 + \hat \phi^5 + \hat \phi^7 + \cdots}
      | c = 
}}
{{eqn | r = \frac 1 {\hat \phi} \paren {\phi^{-1} - 1}
      | c = from above
}}
{{eqn | r = -\phi \paren {\frac 1 \phi - 1}
      | c = Reciprocal Form of One Minus Golden Mean
}}
{{eqn | r = -1 + \phi
      | c = 
}}
{{eqn | r = \frac 1 {\phi}
      | c = {{Defof|Golden Mean|index = 3}}
}}
{{eqn | r = \phi^{-1}
      | c = 
}}
{{end-eqn}}
Thus:
:$\phi^{-1} - 1 \le \hat \phi^{k_1} + \hat \phi^{k_2} + \cdots + \hat \phi^{k_r} \le \phi^{-1}$
and the result follows.
{{qed}}
Theorem: Zeckendorf Representation of Integer shifted Right

Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \floor {x + \phi^{-1} }$
where:
:$\floor {\, \cdot \,}$ denotes the floor function
:$\phi$ denotes the golden mean.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Let $n$ be expressed in Zeckendorf representation:
:$n = F_{k_1} + F_{k_2} + \cdots + F_{k_r}$
with the appropriate restrictions on $k_1, k_2, \ldots, k_r$.
Then:
:$F_{k_1 - 1} + F_{k_2 - 1} + \cdots + F_{k_r - 1} = \map f {\phi^{-1} n}$

Proof:
Follows directly from Zeckendorf Representation of Integer shifted Left, substituting $F_{k_j - 1}$ for $F_{k_j}$ throughout.
{{qed}}
Theorem: Two Non-Negative Integers have Zeckendorf Representations of which one is Shifted Representation of the Other

Let $m, n \in \Z_{\ge 0}$ be non-negative integers.
Then there exists a unique set of integers:
:$\left\{ {k_1, k_2, \ldots, k_r}\right\}$
where:
: $k_1 \gg k_2 \gg \cdots \gg k_r$
where $a \gg b$ denotes that $a - b > 1$
such that:
:$m = F_{k_1} + F_{k_2} + \cdots + F_{k_r}$
and:
:$n = F_{k_1 + 1} + F_{k_2 + 1} + \cdots + F_{k_r + 1}$
Note that:
: each of the $k$'s may be negative
and:
:$r$ may equal $0$.

Proof:
{{ProofWanted|When I have the concentration necessary. It's too hot to think at the moment.}}
Theorem: Existence of Interval of Convergence of Power Series/Corollary 2

Let $\ds \map S x = \sum_{n \mathop = 0}^\infty a_n x^n$ be a power series.
Let $\map S x$ be convergent at $x = x_0$.
Then $\map S x$ is convergent for all $x$ such that $\sequence x < \sequence {x_0}$.

Proof:
Let $\map S x$ converge when $x = x_0$.
Then by Existence of Interval of Convergence of Power Series, $x_0$ is in the interval of convergence of $\map S x$ whose midpoint is $0$.
The result follows by definition of interval of convergence.
{{qed}}
Theorem: Linear Combination of Generating Functions

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
and $\map H z$ be the generating function for the sequence $\sequence {b_n}$.
Then $\alpha \map G z + \beta \map H z$ is the generating function for the sequence $\sequence {\alpha a_n + \beta b_n}$.

Proof:
By definition:
:$\map G z = \ds \sum_{n \mathop \ge 0} a_n z^n$
:$\map H z = \ds \sum_{n \mathop \ge 0} b_n z^n$
Let $\map G z$ and $\map H z$ converge to $x$ and $y$ respectively for some $z_0 \in \R_{>0}$.
Then from Linear Combination of Convergent Series:
:$\ds \sum_{n \mathop \ge 0} \paren {\alpha a_n + \beta b_n} z^n = \alpha \sum_{n \mathop \ge 0} a_n z^n + \beta \sum_{n \mathop \ge 0} b_n z^n$
Hence the result.
{{qed}}
Theorem: Generating Function by Power of Parameter

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Let $m \in \Z_{\ge 0}$ be a non-negative integer.
Then $z^m \map G z$ is the generating function for the sequence $\sequence {a_{n - m} }$.

Proof:
{{begin-eqn}}
{{eqn | l = z^m \map G z
      | r = z^m \sum_{n \mathop \ge 0} a_n z^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{n \mathop \ge 0} a_n z^{n + m}
      | c = 
}}
{{eqn | r = \sum_{n + m \mathop \ge 0} a_{n - m} z^n
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{n \mathop \ge m} a_{n - m} z^n
      | c = 
}}
{{end-eqn}}
By letting $a_n = 0$ for all $n < 0$:
:$z^m \map G z = \ds \sum_{n \mathop \ge 0} a_{n - m} z^n$
Hence the result.
{{qed}}
Theorem: Generating Function Divided by Power of Parameter

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Let $m \in \Z_{\ge 0}$ be a non-negative integer.
Then $\dfrac 1 {z^m} \paren {\map G z - \ds \sum_{k \mathop = 0}^{m - 1} a_k z^k}$ is the generating function for the sequence $\sequence {a_{n + m} }$.

Proof:
{{begin-eqn}}
{{eqn | l = z^{-m} \map G z
      | r = z^{-m} \sum_{n \mathop \ge 0} a_n z^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{n \mathop \ge 0} a_n z^{n - m}
      | c = 
}}
{{eqn | r = \sum_{n + m \mathop \ge 0} a_{n + m} z^n
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{n \mathop \ge 0} a_{n + m} z^n + \sum_{k \mathop = -m}^{-1} a_{k + m} z^k
      | c = splitting up and changing variable 
}}
{{eqn | r = \sum_{n \mathop \ge 0} a_{n + m} z^n + \sum_{k \mathop = 0}^{m - 1} a_k z^{k - m}
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{n \mathop \ge 0} a_{n + m} z^n + z^{-m} \sum_{k \mathop = 0}^{m - 1} a_k z^k
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Generating Function for Linearly Recurrent Sequence

Let $\sequence {a_n}$ be a linearly recurrent sequence defined as:
:$a_n = \begin{cases} b_n & : 1 \le n \le m \\ c_1 a_{n - 1} + c_2 a_{n - 2} + \cdots + c_m a_{n - m} & : n > m \end{cases}$
where:
:$m \in \Z_{>0}$ is a (strictly) positive integer
:$b_1, \ldots, b_m$ are constants.
Then the generating function for $\sequence {a_n}$ is of the form:
:$\map G z = \dfrac {\map P z} {1 - c_1 z - c_2 z^2 - \cdots - c_m z^m}$
where $\map P z$ is a polynomial  in $z$ given by $b_1 z + b_2 z^2 + \cdots + b_m z^m$.

Proof:
{{begin-eqn}}
{{eqn | l = \map G z
      | r = \sum_{n \mathop \ge 1} a_n z^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{n \mathop > m} a_n z^n + \sum_{n \mathop = 1}^m a_n z^n
      | c = 
}}
{{eqn | r = \sum_{n \mathop > m} \paren {\sum_{n \mathop = 1}^m c_k a_{n-k} } z^n + \sum_{n \mathop = 1}^m b_n z^n
      | c = from sequence definition
}}
{{eqn | r = \sum_{n \mathop = 1}^m c_k \paren {\sum_{n \mathop > m}a_{n-k} z^n} + \sum_{n \mathop = 1}^m b_n z^n
      | c = Exchange of Order of Summation
}}
{{eqn | r = \sum_{n \mathop = 1}^m c_k \paren {z^m \map G z} + \sum_{n \mathop = 1}^m b_n z^n
      | c = Generating Function by Power of Parameter
}}
{{eqn | r = \map G z \sum_{n \mathop = 1}^m c_k z^m + \sum_{n \mathop = 1}^m b_n z^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map G z \paren {1 - \sum_{n \mathop = 1}^m c_k z^m}
      | r = \sum_{n \mathop = 1}^m b_n z^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map G z
      | r = \dfrac {\sum_{n \mathop = 1}^m b_n z^n} {1 - \sum_{n \mathop = 1}^m c_k z^m}
      | c = 
}}
{{eqn | r = \dfrac {b_1 z + b_2 z^2 + \cdots + b_m z^m} {1 - c_1 z - c_2 z^2 - \cdots - c_m z^m}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Product of Generating Functions

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Let $\map H z$ be the generating function for the sequence $\sequence {b_n}$.
Then $\map G z \map H z$ is the generating function for the sequence $\sequence {c_n}$, where:
:$\forall n \in \Z_{\ge 0}: c_n = \ds \sum_{k \mathop = 0}^n a_k b_{n - k}$

Proof:
By definition of generating function:
:$\map G z = \ds \sum_{n \mathop \ge 0} a_n z^n$
:$\map H z = \ds \sum_{n \mathop \ge 0} b_n z^n$
Then:
$\quad \begin {array}{c|ccccc}
\times & b_0 & b_1 z & b_2 z^2 & b_3 z^3 & \cdots \\
\hline
a_0 & a_0 b_0 & a_0 b_1 z & a_0 b_2 z^2 & a_0 b_3 z^3 & \cdots \\
a_1 z & a_1 b_0 z & a_1 b_1 z^2 & a_1 b_2 z^3 & a_1 b_3 z^4 & \cdots \\
a_2 z^2 & a_2 b_0 z^2 & a_2 b_1 z^3 & a_2 b_2 z^4 & a_2 b_3 z^5 & \cdots \\
a_3 z^3 & a_3 b_0 z^3 & a_3 b_1 z^4 & a_3 b_2 z^5 & a_3 b_3 z^6 & \cdots \\
\vdots & \vdots & \vdots & \vdots & \vdots & \ddots 
\end {array}$
The result follows by definition of generating function.
{{qed}}
Theorem: Generating Function for Sequence of Partial Sums of Series

Let $s$ be the the series:
:$\ds s = \sum_{n \mathop = 1}^\infty a_n = a_0 + a_1 + a_2 + a_3 + \cdots$
Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Let $\sequence {c_n}$ denote the sequence of partial sums of $s$.
Then the generating function for $\sequence {c_n}$ is given by:
:$\ds \dfrac 1 {1 - z} \map G z = \sum_{n \mathop \ge 0} c_n z^n$

Proof:
By definition of sequence of partial sums of $s$:
{{begin-eqn}}
{{eqn | l = \sequence {c_n}
      | r = a_0 + \paren {a_0 + a_1} + \paren {a_0 + a_1 + a_2} + \cdots
      | c = 
}}
{{eqn | r = \sum_{n \mathop \ge 0} \paren {\sum_{k \mathop = 0}^n a_k}
      | c = 
}}
{{end-eqn}}
Consider the sequence $\sequence {b_n}$ defined as:
:$\forall n \in \Z_{\ge 0}: b_n = 1$
Let $\map H z$ be the generating function for $\sequence {b_n}$.
By Generating Function for Constant Sequence:
:$\map H z = \dfrac 1 {1 - z}$
Then:
{{begin-eqn}}
{{eqn | l = \map G z \map H z
      | r = \sum_{n \mathop \ge 0} \paren {\sum_{k \mathop = 0}^n a_k b_{n - k} } z^n
      | c = Product of Generating Functions
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 {1 - z} \map G z
      | r = \sum_{n \mathop \ge 0} \paren {\sum_{k \mathop = 0}^n a_k} z^n
      | c = as all $b_{n - k} = 1$
}}
{{eqn | r = \sum_{n \mathop \ge 0} c_n z^n
      | c = 
}}
{{end-eqn}}
Hence the result by definition of generating function.
{{qed}}
Theorem: Product of Generating Functions/General Rule

Let $\map {G_0} z, \map {G_1} z, \map {G_2} z, \ldots$ be any number of generating functions (up to countably infinite) for the sequences $\sequence {a_0 n}, \sequence {a_1 n}, \sequence {a_2 n}, \ldots$
Then:
{{begin-eqn}}
{{eqn | l = \prod_{j \mathop \ge 0} \map {G_j} z
      | r = \prod_{j \mathop \ge 0} \sum_{k \mathop \ge 0} a_{j k} z^k
      | c = 
}}
{{eqn | r = \sum_{n \mathop \ge 0} z^n \sum_{\substack {k_0, k_1, k_2, \ldots \mathop \ge 0 \\ k_0 \mathop + k_1 \mathop + \mathop \cdots \mathop = n} } \paren {\prod_{j \mathop \ge 0} a_{j k} }
      | c = 
}}
{{end-eqn}}

Proof:
{{ProofWanted|There may be some general convolution result that can be used. Good luck Jim.}}
Theorem: Product of Exponential Generating Functions

Let $\map G z$ be the exponential generating function for the sequence $\sequence {\dfrac {a_n} {n!} }$.
Let $\map H z$ be the exponential generating function for the sequence $\sequence {\dfrac {b_n} {n!} }$.
Then $\map G z \map H z$ is the generating function for the sequence $\sequence {\dfrac {c_n} {n!} }$, where:
:$\forall n \in \Z_{\ge 0}: c_n = \ds \sum_{k \mathop \in \Z} \dbinom n k a_k b_{n - k}$

Proof:
Let $\map G z \map H z$ be the generating function for the sequence $\sequence {c'_n}$.
By definition of generating function:
{{begin-eqn}}
{{eqn | l = \map G z \map H z
      | r = \sum_{k \mathop \ge 0} \dfrac {a_k} {k!} z^k \sum_{k \mathop \ge 0} \dfrac {b_k} {k!} z^k
      | c = 
}}
{{eqn | r = \paren {\dfrac {a_0} {0!} + \dfrac {a_1} {1!} z + \dfrac {a_2} {2!} z^2 + \cdots} \paren {\dfrac {b_0} {0!} + \dfrac {b_1} {1!} z + \dfrac {b_2} {2!} z^2 + \cdots}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = c'_n
      | r = \sum_{k \mathop = 0}^n \dfrac {a_k} {k!} \dfrac {b_{n - k} } {\paren {n - k}!}
      | c = Product of Generating Functions
}}
{{eqn | r = \dfrac 1 {n!} \paren {\sum_{k \mathop = 0}^n \dfrac {n!} {k! \paren {n - k}!} a_k b_{n - k} }
      | c = 
}}
{{eqn | r = \dfrac 1 {n!} \paren {\sum_{k \mathop = 0}^n \dbinom n k a_k b_{n - k} }
      | c = {{Defof|Binomial Coefficient/Integers|index = 1|disp = Binomial Coefficient}}
}}
{{eqn | r = \dfrac {c_n} {n!}
      | c = where $c_n = \ds \sum_{k \mathop = 0}^n \dbinom n k a_k b_{n - k}$
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Generating Function of Multiple of Parameter

Let $G \left({z}\right)$ be the generating function for the sequence $\left\langle{a_n}\right\rangle$.
Let $c$ be a constant.
Then $G \left({c z}\right)$ be the generating function for the sequence $\left\langle{b_n}\right\rangle$ where:
:$\forall n \in \Z_{\ge 0}: b_n = c^n a_n$

Proof:
{{begin-eqn}}
{{eqn | l = G \left({c z}\right)
      | r = \sum_{n \mathop \ge 0} a_n \left({c z}\right)^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{n \mathop \ge 0} \left({a_n c^n}\right) z^n
      | c = 
}}
{{end-eqn}}
Hence the result by definition of generating function.
{{qed}}
Theorem: Generating Function for Sequence of Powers of Constant

Let $c \in \R$ be a constant.
Let $\sequence {a_n}$ be the sequence defined as:
:$\forall n \in \Z_{\ge 0}: a_n = c^n$
That is:
:$\sequence {a_n} = 1, c, c^2, c^3, \ldots$
Then the generating function for $\sequence {a_n}$ is given as:
:$\map G z = \dfrac 1 {1 - c z}$

Proof:
Consider the sequence $\sequence {b_n}$ defined as:
: $\forall n \in \Z_{\ge 0}: b_n = 1$
Let $\map H z$ be the generating function for $\sequence {b_n}$.
Then:
{{begin-eqn}}
{{eqn | l = \map H z
      | r = \dfrac 1 {1 - z}
      | c = Generating Function for Constant Sequence
}}
{{eqn | ll= \leadsto
      | l =\map H {c z}
      | r = \dfrac 1 {1 - c z}
      | c = 
}}
{{eqn | r = \sum_{n \mathop \ge 0} \paren {b_n c^n} z^n
      | c = Generating Function of Multiple of Parameter
}}
{{eqn | r = \sum_{n \mathop \ge 0} c^n z^n
      | c = as $b_n = 1$ throughout
}}
{{end-eqn}}
The result follows from the definition of a generating function.
{{qed}}
Theorem: Generating Function for Even Terms of Sequence

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Consider the subsequence $\sequence {b_n} := \tuple {a_0, a_2, a_4, \ldots}$
Then the generating function for $\sequence {b_n}$ is:
:$\dfrac 1 2 \paren {\map G z + \map G {-z} }$

Proof:
{{begin-eqn}}
{{eqn | l = \map G z
      | r = \sum_{n \mathop \ge 0} a_n z^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{r \mathop \ge 0} a_{2 r} z^{2 r} + \sum_{r \mathop \ge 0} a_{2 r + 1} z^{2 r + 1}
      | c = separating out odd and even integers
}}
{{eqn | l = \map G {-z}
      | r = \sum_{n \mathop \ge 0} a_n \paren {-z}^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{n \mathop \ge 0} \paren {-1}^n a_n z^n
      | c = 
}}
{{eqn | r = \sum_{r \mathop \ge 0} \paren {-1}^{2 r} a_{2 r} z^{2 r} + \sum_{r \mathop \ge 0} \paren {-1}^{2 r + 1} a_{2 r + 1} z^{2 r + 1}
      | c = separating out odd and even integers
}}
{{eqn | r = \sum_{r \mathop \ge 0} a_{2 r} z^{2 r} - \sum_{r \mathop \ge 0} a_{2 r + 1} z^{2 r + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map G z + \map G {-z}
      | r = 2 \sum_{r \mathop \ge 0} a_{2 r} z^{2 r}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Generating Function for Odd Terms of Sequence

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Consider the subsequence $\sequence {b_n} := \tuple {a_1, a_3, a_5, \ldots}$
Then the generating function for $\sequence {b_n}$ is:
:$\dfrac 1 2 \paren {\map G z - \map G {-z} }$

Proof:
{{begin-eqn}}
{{eqn | l = \map G z
      | r = \sum_{n \mathop \ge 0} a_n z^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{r \mathop \ge 0} a_{2 r} z^{2 r} + \sum_{r \mathop \ge 0} a_{2 r + 1} z^{2 r + 1}
      | c = separating out odd and even integers
}}
{{eqn | l = \map G {-z}
      | r = \sum_{n \mathop \ge 0} a_n \paren {-z}^n
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{n \mathop \ge 0} \paren {-1}^n a_n z^n
      | c = 
}}
{{eqn | r = \sum_{r \mathop \ge 0} \paren {-1}^{2 r} a_{2 r} z^{2 r} + \sum_{r \mathop \ge 0} \paren {-1}^{2 r + 1} a_{2 r + 1} z^{2 r + 1}
      | c = separating out odd and even integers
}}
{{eqn | r = \sum_{r \mathop \ge 0} a_{2 r} z^{2 r} - \sum_{r \mathop \ge 0} a_{2 r + 1} z^{2 r + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map G z - \map G {-z}
      | r = 2 \sum_{r \mathop \ge 0} a_{2 r + 1} z^{2 r + 1}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Generating Function for mth Terms of Sequence

Let $G \left({z}\right)$ be the generating function for the sequence $\left\langle{a_n}\right\rangle$.
Let $m \in \Z_{>0}$ be a (strictly) positive integer.
Let $\omega = e^{2 i \pi / m} = \cos \dfrac {2 \pi} m + i \sin \dfrac {2 \pi} m$.
Then for $r \in \Z$ such that $0 \le r < m$:
:$\displaystyle \sum_{n \bmod m \mathop = r} a_n z^n = \dfrac 1 m \sum_{0 \mathop \le k \mathop < m} \omega^{-k r} G \left({\omega^k z}\right)$

Proof:
{{begin-eqn}}
{{eqn | l = \omega^{-k r} \map G {\omega^k z}
      | r = \sum_{j \mathop \ge 0} a_j \omega^{k \paren {j - r} } z^j
      | c = {{Defof|Generating Function}}
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 m \sum_{0 \mathop \le k \mathop < m} \omega^{-k r} \map G {\omega^k z}
      | r = \dfrac 1 m \sum_{0 \mathop \le k \mathop < m} \ \sum_{j \mathop \ge 0} a_j \omega^{k \paren {j - r} } z^j
      | c = 
}}
{{eqn | r = \dfrac 1 m \sum_{j \mathop \ge 0} a_j z^j \ \sum_{0 \mathop \le k \mathop < m} \omega^{k \paren {j - r} }
      | c = 
}}
{{end-eqn}}
By definition of $\omega$:
:$\omega = \exp \dfrac {2 \pi i} m \implies \omega^m = 1$
and so:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le k \mathop < m} \omega^{k \paren {j - r} }
      | r = \begin {cases} \dfrac {1 - \omega^{m \paren {j - r} } } {1 - \omega^{j - r} } & : j - r \not \equiv 0 \pmod m \\ m & : j \equiv r \pmod m \end {cases}
      | c = Sum of Geometric Progression
}}
{{eqn | ll= \leadsto
      | l = \dfrac 1 m \sum_{0 \mathop \le k \mathop < m} \omega^{-k r} \map G {\omega^k z}
      | r = \dfrac 1 m \sum_{j \mathop \ge 0} m a_j \sqbrk {j \equiv r \pmod m} z^j
      | c = where $\sqbrk \cdots$ is Iverson's convention
}}
{{eqn | r = \sum_{n \bmod m \mathop = r} a_n z^n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Generating Function

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Then:
{{begin-eqn}}
{{eqn | l = \frac \d {\d z} \map G z
      | r = \sum_{k \mathop \ge 0} \left({k + 1}\right) a_{k + 1} z^k
      | c = 
}}
{{eqn | r = a_1 + 2 a_2 z + 3 a_3 z^3 + \cdots
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \frac \d {\d z} \map G z
      | r = \frac \d {\d z} \paren {\sum_{k \mathop \ge 0} a_k z^k}
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{k \mathop \ge 0} \paren {\frac \d {\d z} a_k z^k}
      | c = 
}}
{{eqn | r = \sum_{k \mathop \ge 0} k a_k z^{k - 1}
      | c = Power Rule for Derivatives
}}
{{eqn | r = \sum_{k \mathop \ge 1} k a_k z^{k - 1}
      | c = as the zeroth term vanishes when $k = 0$
}}
{{eqn | r = \sum_{k \mathop \ge 0} \paren {k + 1} a_{k + 1} z^k
      | c = Translation of Index Variable of Summation
}}
{{end-eqn}}
{{qed}}
Theorem: Generating Function of Sequence by Index

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Then:
:$z \map {G'} z$ is the generating function for the sequence $\sequence {n a_n}$
where $\map {G'} z$ is the derivative of $\map G z$ {{WRT|Differentiation}} $z$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {G'} z
      | r = \sum_{k \mathop \ge 0} \paren {k + 1} a_{k + 1} z^k
      | c = Derivative of Generating Function
}}
{{eqn | ll= \leadsto
      | l = z \map {G'} z
      | r = \sum_{k \mathop \ge 0} \paren {k + 1} a_{k + 1} z^{k + 1}
      | c = 
}}
{{eqn | r = \sum_{k + 1 \mathop \ge 0} k a_k z^k
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \sum_{k \mathop \ge 0} k a_k z^k
      | c = as the term vanishes when $k = 0$
}}
{{end-eqn}}
The result follows by definition of generating function.
{{qed}}
Theorem: Integral of Generating Function

Let $\map G z$ be the generating function for the sequence $\sequence {a_n}$.
Then:
{{begin-eqn}}
{{eqn | l = \int_0^z \map G t \rd t
      | r = \sum_{k \mathop \ge 1} \dfrac {a_{k - 1} z^k} k
      | c = 
}}
{{eqn | r = a_0 z + \dfrac {a_1 z^2} 2 + \dfrac {a_2 z^3} 3 + \dfrac {a_3 z^4} 4 + \cdots
      | c = 
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^z \map G t \rd t
      | r = \int_0^z \paren {\sum_{k \mathop \ge 0} a_k t^k} \rd t
      | c = {{Defof|Generating Function}}
}}
{{eqn | r = \sum_{k \mathop \ge 0} \paren {\int_0^z a_k t^k \rd t}
      | c = Tonelli's Theorem
}}
{{eqn | r = \sum_{k \mathop \ge 0} \paren {\intlimits {a_k \dfrac {t^{k + 1} } {k + 1} } 0 z}
      | c = Primitive of Power
}}
{{eqn | r = \sum_{k \mathop \ge 0} \paren {a_k \dfrac {z^{k + 1} } {k + 1} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop \ge 1} \dfrac {a_{k - 1} z^k} k
      | c = Translation of Index Variable of Summation
}}
{{end-eqn}}
{{qed}}
Theorem: Generating Function for Sequence of Reciprocals of Natural Numbers

Let $\sequence {a_n}$ be the sequence defined as:
:$\forall n \in \N_{> 0}: a_n = \dfrac 1 n$
That is:
:$\sequence {a_n} = 1, \dfrac 1 2, \dfrac 1 3, \dfrac 1 4, \ldots$
Then the generating function for $\sequence {a_n}$ is given as:
:$\map G z = \map \ln {\dfrac 1 {1 - z} }$

Proof:
Take the sequence:
:$S_n = 1, 1, 1, \ldots$
From Generating Function for Constant Sequence, this has the generating function:
:$\ds \map G z = \sum_{n \mathop = 0}^\infty z^n = \frac 1 {1 - z}$
By Integral of Generating Function:
{{begin-eqn}}
{{eqn | l = \int_0^z \map G t \rd t
      | r = \sum_{k \mathop \ge 1} \dfrac {z^k} k
      | c = 
}}
{{eqn | r = z + \dfrac {z^2} 2 + \dfrac {z^3} 3 + \dfrac {z^4} 4 + \cdots
      | c = 
}}
{{end-eqn}}
which is the power series whose coefficients are $\sequence {a_n}$.
But:
:$\map G z = \dfrac 1 {1 - z}$
and so by Primitive of Reciprocal and the Integration by Substitution:
{{begin-eqn}}
{{eqn | l = \int_0^z \map G t \rd t
      | r = \int_0^z \dfrac 1 {1 - t} \rd t
      | c = 
}}
{{eqn | r = \map \ln {\dfrac 1 {1 - z} }
      | c = 
}}
{{end-eqn}}
The result follows from the definition of generating function.
{{qed}}