1.9 Non-integer powers

1.9.1 Definition

Definition 1.245

✓

An FPS $f\in K[[x]]$ has constant term one if $[x^0]f=1$. We write $f\in K[[x]]_1$ for this condition.

docs source

def AlgebraicCombinatorics.FPS.HasConstantTermOne {K : Type u_1} [CommRing K] (f : PowerSeries K) :

Prop

AlgebraicCombinatorics.FPS.HasConstantTermOne f = (PowerSeries.constantCoeff f = 1)

Lemma 1.246

✓

If $f,g\in K[[x]]_1$, then $fg\in K[[x]]_1$.

docs source

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_mul {K : Type u_1} [CommRing K] {f g : PowerSeries K} (hf : HasConstantTermOne f) (hg : HasConstantTermOne g) :

HasConstantTermOne (f * g)

Proof ▶

$[x^0](fg) = ([x^0]f)([x^0]g) = 1\cdot 1 = 1$.

Lemma 1.247

✓

$1+x\in K[[x]]_1$.

docs source

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_one_add_X {K : Type u_1} [CommRing K] :

HasConstantTermOne (1 + PowerSeries.X)

Proof ▶

$[x^0](1+x) = 1$.

The Log map

Definition 1.248

✓

The logarithm series (or $\overline{\log }$) is the FPS

\[ \overline{\log } := \sum _{n\geq 1} \frac{(-1)^{n-1}}{n} x^n = x - \frac{x^2}{2} + \frac{x^3}{3} - \cdots \in K[[x]]. \]

Its constant term is $0$.

docs source

noncomputable def AlgebraicCombinatorics.FPS.logSeries {K : Type u_1} [CommRing K] [Algebra ℚ K] :

PowerSeries K

AlgebraicCombinatorics.FPS.logSeries = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else (algebraMap ℚ K) ((-1) ^ (n - 1) / ↑n)

Lemma 1.249

✓

$[x^0]\overline{\log } = 0$.

docs source

theorem AlgebraicCombinatorics.FPS.constantCoeff_logSeries {K : Type u_1} [CommRing K] [Algebra ℚ K] :

PowerSeries.constantCoeff logSeries = 0

Proof ▶

Immediate from the definition.

Definition 1.250

✓

For $f\in K[[x]]_1$, we define

\[ \operatorname {Log}(f) := \overline{\log } \circ (f-1). \]

Since $f$ has constant term $1$, the FPS $f-1$ has constant term $0$, so the substitution is well-defined.

docs source

noncomputable def AlgebraicCombinatorics.FPS.fpsLog {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) :

PowerSeries K

AlgebraicCombinatorics.FPS.fpsLog f = PowerSeries.subst (f - 1) AlgebraicCombinatorics.FPS.logSeries

Lemma 1.251

✓

$\operatorname {Log}(1) = 0$.

docs source

theorem AlgebraicCombinatorics.FPS.fpsLog_one {K : Type u_1} [CommRing K] [Algebra ℚ K] :

fpsLog 1 = 0

Proof ▶

$\operatorname {Log}(1) = \overline{\log }\circ (1-1) = \overline{\log }\circ 0 = 0$, since every term in the substitution sum is zero.

Lemma 1.252

✓

For $f\in K[[x]]_1$, we have $[x^0]\operatorname {Log}(f)=0$.

docs source

theorem AlgebraicCombinatorics.FPS.constantCoeff_fpsLog {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) :

PowerSeries.constantCoeff (fpsLog f) = 0

Proof ▶

The constant term of a substitution $g\circ h$ where both $[x^0]g=0$ and $[x^0]h=0$ is $0$.

Theorem 1.253

✓

For $f,g\in K[[x]]_1$,

\[ \operatorname {Log}(fg) = \operatorname {Log}(f) + \operatorname {Log}(g). \]

docs source

theorem AlgebraicCombinatorics.FPS.fpsLog_mul {K : Type u_1} [CommRing K] [Algebra ℚ K] {f g : PowerSeries K} (hf : HasConstantTermOne f) (hg : HasConstantTermOne g) :

fpsLog (f * g) = fpsLog f + fpsLog g

Proof ▶

Let $h = \operatorname {Log}(fg) - \operatorname {Log}(f) - \operatorname {Log}(g)$. We show $h'=0$ and $[x^0]h = 0$ using the derivative characterization: $(d/dx)\operatorname {Log}(f) = (d/dx \overline{\log })\circ (f-1)\cdot f'$, and the key identity $(d/dx\, \overline{\log })\circ (f-1)\cdot f = 1$ (since $d/dx\, \overline{\log } = 1/(1+x)$ and substituting $f-1$ gives $1/f$). The Leibniz rule for $(fg)'$ then shows $h'=0$. Since $[x^0]h = 0-0-0 = 0$ and $h'=0$, uniqueness gives $h=0$.

The Exp map

Definition 1.254

✓

For $g\in K[[x]]_0$ (FPS with constant term $0$), we define

\[ \operatorname {Exp}(g) := \exp \circ \, g = \left(\sum _{n\in \mathbb {N}} \frac{x^n}{n!}\right)\circ g. \]

Since $g$ has constant term $0$, the substitution is well-defined.

docs source

noncomputable def AlgebraicCombinatorics.FPS.fpsExp {K : Type u_1} [CommRing K] [Algebra ℚ K] (g : PowerSeries K) :

PowerSeries K

AlgebraicCombinatorics.FPS.fpsExp g = PowerSeries.subst g (PowerSeries.exp K)

Lemma 1.255

✓

$\operatorname {Exp}(0)=1$.

docs source

theorem AlgebraicCombinatorics.FPS.fpsExp_zero {K : Type u_1} [CommRing K] [Algebra ℚ K] :

fpsExp 0 = 1

Proof ▶

Only the $m=0$ term in the substitution sum is nonzero, giving $1$.

Lemma 1.256

✓

For $g\in K[[x]]_0$, we have $\operatorname {Exp}(g)\in K[[x]]_1$.

docs source

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_fpsExp {K : Type u_1} [CommRing K] [Algebra ℚ K] {g : PowerSeries K} (hg : PowerSeries.constantCoeff g = 0) :

HasConstantTermOne (fpsExp g)

Proof ▶

The constant term of $\operatorname {Exp}(g) = \exp \circ g$ is $[x^0]\exp = 1/0! = 1$, since all higher powers of $g$ contribute $0$ to the constant term.

Theorem 1.257

✓

For $u,v\in K[[x]]_0$,

\[ \operatorname {Exp}(u+v) = \operatorname {Exp}(u)\cdot \operatorname {Exp}(v). \]

docs source

theorem AlgebraicCombinatorics.FPS.fpsExp_add {K : Type u_1} [CommRing K] [Algebra ℚ K] {x y : PowerSeries K} (hx : PowerSeries.constantCoeff x = 0) (hy : PowerSeries.constantCoeff y = 0) :

fpsExp (x + y) = fpsExp x * fpsExp y

Proof ▶

Follows from the multiplicativity of the exponential map, established in Mathlib’s Exp/Log theory for formal power series.

The power definition

Definition 1.258

✓

Assume that $K$ is a commutative $\mathbb {Q}$-algebra. Let $f\in K\left[ \left[ x\right] \right] _{1}$ and $c\in K$. Then, we define an FPS

\[ f^{c}:=\operatorname {Exp}\left( c\operatorname {Log}f\right) \in K\left[ \left[ x\right] \right] _{1}. \]

docs source

noncomputable def AlgebraicCombinatorics.FPS.fpsPow {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) (c : K) :

PowerSeries K

AlgebraicCombinatorics.FPS.fpsPow f c = AlgebraicCombinatorics.FPS.fpsExp (c • AlgebraicCombinatorics.FPS.fpsLog f)

Lemma 1.259

✓

For any $f\in K[[x]]$, we have $f^0 = 1$.

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_zero {K : Type u_1} [CommRing K] [Algebra ℚ K] (f : PowerSeries K) :

fpsPow f 0 = 1

Proof ▶

$f^0 = \operatorname {Exp}(0\cdot \operatorname {Log}f) = \operatorname {Exp}(0) = 1$.

Lemma 1.260

✓

For $f\in K[[x]]_1$ and $c\in K$, we have $f^c\in K[[x]]_1$.

docs source

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_fpsPow {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) (c : K) :

HasConstantTermOne (fpsPow f c)

Proof ▶

Since $[x^0]\operatorname {Log}f = 0$, we have $[x^0](c\operatorname {Log}f) = 0$, so $\operatorname {Exp}(c\operatorname {Log}f)\in K[[x]]_1$.

Lemma 1.261

✓

For $f\in K[[x]]_1$, we have $f^1 = f$.

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_one {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) :

fpsPow f 1 = f

Proof ▶

$f^1 = \operatorname {Exp}(1\cdot \operatorname {Log}f) = \operatorname {Exp}(\operatorname {Log}f) = f$, using the inverse property $\operatorname {Exp}\circ \operatorname {Log} = \operatorname {id}$ on $K[[x]]_1$. The formal proof bridges the local definitions of $\operatorname {Log}$ and $\operatorname {Exp}$ to Mathlib’s Exp/Log framework (via Lemmas 1.273 and 1.274) and then applies the inverse property.

1.9.2 Rules of exponents

Theorem 1.262

Assume that $K$ is a commutative $\mathbb {Q}$-algebra. For any $a,b\in K$ and $f,g\in K\left[ \left[ x\right] \right] _{1}$, we have

\[ f^{a+b}=f^{a}f^{b},\ \ \ \ \ \ \ \ \ \ \left( fg\right) ^{a}=f^{a}g^{a},\ \ \ \ \ \ \ \ \ \ \left( f^{a}\right) ^{b}=f^{ab}. \]

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_add {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) (a b : K) :

fpsPow f (a + b) = fpsPow f a * fpsPow f b

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_mul {K : Type u_1} [CommRing K] [Algebra ℚ K] {f g : PowerSeries K} (hf : HasConstantTermOne f) (hg : HasConstantTermOne g) (a : K) :

fpsPow (f * g) a = fpsPow f a * fpsPow g a

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_pow {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) (a b : K) :

fpsPow (fpsPow f a) b = fpsPow f (a * b)

Proof ▶

First rule ($f^{a+b}=f^af^b$):

\begin{align*} f^{a+b} & = \operatorname {Exp}((a+b)\operatorname {Log}f) \\ & = \operatorname {Exp}(a\operatorname {Log}f + b\operatorname {Log}f) \\ & = \operatorname {Exp}(a\operatorname {Log}f)\cdot \operatorname {Exp}(b\operatorname {Log}f) \quad \text{(by }\operatorname {Exp}(x+y)=\operatorname {Exp}(x)\operatorname {Exp}(y)\text{)} \\ & = f^a \cdot f^b. \end{align*}

Second rule ($(fg)^a = f^a g^a$):

\begin{align*} (fg)^a & = \operatorname {Exp}(a\operatorname {Log}(fg)) \\ & = \operatorname {Exp}(a(\operatorname {Log}f + \operatorname {Log}g)) \quad \text{(by }\operatorname {Log}(fg)=\operatorname {Log}f+\operatorname {Log}g\text{)} \\ & = \operatorname {Exp}(a\operatorname {Log}f + a\operatorname {Log}g) \\ & = \operatorname {Exp}(a\operatorname {Log}f)\cdot \operatorname {Exp}(a\operatorname {Log}g) = f^a\cdot g^a. \end{align*}

Third rule ($(f^a)^b = f^{ab}$):

\begin{align*} (f^a)^b & = \operatorname {Exp}(b\operatorname {Log}(f^a)) \\ & = \operatorname {Exp}(b\operatorname {Log}(\operatorname {Exp}(a\operatorname {Log}f))) \\ & = \operatorname {Exp}(b\cdot a\operatorname {Log}f) \quad \text{(by }\operatorname {Log}\circ \operatorname {Exp} = \operatorname {id}\text{)} \\ & = \operatorname {Exp}((ab)\operatorname {Log}f) = f^{ab}. \end{align*}

Lemma 1.263

✓

For $f\in K[[x]]_1$ and $n\in \mathbb {N}$, we have $f^n = \underbrace{f\cdot f\cdots f}_{n\text{ times}}$. That is, our definition of $f^c$ is consistent with the standard power when $c\in \mathbb {N}$.

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_nat {K : Type u_1} [CommRing K] [Algebra ℚ K] [CharZero K] {f : PowerSeries K} (hf : HasConstantTermOne f) (n : ℕ) :

fpsPow f ↑n = f ^ n

Proof ▶

By induction on $n$: the base case $n=0$ gives $f^0=1$ (by Lemma 1.259), and the inductive step uses $f^{n+1} = f^n\cdot f^1 = f^n\cdot f$ (by the first rule of exponents and Lemma 1.261).

1.9.3 The Newton binomial formula for arbitrary exponents

Theorem 1.264 Generalized Newton binomial formula

Assume that $K$ is a commutative $\mathbb {Q}$-algebra. Let $c\in K$. Then,

\[ \left( 1+x\right) ^{c}=\sum _{k\in \mathbb {N}}\binom {c}{k}x^{k}. \]

docs source

theorem AlgebraicCombinatorics.FPS.generalizedNewtonBinomial {K : Type u_1} [CommRing K] [Algebra ℚ K] [BinomialRing K] [CharZero K] (c : K) :

fpsPow (1 + PowerSeries.X) c = PowerSeries.binomialSeries K c

Proof ▶

The definition of $\operatorname {Log}$ yields $\operatorname {Log}(1+x) = \overline{\log }\circ x = \overline{\log }$. By Definition 1.258, we have

\begin{align*} (1+x)^c & = \operatorname {Exp}(c\operatorname {Log}(1+x)) = \operatorname {Exp}(c\, \overline{\log }) \\ & = \exp \circ (c\, \overline{\log }) = \sum _{m\in \mathbb {N}} \frac{1}{m!}\left(\sum _{n\geq 1}\frac{(-1)^{n-1}}{n}cx^n\right)^m. \end{align*}

Expanding and collecting by powers of $x$, we obtain

\[ (1+x)^c = \sum _{k\in \mathbb {N}} \left(\sum _{(n_1,\ldots ,n_m)\in \operatorname {Comp}(k)} \frac{1}{m!}\cdot \frac{(-1)^{n_1+\cdots +n_m-m}}{n_1 n_2\cdots n_m} c^m\right) x^k, \]

where $\operatorname {Comp}(k)$ denotes the set of all compositions of $k$.

It remains to show that the coefficient of $x^k$ equals $\binom {c}{k}$. We use the polynomial identity trick: for each $k\in \mathbb {N}$, both sides of the coefficient equality

\[ \sum _{(n_1,\ldots ,n_m)\in \operatorname {Comp}(k)} \frac{1}{m!}\cdot \frac{(-1)^{n_1+\cdots +n_m-m}}{n_1\cdots n_m} c^m = \binom {c}{k} \]

are polynomials in $c$ with rational coefficients. (The left-hand side is a finite sum of “rational number times a power of $c$” expressions. The right-hand side is $\frac{c(c-1)(c-2)\cdots (c-k+1)}{k!}$.)

For $c = n\in \mathbb {N}$, the equality holds by the standard Newton binomial formula (Theorem 1.119), since both sides equal $\binom {n}{k}$. Since two polynomials with rational coefficients that agree on all natural numbers must be equal (having infinitely many common values), the equality holds for all $c\in K$.

In the formal proof:

The base case $k=0$: both sides equal $1$.
The inductive case $k=k'+1$: both the LHS and the RHS are expressed as evaluations of explicit polynomials over $\mathbb {Q}$, mapped to $K$. The LHS polynomial is built by expanding $\exp \circ (c\, \overline{\log })$ as $\sum _{d\ge 0}\frac{1}{d!}(c\, \overline{\log })^d$; the scalar factoring $(c\, \overline{\log })^d = c^d\, \overline{\log }^d$ uses Lemma 1.275, and the truncation of the sum at $d=k$ uses the vanishing $[x^k](\overline{\log }^d)=0$ for $d{\gt}k$ (Lemma 1.276). The polynomial identity principle (Lemma 1.278) then shows these polynomials are equal, since they agree on all $n\in \mathbb {N}$.

Corollary 1.265

✓

For any $c\in K$ and $k\in \mathbb {N}$,

\[ [x^k](1+x)^c = \binom {c}{k}. \]

docs source

theorem AlgebraicCombinatorics.FPS.coeff_one_add_X_fpsPow {K : Type u_1} [CommRing K] [Algebra ℚ K] [BinomialRing K] [CharZero K] (c : K) (k : ℕ) :

(PowerSeries.coeff k) (fpsPow (1 + PowerSeries.X) c) = Ring.choose c k

Proof ▶

Immediate from Theorem 1.264 by reading off coefficients.

Theorem 1.266

✓

For any $n\in K$,

\[ (1+x)^{-n} = \sum _{i\in \mathbb {N}} (-1)^i \binom {n+i-1}{i} x^i. \]

docs source

theorem AlgebraicCombinatorics.FPS.antiNewtonBinomial {K : Type u_1} [CommRing K] [Algebra ℚ K] [BinomialRing K] [CharZero K] (n : K) :

fpsPow (1 + PowerSeries.X) (-n) = PowerSeries.mk fun (i : ℕ) => (-1) ^ i * Ring.choose (n + ↑i - 1) i

Proof ▶

Apply Theorem 1.264 with $c=-n$ and use the upper negation identity $\binom {-n}{i} = (-1)^i\binom {n+i-1}{i}$.

1.9.4 Further rules of exponents

Lemma 1.267

✓

For any $c\in K$, we have $1^c = 1$.

docs source

theorem AlgebraicCombinatorics.FPS.one_fpsPow {K : Type u_1} [CommRing K] [Algebra ℚ K] (c : K) :

fpsPow 1 c = 1

Proof ▶

$1^c = \operatorname {Exp}(c\cdot \operatorname {Log}1) = \operatorname {Exp}(c\cdot 0) = \operatorname {Exp}(0) = 1$.

Lemma 1.268

✓

For $f\in K[[x]]_1$ and $c\in K$, we have $[x^0](f^c) = 1$.

docs source

theorem AlgebraicCombinatorics.FPS.constantCoeff_fpsPow {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) (c : K) :

PowerSeries.constantCoeff (fpsPow f c) = 1

Proof ▶

Immediate from $f^c\in K[[x]]_1$.

Lemma 1.269

✓

For $f\in K'[[x]]_1$ (over a field $K'$) and $c\in K'$,

\[ f^{-c} = (f^c)^{-1}. \]

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_neg {K' : Type u_2} [Field K'] [Algebra ℚ K'] {f : PowerSeries K'} (hf : HasConstantTermOne f) (c : K') :

fpsPow f (-c) = (fpsPow f c)⁻¹

Proof ▶

We have $f^{-c}\cdot f^c = f^{-c+c} = f^0 = 1$, so $f^{-c}$ is the inverse of $f^c$.

Lemma 1.270

✓

For integer exponents, $f^c$ agrees with the standard power: for $n\ge 0$, $f^n = f^n$ (standard), and for $n{\lt}0$, $f^n = (f^{|n|})^{-1}$.

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_int {K' : Type u_2} [Field K'] [Algebra ℚ K'] {f : PowerSeries K'} (hf : HasConstantTermOne f) (n : ℤ) :

fpsPow f ↑n = if n ≥ 0 then f ^ n.toNat else (f ^ (-n).toNat)⁻¹

Proof ▶

For $n\ge 0$, use Lemma 1.263. For $n{\lt}0$, combine $f^{-c}\cdot f^c = 1$ with $f^{|n|}$ computed via the natural-number case.

1.9.5 Another application

Proposition 1.271

Let $n\in \mathbb {C}$ and $k\in \mathbb {N}$. Then,

\[ \sum _{i=0}^{k}\binom {n+i-1}{i}\binom {n}{k-2i}=\binom {n+k-1}{k}. \]

docs source

theorem AlgebraicCombinatorics.FPS.binomialIdentity {K : Type u_1} [CommRing K] [Algebra ℚ K] [BinomialRing K] [CharZero K] (n : K) (k : ℕ) :

∑ i ∈ Finset.range (k / 2 + 1), Ring.choose (n + ↑i - 1) i * Ring.choose n (k - 2 * i) = Ring.choose (n + ↑k - 1) k

Proof ▶

Define two FPSs $f,g\in \mathbb {C}\left[ \left[ x\right] \right] $ by

\begin{align*} f & =\sum _{i\in \mathbb {N}}\binom {n+i-1}{i}x^{2i}\\ \text{and}\ \ \ \ \ \ \ \ \ \ g & =\sum _{j\in \mathbb {N}}\binom {n}{j}x^{j}. \end{align*}

Multiplying and collecting by powers of $x$, we find that

\[ [x^k](fg) = \sum _{i=0}^{k} \binom {n+i-1}{i}\binom {n}{k-2i}, \]

which is the left-hand side of our identity.

For $g$, the generalized Newton formula (Theorem 1.264) gives $g=(1+x)^n$. For $f$, the anti-Newton binomial formula (Theorem 1.266) gives $(1+x)^{-n} = \sum _{i\in \mathbb {N}}(-1)^i\binom {n+i-1}{i}x^i$. Substituting $-x^2$ for $x$, we get $f = (1-x^2)^{-n}$.

Thus

\begin{align*} fg & = (1-x^2)^{-n}(1+x)^n \\ & = \left(\frac{1+x}{1-x^2}\right)^n = \left(\frac{1-x^2}{1+x}\right)^{-n} \\ & = (1-x)^{-n}. \end{align*}

Substituting $-x$ for $x$ in the anti-Newton formula gives

\[ (1-x)^{-n} = \sum _{i\in \mathbb {N}}\binom {n+i-1}{i}x^i. \]

Hence $[x^k](fg) = \binom {n+k-1}{k}$.

The formal proof establishes that $fg = (1-x)^{-n}$ by first showing $f = (1-x^2)^{-n}$. The identity $f = (1-x^2)^{-n}$ is proved by comparing coefficients using the polynomial identity principle: for natural $N$, both sides of the coefficient identity follow from the inverse of $(1-x^2)^N$ expressed via expansion of $(1-x)^{-N}$, and uniqueness of inverses gives agreement; the polynomial identity principle then extends the result to all $n\in K$. The odd-coefficient vanishing is established by a pairing argument: for odd $k$, each pair $(i,k-i)$ contributes terms with opposite signs (since $i$ and $k-i$ have opposite parities), giving a sum of $0$.

1.9.6 Helper lemmas from the formalization

Lemma 1.272

✓

Our $\overline{\log }$ series equals the logarithm series from Mathlib’s Exp/Log framework.

docs source

theorem AlgebraicCombinatorics.FPS.logSeries_eq_logbar {K : Type u_1} [CommRing K] [Algebra ℚ K] :

logSeries = PowerSeries.logbar K

Proof ▶

Coefficient comparison.

Lemma 1.273

✓

The definition of $\operatorname {Log}$ from Definition 1.250 is equivalent to the definition from Mathlib’s Exp/Log framework for FPS with constant term one.

docs source

theorem AlgebraicCombinatorics.FPS.fpsLog_eq_Log_val {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) :

fpsLog f = ↑(PowerSeries.Log ⟨f, hf⟩)

Proof ▶

Unfold definitions and use Lemma 1.272.

Lemma 1.274

✓

For $g$ with $[x^0]g=0$, the definition of $\operatorname {Exp}(g)$ from Definition 1.254 is equivalent to the definition from Mathlib’s Exp/Log framework for FPS with constant term zero.

docs source

theorem AlgebraicCombinatorics.FPS.fpsExp_eq_Exp_val {K : Type u_1} [CommRing K] [Algebra ℚ K] {g : PowerSeries K} (hg : PowerSeries.constantCoeff g = 0) :

fpsExp g = ↑(PowerSeries.Exp ⟨g, hg⟩)

Proof ▶

Unfold definitions.

Lemma 1.275

✓

$(c\cdot g)^m = c^m\cdot g^m$ for $c\in K$, $g\in K[[x]]$, $m\in \mathbb {N}$.

docs source

theorem AlgebraicCombinatorics.FPS.smul_pow_eq_pow_smul {K : Type u_1} [CommRing K] (c : K) (g : PowerSeries K) (m : ℕ) :

(c • g) ^ m = c ^ m • g ^ m

Proof ▶

Induction on $m$.

Lemma 1.276

✓

For $k {\lt} m$, we have $[x^k](\overline{\log }^m) = 0$ (since $\overline{\log }$ has order $\geq 1$, so $\overline{\log }^m$ has order $\geq m$).

docs source

theorem AlgebraicCombinatorics.FPS.coeff_logSeries_pow_eq_zero_of_gt {K : Type u_1} [CommRing K] [Algebra ℚ K] (k m : ℕ) (h : k < m) :

(PowerSeries.coeff k) (logSeries ^ m) = 0

Proof ▶

The order of $\overline{\log }^m$ is at least $m$ since $[x^0]\overline{\log }=0$.

Theorem 1.277

✓

Let $R$ be a commutative domain of characteristic $0$, and let $p\in R[x]$ be a polynomial such that $p(n)=0$ for all $n\in \mathbb {N}$. Then $p=0$.

docs source

theorem AlgebraicCombinatorics.FPS.polynomial_identity_trick {R : Type u_2} [CommRing R] [IsDomain R] [CharZero R] (p : Polynomial R) (h : ∀ (n : ℕ), Polynomial.eval (↑n) p = 0) :

p = 0

Proof ▶

The set of roots of $p$ contains all natural numbers, which is an infinite subset of $R$ (since $R$ has characteristic $0$). A nonzero polynomial of degree $d$ has at most $d$ roots, so $p$ must be zero.

Lemma 1.278

If two polynomials over $\mathbb {Q}$ agree when evaluated at all natural numbers (after mapping to $K$ via the algebra map), then they are equal: if $p(n) = q(n)$ for all $n\in \mathbb {N}$, then $p = q$.

docs source

theorem AlgebraicCombinatorics.FPS.poly_eq_of_nat_eval_eq {K : Type u_1} [CommRing K] [Algebra ℚ K] [CharZero K] (p q : Polynomial ℚ) (h : ∀ (n : ℕ), Polynomial.eval (↑n) (Polynomial.map (algebraMap ℚ K) p) = Polynomial.eval (↑n) (Polynomial.map (algebraMap ℚ K) q)) :

p = q

Proof ▶

Apply the polynomial identity trick to $p - q$.

Lemma 1.279

Pascal’s rule for generalized binomial coefficients:

\[ \binom {c}{k+1} = \binom {c-1}{k} + \binom {c-1}{k+1}. \]

docs source

theorem AlgebraicCombinatorics.FPS.Ring_choose_pascal {K : Type u_1} [CommRing K] [BinomialRing K] (c : K) (k : ℕ) :

Ring.choose c (k + 1) = Ring.choose (c - 1) k + Ring.choose (c - 1) (k + 1)

Proof ▶

Follows from the Pascal recurrence for generalized binomial coefficients.

Lemma 1.280

The coefficients of $(1+x)^c$ satisfy Pascal’s recurrence:

\[ [x^{k+1}](1+x)^c = [x^k](1+x)^{c-1} + [x^{k+1}](1+x)^{c-1}. \]

docs source

theorem AlgebraicCombinatorics.FPS.fpsPow_coeff_pascal {K : Type u_1} [CommRing K] [Algebra ℚ K] (c : K) (k : ℕ) :

(PowerSeries.coeff (k + 1)) (fpsPow (1 + PowerSeries.X) c) = (PowerSeries.coeff k) (fpsPow (1 + PowerSeries.X) (c - 1)) + (PowerSeries.coeff (k + 1)) (fpsPow (1 + PowerSeries.X) (c - 1))

Proof ▶

Since $(1+x)^{c} = (1+x)^{c-1}\cdot (1+x)$, the coefficient $[x^{k+1}]$ of the product is $[x^k](1+x)^{c-1} + [x^{k+1}](1+x)^{c-1}$.

1.9.7 Helpers for Theorem 1.264

The generalized Newton binomial formula requires showing that both the LHS (coefficients of $(1+x)^c$) and the RHS ($\binom {c}{k}$) are polynomial functions of $c$ that agree on all natural numbers.

Lemma 1.281

The generalized binomial coefficient $\binom {c}{k}$ equals the evaluation of a polynomial in $c$: there exists a polynomial $p_k\in \mathbb {Q}[x]$ such that $\binom {c}{k} = p_k(c)$ for all $c\in K$.

docs source

theorem AlgebraicCombinatorics.FPS.Ring_choose_eq_choosePoly_eval {K : Type u_1} [CommRing K] [Algebra ℚ K] [BinomialRing K] [CharZero K] (k : ℕ) (c : K) :

Ring.choose c k = Polynomial.eval c (Polynomial.map (algebraMap ℚ K) (AlgebraicCombinatorics.FPS.choosePoly✝ k))

Proof ▶

The polynomial is $p_k(x) = x(x-1)\cdots (x-k+1)/k!$, evaluated at $c$ via the algebra map $\mathbb {Q} \to K$.

Lemma 1.282

The coefficient $[x^k](1+x)^c$ equals the evaluation of a polynomial in $c$:

\[ [x^k](1+x)^c = q_k(c) \]

for some $q_k\in \mathbb {Q}[x]$.

docs source

theorem AlgebraicCombinatorics.FPS.coeff_fpsPow_eq_coeffExpPoly_eval {K : Type u_1} [CommRing K] [Algebra ℚ K] (k : ℕ) (c : K) :

(PowerSeries.coeff k) (PowerSeries.subst (c • logSeries) (PowerSeries.exp K)) = Polynomial.eval c (Polynomial.map (algebraMap ℚ K) (AlgebraicCombinatorics.FPS.coeffExpPoly✝ k))

Proof ▶

Expand $(1+x)^c = \operatorname {Exp}(c\cdot \overline{\log }) = \sum _{d\ge 0}\frac{1}{d!}(c\, \overline{\log })^d$. Using $(c\, \overline{\log })^d = c^d\, \overline{\log }^d$ and the vanishing $[x^k](\overline{\log }^d)=0$ for $d{\gt}k$, the coefficient $[x^k]$ is a polynomial in $c$ of degree $\leq k$.

Lemma 1.283

✓

For $n\in K$ and $k\in \mathbb {N}$,

\[ [x^k](1-x)^{-n} = \binom {n+k-1}{k}. \]

docs source

theorem AlgebraicCombinatorics.FPS.one_sub_X_pow_neg_coeff {K : Type u_1} [CommRing K] [BinomialRing K] (n : K) (k : ℕ) :

(PowerSeries.coeff k) ((PowerSeries.rescale (-1)) (PowerSeries.binomialSeries K (-n))) = Ring.choose (n + ↑k - 1) k

Proof ▶

Use the upper negation identity $\binom {-n}{k} = (-1)^k\binom {n+k-1}{k}$ and the sign cancellation $(-1)^k\cdot (-1)^k = 1$.

1.9.8 Helpers for Proposition 1.271

The proof of the binomial identity requires establishing that the product $f\cdot g$ (where $f = (1-x^2)^{-n}$ and $g = (1+x)^n$) equals $(1-x)^{-n}$. This is done in several steps:

Define $f = \sum _{i\in \mathbb {N}} \binom {n+i-1}{i} x^{2i}$ and $g = \sum _{j\in \mathbb {N}} \binom {n}{j} x^j$.
Show $fg = (1-x)^{-n}$ (Lemma 1.290).
Read off coefficients.

Definition 1.284

✓

Define two FPSs for the binomial identity:

\begin{align*} f(n) & := \sum _{i\in \mathbb {N}} \binom {n+i-1}{i} x^{2i} \quad \text{(i.e., the even-indexed coefficients of $(1-x^2)^{-n}$)}, \\ g(n) & := \sum _{j\in \mathbb {N}} \binom {n}{j} x^j = (1+x)^n. \end{align*}

docs source

noncomputable def AlgebraicCombinatorics.FPS.f_series' {K : Type u_1} [CommRing K] [BinomialRing K] (n : K) :

PowerSeries K

AlgebraicCombinatorics.FPS.f_series' n = PowerSeries.mk fun (m : ℕ) => if Even m then Ring.choose (n + ↑(m / 2) - 1) (m / 2) else 0

docs source

noncomputable def AlgebraicCombinatorics.FPS.g_series' {K : Type u_1} [CommRing K] [BinomialRing K] (n : K) :

PowerSeries K

AlgebraicCombinatorics.FPS.g_series' n = PowerSeries.binomialSeries K n

Lemma 1.285

The coefficient of $x^k$ in $f(n)\cdot g(n)$ equals

\[ [x^k](f\cdot g) = \sum _{i=0}^{\lfloor k/2\rfloor } \binom {n+i-1}{i}\binom {n}{k-2i}. \]

docs source

theorem AlgebraicCombinatorics.FPS.coeff_f_mul_g' {K : Type u_1} [CommRing K] [BinomialRing K] (n : K) (k : ℕ) :

(PowerSeries.coeff k) (f_series' n * g_series' n) = ∑ i ∈ Finset.range (k / 2 + 1), Ring.choose (n + ↑i - 1) i * Ring.choose n (k - 2 * i)

Proof ▶

By expanding the Cauchy product and using the fact that $f$ has nonzero coefficients only at even positions.

Lemma 1.286

For natural $N$,

\[ (1-x)^{-N}\cdot (1+x)^{-N}\cdot (1-x^2)^N = 1. \]

That is, $(1-x)^{-N}\cdot (1+x)^{-N}$ is the inverse of $(1-x^2)^N$.

docs source

theorem AlgebraicCombinatorics.FPS.invOneSubPow_mul_rescale_mul_one_sub_sq_pow' {K : Type u_1} [CommRing K] (N : ℕ) :

↑(PowerSeries.invOneSubPow K N) * (PowerSeries.rescale (-1)) ↑(PowerSeries.invOneSubPow K N) * (1 - PowerSeries.X ^ 2) ^ N = 1

Proof ▶

Factor $(1-x^2)^N = (1-x)^N(1+x)^N$ and use the inverse relations $(1-x)^{-N}\cdot (1-x)^N = 1$ and $(1+x)^{-N}\cdot (1+x)^N = 1$.

Lemma 1.287

For natural $N$, $(1-x)^{-N}\big|_{x \mapsto x^2}\cdot (1-x^2)^N = 1$. That is, $(1-x)^{-N}\big|_{x \mapsto x^2}$ is also the inverse of $(1-x^2)^N$.

docs source

theorem AlgebraicCombinatorics.FPS.expand_invOneSubPow_eq_inv_one_sub_X_sq {K : Type u_1} [CommRing K] (N : ℕ) :

(PowerSeries.expand 2 ⋯) ↑(PowerSeries.invOneSubPow K N) * (1 - PowerSeries.X ^ 2) ^ N = 1

Proof ▶

Since the substitution $x \mapsto x^2$ is a ring homomorphism and $(1-x)\big|_{x \mapsto x^2} = 1-x^2$, we have $(1-x)^{-N}\big|_{x \mapsto x^2}\cdot (1-x)^N\big|_{x \mapsto x^2} = 1\big|_{x \mapsto x^2} = 1$.

Lemma 1.288

For natural $N$,

\[ (1-x)^{-N}\cdot (1+x)^{-N} = (1-x)^{-N}\big|_{x \mapsto x^2}. \]

Both sides are inverses of $(1-x^2)^N$, so they are equal by uniqueness of inverses.

docs source

theorem AlgebraicCombinatorics.FPS.product_eq_expand_invOneSubPow {K : Type u_1} [CommRing K] (N : ℕ) :

↑(PowerSeries.invOneSubPow K N) * (PowerSeries.rescale (-1)) ↑(PowerSeries.invOneSubPow K N) = (PowerSeries.expand 2 ⋯) ↑(PowerSeries.invOneSubPow K N)

Proof ▶

Both $P := (1-x)^{-N}\cdot (1+x)^{-N}$ and $E := (1-x)^{-N}\big|_{x \mapsto x^2}$ satisfy $(\cdot )\cdot (1-x^2)^N = 1$. Since $(1-x^2)^N$ is a unit, $P = E$.

Lemma 1.289

For natural $N\ge 1$ and $m\in \mathbb {N}$,

\[ [x^{2m}]\bigl((1-x)^{-N}\cdot (1+x)^{-N}\bigr) = \binom {N+m-1}{m}. \]

docs source

theorem AlgebraicCombinatorics.FPS.coeff_invOneSubPow_product_even' {K : Type u_1} [CommRing K] (N m : ℕ) (hN : 0 < N) :

(PowerSeries.coeff (m + m)) (↑(PowerSeries.invOneSubPow K N) * (PowerSeries.rescale (-1)) ↑(PowerSeries.invOneSubPow K N)) = ↑((N + m - 1).choose m)

Proof ▶

By Lemma 1.288, the product equals $(1-x)^{-N}\big|_{x \mapsto x^2}$, so the coefficient at $2m$ is $[x^m](1-x)^{-N} = \binom {N+m-1}{m}$.

Lemma 1.290 Key product identity

For all $n\in K$,

\[ f(n)\cdot g(n) = (1-x)^{-n}. \]

In other words, $(1-x^2)^{-n}\cdot (1+x)^n = (1-x)^{-n}$.

docs source

theorem AlgebraicCombinatorics.FPS.key_product_identity' {K : Type u_1} [CommRing K] [Algebra ℚ K] [BinomialRing K] [CharZero K] (n : K) :

f_series' n * g_series' n = (PowerSeries.rescale (-1)) (PowerSeries.binomialSeries K (-n))

Proof ▶

First show $f(n) = (1-x^2)^{-n}$ by establishing that $f(n)$ equals $(1+x)^{-n} \cdot (1-x)^{-n}$. The even-coefficient identity uses Lemma 1.289 for natural $N$ and then extends to all $n$ by the polynomial identity principle (Theorem 1.277). The odd-coefficient vanishing follows from a pairing argument: for odd $k$, each pair $(i,k-i)$ contributes terms with opposite signs. Then $f(n)\cdot g(n) = (1-x^2)^{-n}\cdot (1+x)^n$, and the cancellation $(1+x)^{-n}\cdot (1+x)^n = 1$ gives the result.