Non-integer Powers of Formal Power Series

This file formalizes non-integer powers of formal power series (FPS) and the generalized Newton binomial formula, following Section 7.12 (sec.gf.nips) of the source.

Main Definitions

• AlgebraicCombinatorics.FPS.fpsPow: The c-th power f^c for f ∈ K⟦X⟧₁ (FPS with constant term 1) and c ∈ K, defined as Exp(c * Log f) (Definition def.fps.power-c).

Main Results

• AlgebraicCombinatorics.FPS.fpsPow_add: The rule f^{a+b} = f^a * f^b (Theorem thm.fps.power-c.rules).
• AlgebraicCombinatorics.FPS.fpsPow_mul: The rule (fg)^a = f^a * g^a (Theorem thm.fps.power-c.rules).
• AlgebraicCombinatorics.FPS.fpsPow_pow: The rule (f^a)^b = f^{ab} (Theorem thm.fps.power-c.rules).
• AlgebraicCombinatorics.FPS.generalizedNewtonBinomial: The generalized Newton binomial formula (1+x)^c = ∑_{k ∈ ℕ} C(c,k) x^k (Theorem thm.fps.gen-newton).
• AlgebraicCombinatorics.FPS.binomialIdentity: The binomial identity ∑_{i=0}^k C(n+i-1,i) C(n,k-2i) = C(n+k-1,k) (Proposition prop.binom.nCk-2i-qedmo.CN).

Implementation Notes

The definition of f^c uses the Exp and Log maps from Mathlib. Specifically:

• For f ∈ K⟦X⟧₁ (constant term 1), we define f^c := Exp(c * Log f)
• This requires K to be a commutative ℚ-algebra

The generalized Newton binomial formula is proved using the polynomial identity trick: both sides are polynomials in c that agree on ℕ, hence they agree everywhere.

References

• Source: NonIntegerPowers.tex, Section sec.gf.nips

The Exp and Log Maps

We use Mathlib's PowerSeries.exp for the exponential series. For the logarithm, we define it via the standard series log(1+x) = ∑_{n≥1} (-1)^{n-1}/n * x^n.

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

The logarithm series: log(1+x) = x - x²/2 + x³/3 - x⁴/4 + ... This is \overline{log} in the source notation. Label: def.fps.logbar

Equations

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

theorem AlgebraicCombinatorics.FPS.coeff_logSeries {K : Type u_1} [CommRing K] [Algebra ℚ K] (n : ℕ) : (PowerSeries.coeff n) logSeries = if n = 0 then 0 else (algebraMap ℚ K) ((-1) ^ (n - 1) / ↑n)

Coefficient of the log series at position n. For n ≥ 1: [x^n] log(1+x) = (-1)^{n-1}/n

@[simp]

theorem AlgebraicCombinatorics.FPS.constantCoeff_logSeries {K : Type u_1} [CommRing K] [Algebra ℚ K] : PowerSeries.constantCoeff logSeries = 0

The constant term of the log series is 0

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

Key lemma: coeff k (logSeries^m) = 0 for m > k. This follows from logSeries having constant term 0.

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

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

theorem AlgebraicCombinatorics.FPS.coeff_smul_pow {K : Type u_1} [CommRing K] (c : K) (g : PowerSeries K) (k m : ℕ) : (PowerSeries.coeff k) ((c • g) ^ m) = c ^ m • (PowerSeries.coeff k) (g ^ m)

Helper: coeff k ((c • g)^m) = c^m • coeff k (g^m)

FPS with Constant Term 1

We define the set K⟦X⟧₁ of FPS with constant term 1. This is the domain on which non-integer powers are defined.

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

An FPS has constant term 1. This is the condition for f ∈ K⟦X⟧₁ in the source. Label: def.fps.Exp-Log-maps (b)

Note: This is definitionally equivalent to membership in PowerSeries₁ from ExpLog.lean: HasConstantTermOne f ↔ f ∈ PowerSeries₁. The Prop form is used here for convenience in hypotheses, while PowerSeries₁ (a Set) is used in ExpLog.lean for subgroup structures.

Equations

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

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_iff_mem_PowerSeries₁ {R : Type u_2} [CommRing R] {f : PowerSeries R} : HasConstantTermOne f ↔ f ∈ PowerSeries.PowerSeries₁

HasConstantTermOne f is equivalent to membership in PowerSeries₁. This bridges the two representations of "constant term equals 1".

theorem AlgebraicCombinatorics.FPS.HasConstantTermOne.mem_PowerSeries₁ {R : Type u_2} [CommRing R] {f : PowerSeries R} (hf : HasConstantTermOne f) : f ∈ PowerSeries.PowerSeries₁

Alias for hasConstantTermOne_iff_mem_PowerSeries₁.mp.

theorem AlgebraicCombinatorics.FPS.mem_PowerSeries₁.hasConstantTermOne {R : Type u_2} [CommRing R] {f : PowerSeries R} (hf : f ∈ PowerSeries.PowerSeries₁) : HasConstantTermOne f

Alias for hasConstantTermOne_iff_mem_PowerSeries₁.mpr.

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_one' {R : Type u_2} [CommRing R] : HasConstantTermOne 1

The set of FPS with constant term 1 forms a submonoid under multiplication

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_mul' {R : Type u_2} [CommRing R] {f g : PowerSeries R} (hf : HasConstantTermOne f) (hg : HasConstantTermOne g) : HasConstantTermOne (f * g)

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_one_add_X' {R : Type u_2} [CommRing R] : HasConstantTermOne (1 + PowerSeries.X)

1 + x has constant term 1

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_of_constantCoeff_zero' {R : Type u_2} [CommRing R] {g : PowerSeries R} (hg : PowerSeries.constantCoeff g = 0) : HasConstantTermOne (1 + g)

Any FPS of the form 1 + g where g has constant term 0 has constant term 1

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_one {K : Type u_1} [CommRing K] : HasConstantTermOne 1

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

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_one_add_X {K : Type u_1} [CommRing K] : HasConstantTermOne (1 + PowerSeries.X)

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_of_constantCoeff_zero {K : Type u_1} [CommRing K] {g : PowerSeries K} (hg : PowerSeries.constantCoeff g = 0) : HasConstantTermOne (1 + g)

The Log Map for FPS with Constant Term 1

For f ∈ K⟦X⟧₁, we define Log(f) by substituting (f-1) into the log series. Since f has constant term 1, f-1 has constant term 0, so the substitution is well-defined.

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

The Log map: Log(f) = log_series(f-1) = logSeries.subst (f-1) This is well-defined when f has constant term 1. Label: def.fps.Exp-Log-maps

Equations

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

@[simp]

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

Log(1) = 0

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

The constant term of Log(f) is 0 when f has constant term 1

The Exp Map for FPS with Constant Term 0

For g ∈ K⟦X⟧₀ (constant term 0), we define Exp(g) by substituting g into exp.

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

The Exp map: Exp(g) = exp(g) = (exp K).subst g This is well-defined when g has constant term 0. Label: def.fps.Exp-Log-maps

Equations

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

@[simp]

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

Exp(0) = 1

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

Exp(g) has constant term 1 when g has constant term 0

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

The exponential functional equation: Exp(x + y) = Exp(x) * Exp(y) This is a fundamental property of the exponential series. For power series x, y with constant term 0: exp(x + y) = exp(x) * exp(y) Label: (exp functional equation)

Proof strategy (from the textbook): Both sides satisfy the same differential equation with the same initial condition. Let F(x,y) = exp(x+y) and G(x,y) = exp(x) * exp(y).

• ∂F/∂x = exp(x+y) = F and ∂F/∂y = exp(x+y) = F
• ∂G/∂x = exp(x) * exp(y) = G and ∂G/∂y = exp(x) * exp(y) = G
• F(0,0) = exp(0) = 1 and G(0,0) = exp(0) * exp(0) = 1 By uniqueness of solutions to the ODE, F = G.

Alternative proof (coefficient comparison): Use the Cauchy product formula and the fact that x^n = ∑_{k=0}^n [x^k](exp x) * [x^{n-k}](exp y) * C(n,k) which equals [x^n](exp x * exp y) by the binomial theorem.

Mathlib note: Mathlib's exp_mul_exp_eq_exp_add proves this for the special case where x = a • X and y = b • X (i.e., rescaling). The general case requires the derivative characterization or coefficient comparison.

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

The logarithm product rule: Log(f * g) = Log(f) + Log(g) This is a fundamental property of the logarithm series. For power series f, g with constant term 1: log(f * g) = log(f) + log(g) Label: (log product rule)

Proof strategy (from the textbook): Use the derivative characterization. Let h = log(fg) - log(f) - log(g). Then h' = (fg)'/(fg) - f'/f - g'/g = (f'g + fg')/(fg) - f'/f - g'/g = 0. Since h(0) = 0 and h' = 0, we have h = 0.

Alternative proof: Use the inverse property: if Exp and Log are inverses, then Log(fg) = Log(Exp(Log f) * Exp(Log g)) = Log(Exp(Log f + Log g)) = Log f + Log g.

Dependency: This proof requires either the derivative characterization or the inverse property Exp_Log_inverse from ExpLog.lean.

Definition of Non-integer Powers (Definition def.fps.power-c)

For f ∈ K⟦X⟧₁ and c ∈ K, we define f^c := Exp(c * Log(f)).

This definition:

• Does not conflict with integer powers (since Log and Exp are inverses on the appropriate domains)
• Makes the rules of exponents hold
• Yields (1+x)^c = ∑ C(c,k) x^k (generalized Newton binomial formula)

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

The c-th power of an FPS f with constant term 1. f^c := Exp(c * Log(f)) = exp.subst (c * log_series.subst (f-1)) Label: def.fps.power-c

Equations

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

def AlgebraicCombinatorics.FPS.«term_^ᶠ_» : Lean.TrailingParserDescr

Notation for non-integer powers (when needed)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

f^0 = 1 for any f with constant term 1

@[simp]

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

1^c = 1 for any c

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)

f^c has constant term 1 when f has constant term 1

Rules of Exponents (Theorem thm.fps.power-c.rules)

For any a, b ∈ K and f, g ∈ K⟦X⟧₁:

• f^{a+b} = f^a * f^b
• (fg)^a = f^a * g^a
• (f^a)^b = f^{ab}

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

Rule of exponents: f^{a+b} = f^a * f^b Label: eq.sec.gf.nips.rules-of-exps (first rule)

Proof: f^{a+b} = Exp((a+b) • Log f) = Exp(a • Log f + b • Log f) [by smul_add] = Exp(a • Log f) * Exp(b • Log f) [by fpsExp_add] = f^a * f^b

Dependency: Requires fpsExp_add.

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

Rule of exponents: (fg)^a = f^a * g^a Label: eq.sec.gf.nips.rules-of-exps (second rule)

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)

Rule of exponents: (f^a)^b = f^{ab} Label: eq.sec.gf.nips.rules-of-exps (third rule)

Proof strategy: (f^a)^b = Exp(b • Log(f^a)) = Exp(b • Log(Exp(a • Log f))) = Exp(b • (a • Log f)) [by fpsLog_fpsExp: Log(Exp g) = g] = Exp((b * a) • Log f) [by smul_smul] = Exp((a * b) • Log f) [by mul_comm] = f^{ab}

Dependency: Requires the inverse property fpsLog (fpsExp g) = g for g with constant term 0. This is proved in ExpLog.lean as Log_Exp.

Connection to ExpLog.lean

We establish the connection between our logSeries/fpsLog/fpsExp definitions and the logbar/Log/Exp definitions from ExpLog.lean. This allows us to use the Exp_Log theorem to prove fpsPow_one.

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

Our logSeries equals PowerSeries.logbar from ExpLog.lean

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⟩)

fpsLog f equals (Log f).val when f has constant term 1

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⟩)

fpsExp g equals (Exp g').val when g has constant term 0

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

f^1 = f for any f with constant term 1. This follows from the Exp-Log inverse property: Exp(Log(f)) = f. Label: (implicit in def.fps.power-c consistency)

@[simp]

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

The constant term of f^c is 1 when f has constant term 1. This is a simp-friendly version of hasConstantTermOne_fpsPow. Label: def.fps.power-c (property)

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)⁻¹

f^(-c) = (f^c)⁻¹ for f with constant term 1 (over a field). This extends the rules of exponents to negative powers. Label: def.fps.power-c (negative power property)

theorem AlgebraicCombinatorics.FPS.fpsPow_sub {K' : Type u_2} [Field K'] [Algebra ℚ K'] {f : PowerSeries K'} (hf : HasConstantTermOne f) (a b : K') : fpsPow f (a - b) = fpsPow f a * (fpsPow f b)⁻¹

f^(a-b) = f^a / f^b for f with constant term 1 (over a field). This extends the rules of exponents to subtraction. Label: def.fps.power-c (subtraction rule)

theorem AlgebraicCombinatorics.FPS.fpsPow_two_mul {K : Type u_1} [CommRing K] [Algebra ℚ K] {f : PowerSeries K} (hf : HasConstantTermOne f) (c : K) : fpsPow f (2 * c) = fpsPow f c ^ 2

f^(2*c) = (f^c)^2 for f with constant term 1. A useful special case of fpsPow_pow. Label: def.fps.power-c (doubling rule)

Generalized Newton Binomial Formula (Theorem thm.fps.gen-newton)

For any c ∈ K (where K is a commutative ℚ-algebra): (1+x)^c = ∑_{k ∈ ℕ} C(c,k) x^k

where C(c,k) = c(c-1)(c-2)⋯(c-k+1)/k! is the generalized binomial coefficient.

Note: We need K to be a BinomialRing to use Ring.choose. Since K is a ℚ-algebra, it has a BinomialRing structure.

Key lemmas for the proof

The proof strategy is:

1. Show that fpsLog (1+X) = logSeries
2. Show that fpsPow (1+X) c = fpsExp (c • logSeries)
3. Show that for natural n, fpsExp (n • logSeries) = (1+X)^n using the exp functional equation
4. Use binomialSeries_nat: binomialSeries K n = (1+X)^n
5. Apply the polynomial identity trick: both sides have polynomial coefficients in c that agree on all natural numbers, hence they agree everywhere

Helper lemmas for the polynomial identity principle

The proof of generalizedNewtonBinomial uses the polynomial identity principle: both Ring.choose c k and coeff k ((1+X)^ᶠ c) are polynomial functions of c that agree on all natural numbers, hence they are equal.

The following lemmas establish the polynomial structure of Ring.choose c k.

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))

coeffExpPoly k evaluated at c equals coeff k (fpsExp (c • logSeries)). This is the key lemma showing the LHS coefficient is a polynomial function.

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))

Ring.choose c k equals the evaluation of choosePoly.map at c. This is the key lemma showing Ring.choose is a polynomial function.

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

Key: if two polynomial evaluations agree on all naturals, the polynomials are equal

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)

Pascal identity for Ring.choose: C(c, k+1) = C(c-1, k) + C(c-1, k+1)

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))

Pascal identity for fpsPow coefficients: coeff (k+1) ((1+X)^c) = coeff k ((1+X)^(c-1)) + coeff (k+1) ((1+X)^(c-1))

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

The generalized Newton binomial formula: (1+x)^c = ∑_{k ∈ ℕ} C(c,k) x^k

This extends the standard Newton binomial formula (Theorem thm.fps.newton-binom) from natural number exponents to arbitrary exponents in a ℚ-algebra.

The proof uses the polynomial identity trick: both sides of the coefficient equality are polynomials in c that agree on ℕ (by the standard Newton formula), hence they agree everywhere.

Proof outline: For each coefficient k, we need to show coeff k ((1+X)^c) = Ring.choose c k.

1. Both sides are polynomial functions of c with rational coefficients:

   • Ring.choose c k = descPochhammer(c, k) / k! is a polynomial of degree k
   • coeff k (fpsExp (c • logSeries)) is also a polynomial in c (by expanding the exponential series and collecting terms)

2. For natural c = n, both sides equal Nat.choose n k:

   • Ring.choose n k = Nat.choose n k by Ring.choose_natCast
   • coeff k ((1+X)^n) = Nat.choose n k by the standard binomial theorem

3. By the polynomial identity trick: two polynomials (over ℚ) that agree on all natural numbers must be equal. Hence the coefficients agree for all c ∈ K.

Label: thm.fps.gen-newton

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

Corollary: coefficient of x^k in (1+x)^c is C(c,k) Label: thm.fps.gen-newton (coefficient form)

Application: The Catalan Number Generating Function

The equation C = 1 + xC² for the Catalan generating function has solution C = (1 - √(1-4x))/(2x) = (1 - (1-4x)^{1/2})/(2x)

This is now rigorous using our definition of non-integer powers.

noncomputable def AlgebraicCombinatorics.FPS.sqrtOneMinusFourX : PowerSeries ℚ

The square root of 1-4x as an FPS. √(1-4x) = (1-4x)^{1/2} = (1 + (-4x))^{1/2} Label: eq.sec.gf.exas.2.(1+x)1/2

Equations

• AlgebraicCombinatorics.FPS.sqrtOneMinusFourX = AlgebraicCombinatorics.FPS.fpsPow (1 + -4 • PowerSeries.X) (1 / 2)

theorem AlgebraicCombinatorics.FPS.hasConstantTermOne_oneMinusFourX : HasConstantTermOne (1 + -4 • PowerSeries.X)

1-4x has constant term 1, so its square root is well-defined

theorem AlgebraicCombinatorics.FPS.coeff_sqrtOneMinusFourX (k : ℕ) : (PowerSeries.coeff k) sqrtOneMinusFourX = Ring.choose (1 / 2) k * (-4) ^ k

The coefficient of x^k in √(1-4x) is C(1/2, k) * (-4)^k

Another Application: A Binomial Identity (Proposition prop.binom.nCk-2i-qedmo.CN)

For n ∈ ℂ and k ∈ ℕ: ∑_{i=0}^k C(n+i-1, i) C(n, k-2i) = C(n+k-1, k)

The proof uses generating functions:

• Define f = ∑_{i ∈ ℕ} C(n+i-1, i) x^{2i} = (1-x²)^{-n}
• Define g = ∑_{j ∈ ℕ} C(n, j) x^j = (1+x)^n
• Then fg = (1-x)^{-n} = ∑_{i ∈ ℕ} C(n+i-1, i) x^i
• Comparing coefficients of x^k gives the identity

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

The anti-Newton binomial formula: (1+x)^{-n} = ∑_{i ∈ ℕ} (-1)^i C(n+i-1, i) x^i This is a consequence of the generalized Newton formula. Label: prop.fps.anti-newton-binom

Helper Lemmas for the Binomial Identity

We prove the identity using generating functions:

• Define f = ∑_{i ∈ ℕ} C(n+i-1, i) x^{2i}
• Define g = ∑_{j ∈ ℕ} C(n, j) x^j = (1+x)^n
• Show that fg = (1-x)^{-n} using the factorization (1-x²) = (1-x)(1+x)
• Compare coefficients of x^k

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

(1-x)^{-n} has coefficient C(n+k-1, k) at position k. This is rescale (-1) applied to (1+x)^{-n}.

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

The series f = ∑_i C(n+i-1, i) x^{2i} used in the proof

Equations

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

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

The series g = (1+x)^n = binomialSeries K n

Equations

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

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)

The coefficient of x^k in f * g equals the LHS of the binomial identity

Infrastructure for the Polynomial Identity Principle

The following lemmas establish the connection between binomialSeries and invOneSubPow, which is needed for proving the coefficient identity using the polynomial identity principle.

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

The product (invOneSubPow K N).val * rescale (-1) (invOneSubPow K N).val times (1 - X²)^N equals 1. This shows the product is the inverse of (1 - X²)^N.

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

expand 2 (invOneSubPow K N).val = (1 - X²)^{-N}, i.e., the inverse of (1 - X²)^N. This follows from expand 2 being a ring homomorphism that maps (1 - X) to (1 - X²).

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)

The product (invOneSubPow K N).val * rescale (-1) (invOneSubPow K N).val equals expand 2 (invOneSubPow K N).val.

Both are inverses of (1 - X²)^N:

• The product: by invOneSubPow_mul_rescale_mul_one_sub_sq_pow'
• The expand: by expand_invOneSubPow_eq_inv_one_sub_X_sq

Since the inverse is unique (when it exists), they must be equal.

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)

For natural N ≥ 1, the coefficient of X^{2m} in the product (invOneSubPow K N).val * rescale (-1) (invOneSubPow K N).val is Nat.choose (N+m-1) m. This follows from the product being (1-X²)^{-N}.

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))

The key product identity: f * g = (1-x)^{-n}

This is the algebraic identity (1-x²)^{-n} * (1+x)^n = (1-x)^{-n}. The proof uses the factorization (1-x²) = (1-x)(1+x): (1-x²)^{-n} * (1+x)^n = (1-x)^{-n} * (1+x)^{-n} * (1+x)^n = (1-x)^{-n}

Note: This requires showing that f_series' n represents (1-x²)^{-n}, which follows from the anti-Newton binomial formula with the substitution x → -x².

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

The binomial identity: ∑_{i=0}^{⌊k/2⌋} C(n+i-1, i) C(n, k-2i) = C(n+k-1, k)

This is proved using generating functions and the generalized Newton formula. Note: The sum is restricted to i ≤ k/2 (equivalently, 2i ≤ k) because when 2i > k, the binomial coefficient C(n, k-2i) should be 0 (as k-2i would be negative). Using ℕ subtraction directly would incorrectly give C(n, 0) = 1 for those terms. Label: prop.binom.nCk-2i-qedmo.CN

Consistency with Integer Powers

Our definition of f^c agrees with the standard definition when c is a natural number.

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

For natural number exponents, fpsPow agrees with the standard power. This shows our definition is consistent with integer powers. Label: (consistency claim after def.fps.power-c)

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)⁻¹

For integer exponents, fpsPow agrees with the standard power (when f is invertible). For negative integers, this requires f to be invertible (which holds when constantCoeff f ≠ 0). Label: (consistency claim after def.fps.power-c)

The Proof Method: Polynomial Identity Trick

The proof of the generalized Newton formula uses the "polynomial identity trick": If two polynomials (with rational coefficients) agree on all natural numbers, they must be equal as polynomials, and hence agree on all values in any ℚ-algebra.

This is formalized in Mathlib as polynomial equality from infinitely many roots.

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

The polynomial identity trick: If a polynomial has infinitely many roots, it is zero. This is the key lemma used in the proof of the generalized Newton formula.

Note: This requires CharZero R to ensure that the natural numbers are distinct when coerced to R. Without this assumption, the theorem is false: for example, in ZMod 2, the polynomial x(x-1) evaluates to 0 at all natural numbers but is nonzero.

Label: (polynomial identity trick in proof of thm.fps.gen-newton)