Multivariate Formal Power Series

This file formalizes the material from Section sec.gf.multivar on multivariate formal power series (FPSs).

Main Content

Multivariate FPSs are FPSs in several variables. Their theory is mostly analogous to the theory of univariate FPSs, but requires more subscripts. In Mathlib, multivariate formal power series are defined as MvPowerSeries σ R := (σ →₀ ℕ) → R, where σ is the index set of variables.

Key concepts from the source:

• Bivariate FPSs: FPSs in two variables x and y have the form ∑_{i,j∈ℕ} a_{i,j} x^i y^j. In Mathlib, this is MvPowerSeries (Fin 2) R.

• Multiplication: For any two FPSs a and b and any n ∈ ℕ^k: [x^n](ab) = ∑_{i+j=n} [x^i]a · [x^j]b This is already captured by MvPowerSeries.coeff_mul.

• Indeterminates: The indeterminate x_i is defined as the family with a single 1 at position (0,...,0,1,0,...,0) (with 1 in the i-th position). This is MvPowerSeries.X i in Mathlib.

• Partial derivatives: Instead of one derivative, there are k partial derivatives (one for each variable).

Main Results

• embedUnivInBiv: Embedding of sequences of univariate power series into bivariate power series
• eq_of_embedUnivInBiv_eq: Proposition prop.fps.mulvar.comp-y-coeff - if ∑_k f_k y^k = ∑_k g_k y^k in K[[x,y]], then f_k = g_k for each k.
• binomialGenFun_eq: The generating function identity ∑_{n,k∈ℕ} C(n,k) x^n y^k = 1/(1-x(1+y))
• binomialGenFun_xyk_eq: Equation eq.fps.mulvar.exa1.xyk - the intermediate bivariate equation
• sum_choose_pow_eq: Equation eq.fps.mulvar.exa1.res1 - the univariate identity derived from comparing coefficients
• partialDeriv: Partial derivative of a multivariate power series
• partialDeriv_mul: The product rule for partial derivatives

References

• Section sec.gf.multivar of the source text

TODO

The source notes that this section needs more details.

Notation for multivariate power series rings

The K-algebra of all FPSs in k variables x₁, x₂, ..., xₖ over K is denoted by K[[x₁, x₂, ..., xₖ]] in the source. In Mathlib, this is MvPowerSeries (Fin k) K.

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS (k : ℕ) (R : Type u_2) [CommSemiring R] : Type u_2

The algebra of formal power series in k variables over R. This corresponds to K[[x₁, x₂, ..., xₖ]] in the source notation.

Equations

• AlgebraicCombinatorics.FPS k R = MvPowerSeries (Fin k) R

@[reducible, inline]

abbrev AlgebraicCombinatorics.BivFPS (R : Type u_2) [CommSemiring R] : Type u_2

The algebra of formal power series in 2 variables (bivariate). This corresponds to K[[x, y]] in the source.

Equations

• AlgebraicCombinatorics.BivFPS R = MvPowerSeries (Fin 2) R

noncomputable def AlgebraicCombinatorics.BivFPS.x {R : Type u_1} [CommSemiring R] : BivFPS R

The first variable x in a bivariate power series ring.

Equations

• AlgebraicCombinatorics.BivFPS.x = MvPowerSeries.X 0

noncomputable def AlgebraicCombinatorics.BivFPS.y {R : Type u_1} [CommSemiring R] : BivFPS R

The second variable y in a bivariate power series ring.

Equations

• AlgebraicCombinatorics.BivFPS.y = MvPowerSeries.X 1

Embedding univariate power series into bivariate power series

To formalize Proposition prop.fps.mulvar.comp-y-coeff, we need to embed sequences of univariate power series into bivariate power series. Given a sequence f : ℕ → PowerSeries R, we define the bivariate power series ∑_k f_k y^k whose coefficient at x^n y^k is the coefficient of x^n in f_k.

noncomputable def AlgebraicCombinatorics.embedUnivInBiv {R : Type u_1} [CommSemiring R] (f : ℕ → PowerSeries R) : BivFPS R

Embedding of a sequence of univariate power series f : ℕ → PowerSeries R into a bivariate power series ∑_k f_k y^k in K[[x, y]].

The coefficient of x^n y^k in the result is the coefficient of x^n in f_k.

Equations

• AlgebraicCombinatorics.embedUnivInBiv f nm = (PowerSeries.coeff (nm 0)) (f (nm 1))

@[simp]

theorem AlgebraicCombinatorics.coeff_embedUnivInBiv {R : Type u_1} [CommSemiring R] (f : ℕ → PowerSeries R) (n k : ℕ) : embedUnivInBiv f ((fun₀ | 0 => n) + fun₀ | 1 => k) = (PowerSeries.coeff n) (f k)

The coefficient of x^n y^k in embedUnivInBiv f is the coefficient of x^n in f k.

theorem AlgebraicCombinatorics.eq_of_embedUnivInBiv_eq {R : Type u_1} [CommSemiring R] (f g : ℕ → PowerSeries R) (h : embedUnivInBiv f = embedUnivInBiv g) : f = g

Proposition prop.fps.mulvar.comp-y-coeff: If two sequences of univariate power series f and g satisfy ∑_k f_k y^k = ∑_k g_k y^k in K[[x,y]], then f_k = g_k for each k.

This is the key tool for "comparing coefficients in front of y^k" to extract univariate identities from bivariate manipulations.

Example: Binomial generating function

The source derives the following identity using bivariate power series:

∑_{n,k∈ℕ} C(n,k) x^n y^k = 1/(1 - x(1+y))

From this, by comparing coefficients of y^k, one obtains the univariate identity:

x^k / (1-x)^{k+1} = ∑_{n∈ℕ} C(n,k) x^n  for each k ∈ ℕ

This is equation eq.fps.mulvar.exa1.res1 in the source.

noncomputable def AlgebraicCombinatorics.binomialGenFun : BivFPS ℚ

The generating function for binomial coefficients as a bivariate power series: ∑_{n,k∈ℕ} C(n,k) x^n y^k.

Equations

• AlgebraicCombinatorics.binomialGenFun nm = ↑((nm 0).choose (nm 1))

noncomputable def AlgebraicCombinatorics.binomialGenFunClosedForm : BivFPS ℚ

The closed form 1/(1 - x(1+y)) for the binomial generating function.

Equations

• AlgebraicCombinatorics.binomialGenFunClosedForm = (1 - AlgebraicCombinatorics.BivFPS.x * (1 + AlgebraicCombinatorics.BivFPS.y)).invOfUnit 1

theorem AlgebraicCombinatorics.binomialGenFun_eq : binomialGenFun = binomialGenFunClosedForm

The binomial generating function equals its closed form. ∑_{n,k∈ℕ} C(n,k) x^n y^k = 1/(1 - x(1+y))

This is the main computation in the example from the source.

theorem AlgebraicCombinatorics.one_sub_X_inv_eq_mk_one : (1 - PowerSeries.X)⁻¹ = PowerSeries.mk 1

The inverse of 1 - X in ℚ⟦X⟧ equals the power series with all coefficients 1.

theorem AlgebraicCombinatorics.X_pow_mul_inv_one_sub_pow_eq_mk_choose (k : ℕ) : PowerSeries.X ^ k * (1 - PowerSeries.X)⁻¹ ^ (k + 1) = PowerSeries.mk fun (n : ℕ) => ↑(n.choose k)

The univariate identity X^k * (1-X)⁻¹^(k+1) = ∑_n C(n,k) X^n. This is used to prove binomialGenFun_xyk_eq.

theorem AlgebraicCombinatorics.binomialGenFun_xyk_eq : (embedUnivInBiv fun (k : ℕ) => PowerSeries.X ^ k * (1 - PowerSeries.X)⁻¹ ^ (k + 1)) = embedUnivInBiv fun (k : ℕ) => PowerSeries.mk fun (n : ℕ) => ↑(n.choose k)

Equation eq.fps.mulvar.exa1.xyk: The intermediate bivariate identity ∑_{k∈ℕ} x^k/(1-x)^{k+1} y^k = ∑_{k∈ℕ} (∑_{n∈ℕ} C(n,k) x^n) y^k

expressed as equality of embedded univariate sequences. The left side is the sequence k ↦ x^k/(1-x)^{k+1} and the right side is k ↦ ∑_{n∈ℕ} C(n,k) x^n.

This equation is used to derive eq.fps.mulvar.exa1.res1 by comparing coefficients.

theorem AlgebraicCombinatorics.sum_choose_pow_eq (k : ℕ) : PowerSeries.X ^ k * (1 - PowerSeries.X)⁻¹ ^ (k + 1) = PowerSeries.mk fun (n : ℕ) => ↑(n.choose k)

Equation eq.fps.mulvar.exa1.res1: The generating function identity x^k / (1-x)^{k+1} = ∑_{n∈ℕ} C(n,k) x^n for each k ∈ ℕ.

This is derived from the bivariate identity by comparing coefficients of y^k.

Partial Derivatives

The source mentions that multivariate FPSs have k partial derivatives (one for each variable). This section provides the basic infrastructure for partial derivatives.

In Mathlib, more general derivation theory is available via MvPowerSeries.derivation. Here we provide a direct definition that matches the source's description: for f = ∑_m a_m x^m, we have ∂f/∂x_i = ∑_m m_i · a_m · x^{m - e_i}.

noncomputable def AlgebraicCombinatorics.partialDeriv {R : Type u_1} [CommSemiring R] {σ : Type u_2} [DecidableEq σ] (i : σ) : MvPowerSeries σ R →ₗ[R] MvPowerSeries σ R

The partial derivative of a multivariate power series with respect to variable i. For f = ∑_m a_m x^m, we have ∂f/∂x_i = ∑_m m_i · a_m · x^{m - e_i} where e_i is the i-th standard basis vector.

Equations

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

theorem AlgebraicCombinatorics.coeff_partialDeriv {R : Type u_1} [CommSemiring R] {σ : Type u_2} [DecidableEq σ] (i : σ) (f : MvPowerSeries σ R) (m : σ →₀ ℕ) : (MvPowerSeries.coeff m) ((partialDeriv i) f) = ↑((m + fun₀ | i => 1) i) * (MvPowerSeries.coeff (m + fun₀ | i => 1)) f

The coefficient of partialDeriv i f at m is (m + single i 1) i * coeff (m + single i 1) f.

theorem AlgebraicCombinatorics.antidiag_shift_fst {σ : Type u_2} [DecidableEq σ] (i : σ) (m : σ →₀ ℕ) : Finset.map { toFun := fun (p : (σ →₀ ℕ) × (σ →₀ ℕ)) => (p.1 + fun₀ | i => 1, p.2), inj' := ⋯ } (Finset.antidiagonal m) = {p ∈ Finset.antidiagonal (m + fun₀ | i => 1) | (fun₀ | i => 1) ≤ p.1}

The map (a, b) ↦ (a + single i 1, b) gives a bijection from antidiagonal m to the subset of antidiagonal (m + single i 1) where single i 1 ≤ a.

theorem AlgebraicCombinatorics.antidiag_shift_snd {σ : Type u_2} [DecidableEq σ] (i : σ) (m : σ →₀ ℕ) : Finset.map { toFun := fun (p : (σ →₀ ℕ) × (σ →₀ ℕ)) => (p.1, p.2 + fun₀ | i => 1), inj' := ⋯ } (Finset.antidiagonal m) = {p ∈ Finset.antidiagonal (m + fun₀ | i => 1) | (fun₀ | i => 1) ≤ p.2}

The map (a, b) ↦ (a, b + single i 1) gives a bijection from antidiagonal m to the subset of antidiagonal (m + single i 1) where single i 1 ≤ b.

theorem AlgebraicCombinatorics.sum_filter_zero_fst {R : Type u_1} [CommSemiring R] {σ : Type u_2} [DecidableEq σ] (i : σ) (m : σ →₀ ℕ) (f g : MvPowerSeries σ R) : ∑ p ∈ Finset.antidiagonal (m + fun₀ | i => 1) with ¬(fun₀ | i => 1) ≤ p.1, ↑(p.1 i) * (MvPowerSeries.coeff p.1) f * (MvPowerSeries.coeff p.2) g = 0

Terms where p.1 i = 0 contribute zero to the first derivative sum.

theorem AlgebraicCombinatorics.sum_filter_zero_snd {R : Type u_1} [CommSemiring R] {σ : Type u_2} [DecidableEq σ] (i : σ) (m : σ →₀ ℕ) (f g : MvPowerSeries σ R) : ∑ p ∈ Finset.antidiagonal (m + fun₀ | i => 1) with ¬(fun₀ | i => 1) ≤ p.2, (MvPowerSeries.coeff p.1) f * (↑(p.2 i) * (MvPowerSeries.coeff p.2) g) = 0

Terms where p.2 i = 0 contribute zero to the second derivative sum.

theorem AlgebraicCombinatorics.partialDeriv_mul {R : Type u_1} [CommSemiring R] {σ : Type u_2} [DecidableEq σ] (i : σ) (f g : MvPowerSeries σ R) : (partialDeriv i) (f * g) = (partialDeriv i) f * g + f * (partialDeriv i) g

The partial derivative satisfies the product rule.

Substitution in multivariate power series

One needs to be careful with substitution - one cannot substitute non-commuting elements into a multivariate polynomial. For example, you cannot substitute two non-commuting matrices A and B for x and y into the polynomial xy without sacrificing the rule that a value of the product of two polynomials should be the product of their values.

However, you can still substitute k commuting elements for the k indeterminates in a k-variable polynomial. You can also compose multivariate FPSs as long as appropriate summability conditions are satisfied.

The full theory of evaluation/substitution for multivariate power series is available in Mathlib via MvPowerSeries.eval and related constructions.