The generating function of power sums

For a multiset s in a commutative ring, the generating function of the power sums p_k = ∑_{θ ∈ s} θᵏ is the sum over s of the geometric series ∑ₖ θᵏ Xᵏ = (1 - θ X)⁻¹. Applied to the roots of the matching polynomial this gives the generating function of matchingPowerSum.

Main definitions

• PowerSeries.geomSeries a: the power series ∑ₖ aᵏ Xᵏ.

Main results

• PowerSeries.geomSeries_mul_one_sub: geomSeries a * (1 - C a * X) = 1.
• PowerSeries.powerSum_genfun: mk (fun k => (s.map (·ᵏ)).sum) = ∑_{θ ∈ s} geomSeries θ.
• SimpleGraph.matchingPowerSum_genfun: the same for the roots of μ(G).

noncomputable def PowerSeries.geomSeries {R : Type u_1} [CommRing R] (a : R) : PowerSeries R

The per-root geometric series Σ_k aᵏ Xᵏ ∈ R⟦X⟧, the formal inverse of 1 - aX.

Equations

• PowerSeries.geomSeries a = PowerSeries.mk fun (k : ℕ) => a ^ k

@[simp]

theorem PowerSeries.coeff_geomSeries {R : Type u_1} [CommRing R] (a : R) (n : ℕ) : (coeff n) (geomSeries a) = a ^ n

theorem PowerSeries.geomSeries_mul_one_sub {R : Type u_1} [CommRing R] (a : R) : geomSeries a * (1 - C a * X) = 1

geomSeries a is the formal inverse of 1 - aX: (Σ_k aᵏ Xᵏ)·(1 - aX) = 1. Transport of the unit a = 1 case (mk_one_mul_one_sub_eq_one, the geometric series (Σ Xᵏ)(1-X)=1) along the rescale a ring homomorphism X ↦ aX.

theorem PowerSeries.powerSum_genfun {R : Type u_1} [CommRing R] (s : Multiset R) : (mk fun (k : ℕ) => (Multiset.map (fun (x : R) => x ^ k) s).sum) = (Multiset.map geomSeries s).sum

Power-sum generating function (Lemma 4 core). For a multiset s : Multiset R, the generating function of the power sums p_k = Σ_{θ∈s} θᵏ is the multiset-sum of the per-root geometric series:

mk (fun k => (s.map (·ᵏ)).sum) = Σ_{θ∈s} geomSeries θ.

Proof: take the coefficient of Xⁿ on both sides. On the left, coeff_mk gives (s.map (·ⁿ)).sum; on the right, coeff n is additive (map_multiset_sum) and coeff n (geomSeries θ) = θⁿ, so both sides are Σ_{θ∈s} θⁿ.

theorem SimpleGraph.matchingPowerSum_genfun {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : (PowerSeries.mk fun (k : ℕ) => matchingPowerSum k) = (Multiset.map PowerSeries.geomSeries (Polynomial.map (algebraMap ℝ ℂ) G.matchingPoly).roots).sum

The matching-side generating function. Specialising powerSum_genfun to the multiset of complex roots of the matching polynomial: the generating function of matchingPowerSum G (Godsil's p_k = Σᵢ θᵢᵏ) is the sum over those roots of the per-root geometric series. This is the matching side of the moment-theorem bridge in formal-power-series form; the trace side is treeLikeWalkCount_eq_sum_pathTree_adjMatrix_pow welded through godsil_resolvent_charpoly_form.