Formal Power Series: Definition and Basic Properties

This file formalizes the definition of formal power series (FPS) and their basic operations, following Section "The definition of formal power series" (subsec.gf.defs.fps) of the source.

Main definitions

• fpsEquivSeq (Definition def.fps.fps): The equivalence between formal power series R⟦X⟧ and sequences ℕ → R. This formalizes that an FPS is a sequence (a₀, a₁, a₂, ...).

• We use Mathlib's PowerSeries R which represents formal power series over a ring R. This is defined as MvPowerSeries Unit R, i.e., sequences ℕ → R.

• PowerSeries.coeff n f extracts the n-th coefficient of a power series f. This corresponds to [x^n] f in the source notation.

• PowerSeries.mk constructs a power series from a sequence of coefficients.

• PowerSeries.X is the indeterminate x = (0, 1, 0, 0, ...).

• PowerSeries.C embeds constants into power series as (a, 0, 0, ...).

Main results

• PowerSeries forms a commutative ring (Theorem thm.fps.ring (a))
• PowerSeries is a module over the base ring (Theorem thm.fps.ring (b))
• Scaling by λ equals multiplication by C λ (Theorem thm.fps.ring (d))
• Coefficient extraction is additive and compatible with multiplication
• Multiplication by x shifts coefficients: X * (a₀, a₁, ...) = (0, a₀, a₁, ...) (Lemma lem.fps.xa)
• x^k has the form (0, 0, ..., 0, 1, 0, 0, ...) with k zeros (Proposition prop.fps.xk)
• Any FPS can be written as ∑ aₙ xⁿ (Corollary cor.fps.sumakxk)

References

• Source: FPSDefinition.tex, subsec.gf.defs.fps

Implementation notes

Mathlib already provides PowerSeries R with all the ring structure and basic operations. This file provides additional lemmas and connects Mathlib's API to the textbook presentation.

For summable families of FPS, we use Mathlib's topological structure on power series (PowerSeries.WithPiTopology), where a family is summable when for each coefficient index, all but finitely many terms have that coefficient equal to zero.

Definition of FPS (Definition def.fps.fps)

Definition def.fps.fps: A formal power series (FPS) in one indeterminate over K is a sequence (a₀, a₁, a₂, ...) = (aₙ)_{n ∈ ℕ} ∈ K^ℕ of elements of K.

In Mathlib, this is represented by PowerSeries R (notation: R⟦X⟧). The type PowerSeries R is defined as MvPowerSeries Unit R, which is definitionally (Unit →₀ ℕ) → R. Since Unit →₀ ℕ is equivalent to ℕ, this is essentially ℕ → R.

The constructor PowerSeries.mk : (ℕ → R) → R⟦X⟧ builds an FPS from a sequence. The extractor PowerSeries.coeff n : R⟦X⟧ → R retrieves the n-th coefficient.

noncomputable def AlgebraicCombinatorics.FPS.fpsEquivSeq {R : Type u_1} [CommRing R] : PowerSeries R ≃ (ℕ → R)

Definition def.fps.fps: The equivalence between formal power series R⟦X⟧ and sequences ℕ → R.

This formalizes Definition def.fps.fps from the source: a formal power series is a sequence (a₀, a₁, a₂, ...) of elements of R.

The forward direction extracts coefficients, the inverse constructs the FPS.

Equations

• AlgebraicCombinatorics.FPS.fpsEquivSeq = { toFun := fun (f : PowerSeries R) (n : ℕ) => (PowerSeries.coeff n) f, invFun := fun (a : ℕ → R) => PowerSeries.mk a, left_inv := ⋯, right_inv := ⋯ }

theorem AlgebraicCombinatorics.FPS.fps_mk_eq_symm {R : Type u_1} [CommRing R] (a : ℕ → R) : PowerSeries.mk a = fpsEquivSeq.symm a

The FPS (a₀, a₁, a₂, ...) is constructed from a sequence using PowerSeries.mk. This is the inverse of coefficient extraction.

theorem AlgebraicCombinatorics.FPS.fps_coeff_mk {R : Type u_1} [CommRing R] (a : ℕ → R) (n : ℕ) : (PowerSeries.coeff n) (PowerSeries.mk a) = a n

Extracting coefficients from an FPS gives back the original sequence (Definition def.fps.fps).

theorem AlgebraicCombinatorics.FPS.fps_eq_mk_coeff {R : Type u_1} [CommRing R] (f : PowerSeries R) : f = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff n) f

Any FPS equals the FPS constructed from its coefficient sequence (Definition def.fps.fps). This shows that every FPS is determined by its coefficients.

theorem AlgebraicCombinatorics.FPS.fps_ext_iff {R : Type u_1} [CommRing R] (f g : PowerSeries R) : f = g ↔ ∀ (n : ℕ), (PowerSeries.coeff n) f = (PowerSeries.coeff n) g

Two FPS are equal iff they have the same coefficients (Definition def.fps.fps). This is the extensionality principle for FPS.

theorem AlgebraicCombinatorics.FPS.zero_fps_eq {R : Type u_1} [CommRing R] : 0 = PowerSeries.mk fun (x : ℕ) => 0

The zero FPS is (0, 0, 0, ...)

theorem AlgebraicCombinatorics.FPS.one_fps_eq {R : Type u_1} [CommRing R] : 1 = PowerSeries.mk fun (n : ℕ) => if n = 0 then 1 else 0

The one FPS is (1, 0, 0, ...)

Operations on FPS (Definition def.fps.ops)

(a) Sum: (a₀ + b₀, a₁ + b₁, ...) (b) Difference: (a₀ - b₀, a₁ - b₁, ...) (c) Scalar multiplication: λa = (λa₀, λa₁, ...) (d) Product: c_n = ∑{i=0}^n a_i b{n-i} (e) Constants: a̲ = (a, 0, 0, ...)

@[simp]

theorem AlgebraicCombinatorics.FPS.coeff_add_fps {R : Type u_1} [CommRing R] (n : ℕ) (f g : PowerSeries R) : (PowerSeries.coeff n) (f + g) = (PowerSeries.coeff n) f + (PowerSeries.coeff n) g

(a) Sum of FPS is componentwise (eq. pf.thm.fps.ring.xn(a+b)=) Label: pf.thm.fps.ring.xn(a+b)=

@[simp]

theorem AlgebraicCombinatorics.FPS.coeff_sub_fps {R : Type u_1} [CommRing R] (n : ℕ) (f g : PowerSeries R) : (PowerSeries.coeff n) (f - g) = (PowerSeries.coeff n) f - (PowerSeries.coeff n) g

(b) Difference of FPS is componentwise (eq. pf.thm.fps.ring.xn(a-b)=) Label: pf.thm.fps.ring.xn(a-b)=

@[simp]

theorem AlgebraicCombinatorics.FPS.coeff_neg_fps {R : Type u_1} [CommRing R] (n : ℕ) (f : PowerSeries R) : (PowerSeries.coeff n) (-f) = -(PowerSeries.coeff n) f

Negation of FPS is componentwise (eq. pf.thm.fps.ring.xn(-a)=) Label: pf.thm.fps.ring.xn(-a)=

@[simp]

theorem AlgebraicCombinatorics.FPS.coeff_smul_fps {R : Type u_1} [CommRing R] (n : ℕ) (c : R) (f : PowerSeries R) : (PowerSeries.coeff n) (c • f) = c * (PowerSeries.coeff n) f

(c) Scalar multiplication (eq. pf.thm.fps.ring.xn(la)=) Label: pf.thm.fps.ring.xn(la)=

theorem AlgebraicCombinatorics.FPS.coeff_mul_fps {R : Type u_1} [CommRing R] (n : ℕ) (f g : PowerSeries R) : (PowerSeries.coeff n) (f * g) = ∑ p ∈ Finset.antidiagonal n, (PowerSeries.coeff p.1) f * (PowerSeries.coeff p.2) g

(d) Product of FPS uses convolution (eq. pf.thm.fps.ring.xn(ab)=2) Label: pf.thm.fps.ring.xn(ab)=2

theorem AlgebraicCombinatorics.FPS.coeff_mul_fps' {R : Type u_1} [CommRing R] (n : ℕ) (f g : PowerSeries R) : (PowerSeries.coeff n) (f * g) = ∑ i ∈ Finset.range (n + 1), (PowerSeries.coeff i) f * (PowerSeries.coeff (n - i)) g

Alternative form of product formula (eq. pf.thm.fps.ring.xn(ab)=3) Label: pf.thm.fps.ring.xn(ab)=3

theorem AlgebraicCombinatorics.FPS.coeff_C_fps {R : Type u_1} [CommRing R] (n : ℕ) (a : R) : (PowerSeries.coeff n) (PowerSeries.C a) = if n = 0 then a else 0

(e) Constant FPS: C a = (a, 0, 0, ...)

theorem AlgebraicCombinatorics.FPS.coeff_zero_mul_fps {R : Type u_1} [CommRing R] (f g : PowerSeries R) : (PowerSeries.coeff 0) (f * g) = (PowerSeries.coeff 0) f * (PowerSeries.coeff 0) g

The constant term of a product is the product of constant terms (eq. pf.thm.fps.ring.x0(ab)=) Label: pf.thm.fps.ring.x0(ab)=

Ring Structure (Theorem thm.fps.ring)

Theorem thm.fps.ring states that R⟦X⟧ is: (a) A commutative ring with zero = (0,0,...) and one = (1,0,0,...) (b) An R-module (c) Scaling commutes with multiplication: λ(fg) = (λf)g = f(λg) (d) Scaling equals multiplication by constant: λf = (C λ) * f

Note: Mathlib already provides these structures on PowerSeries R:

• CommRing R⟦X⟧ instance exists in Mathlib.RingTheory.PowerSeries.Basic
• Module R R⟦X⟧ instance exists via the algebra structure

theorem AlgebraicCombinatorics.FPS.smul_mul_fps {R : Type u_1} [CommRing R] (c : R) (f g : PowerSeries R) : c • (f * g) = c • f * g

(c) Scaling commutes with multiplication (Theorem thm.fps.ring (c))

theorem AlgebraicCombinatorics.FPS.smul_mul_fps' {R : Type u_1} [CommRing R] (c : R) (f g : PowerSeries R) : c • (f * g) = f * c • g

theorem AlgebraicCombinatorics.FPS.smul_eq_C_mul_fps {R : Type u_1} [CommRing R] (c : R) (f : PowerSeries R) : c • f = PowerSeries.C c * f

(d) Scaling equals multiplication by constant (Theorem thm.fps.ring (d))

Coefficient Extraction (Definition def.fps.coeff)

[x^n] f denotes the n-th coefficient of f. In Mathlib this is PowerSeries.coeff n f.

The Indeterminate x (Definition def.fps.x)

x = (0, 1, 0, 0, ...) is the FPS with [x^1] x = 1 and [x^i] x = 0 for i ≠ 1.

@[simp]

theorem AlgebraicCombinatorics.FPS.X_coeff_one {R : Type u_1} [CommRing R] : (PowerSeries.coeff 1) PowerSeries.X = 1

x = (0, 1, 0, 0, ...) (Definition def.fps.x)

theorem AlgebraicCombinatorics.FPS.X_coeff_ne_one {R : Type u_1} [CommRing R] (i : ℕ) (hi : i ≠ 1) : (PowerSeries.coeff i) PowerSeries.X = 0

Multiplication by x (Lemma lem.fps.xa)

Multiplying by x shifts the sequence: x * (a₀, a₁, a₂, ...) = (0, a₀, a₁, a₂, ...)

Lemma lem.fps.xa states: If f = (a₀, a₁, a₂, ...), then X * f = (0, a₀, a₁, a₂, ...). This is equivalent to:

• x^n = a_{n-1} if n > 0
• x^0 = 0

theorem AlgebraicCombinatorics.FPS.X_mul_shift {R : Type u_1} [CommRing R] (f : PowerSeries R) (n : ℕ) : (PowerSeries.coeff (n + 1)) (PowerSeries.X * f) = (PowerSeries.coeff n) f

Multiplying by x shifts coefficients: x^{n+1} = [x^n]f (Lemma lem.fps.xa)

theorem AlgebraicCombinatorics.FPS.mul_X_shift {R : Type u_1} [CommRing R] (f : PowerSeries R) (n : ℕ) : (PowerSeries.coeff (n + 1)) (f * PowerSeries.X) = (PowerSeries.coeff n) f

Multiplying by x on the right shifts coefficients: x^{n+1} = [x^n]f

@[simp]

theorem AlgebraicCombinatorics.FPS.X_mul_coeff_zero {R : Type u_1} [CommRing R] (f : PowerSeries R) : (PowerSeries.coeff 0) (PowerSeries.X * f) = 0

The constant term of X * f is 0 (Lemma lem.fps.xa, case n = 0)

@[simp]

theorem AlgebraicCombinatorics.FPS.mul_X_coeff_zero {R : Type u_1} [CommRing R] (f : PowerSeries R) : (PowerSeries.coeff 0) (f * PowerSeries.X) = 0

The constant term of f * X is 0

theorem AlgebraicCombinatorics.FPS.coeff_X_mul {R : Type u_1} [CommRing R] (f : PowerSeries R) (n : ℕ) : (PowerSeries.coeff n) (PowerSeries.X * f) = if n = 0 then 0 else (PowerSeries.coeff (n - 1)) f

Complete characterization of multiplication by X (Lemma lem.fps.xa, unified form)

If f = (a₀, a₁, a₂, ...), then X * f = (0, a₀, a₁, a₂, ...) This is equivalent to: x^n = if n = 0 then 0 else [x^{n-1}]f

theorem AlgebraicCombinatorics.FPS.coeff_mul_X {R : Type u_1} [CommRing R] (f : PowerSeries R) (n : ℕ) : (PowerSeries.coeff n) (f * PowerSeries.X) = if n = 0 then 0 else (PowerSeries.coeff (n - 1)) f

Complete characterization of multiplication by X on the right (Lemma lem.fps.xa, variant)

If f = (a₀, a₁, a₂, ...), then f * X = (0, a₀, a₁, a₂, ...) This is equivalent to: x^n = if n = 0 then 0 else [x^{n-1}]f

theorem AlgebraicCombinatorics.FPS.X_mul_eq_shift {R : Type u_1} [CommRing R] (f : PowerSeries R) : PowerSeries.X * f = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else (PowerSeries.coeff (n - 1)) f

X * f equals f with all coefficients shifted by one position (Lemma lem.fps.xa, equality form)

This directly expresses: X * (a₀, a₁, a₂, ...) = (0, a₀, a₁, a₂, ...)

theorem AlgebraicCombinatorics.FPS.mul_X_eq_shift {R : Type u_1} [CommRing R] (f : PowerSeries R) : f * PowerSeries.X = PowerSeries.mk fun (n : ℕ) => if n = 0 then 0 else (PowerSeries.coeff (n - 1)) f

f * X equals f with all coefficients shifted by one position (Lemma lem.fps.xa, equality form)

theorem AlgebraicCombinatorics.FPS.coeff_X_pow_mul {R : Type u_1} [CommRing R] (k : ℕ) (f : PowerSeries R) (n : ℕ) : (PowerSeries.coeff n) (PowerSeries.X ^ k * f) = if n < k then 0 else (PowerSeries.coeff (n - k)) f

X^k * f shifts f by k positions (generalization of Lemma lem.fps.xa)

If f = (a₀, a₁, a₂, ...), then X^k * f = (0, ..., 0, a₀, a₁, a₂, ...) with k leading zeros.

theorem AlgebraicCombinatorics.FPS.coeff_mul_X_pow {R : Type u_1} [CommRing R] (k : ℕ) (f : PowerSeries R) (n : ℕ) : (PowerSeries.coeff n) (f * PowerSeries.X ^ k) = if n < k then 0 else (PowerSeries.coeff (n - k)) f

f * X^k shifts f by k positions (generalization of Lemma lem.fps.xa)

Powers of x (Proposition prop.fps.xk)

x^k = (0, 0, ..., 0, 1, 0, 0, ...) with k zeros before the 1.

theorem AlgebraicCombinatorics.FPS.X_pow_coeff {R : Type u_1} [CommRing R] (k n : ℕ) : (PowerSeries.coeff n) (PowerSeries.X ^ k) = if n = k then 1 else 0

x^k has 1 in position k and 0 elsewhere (Proposition prop.fps.xk)

@[simp]

theorem AlgebraicCombinatorics.FPS.X_pow_coeff_self {R : Type u_1} [CommRing R] (k : ℕ) : (PowerSeries.coeff k) (PowerSeries.X ^ k) = 1

FPS as Infinite Sum (Corollary cor.fps.sumakxk)

Any FPS (a₀, a₁, a₂, ...) can be written as ∑_{n ∈ ℕ} aₙ x^n. This requires the notion of summable families of FPS.

theorem AlgebraicCombinatorics.FPS.fps_eq_tsum_coeff {R : Type u_1} [CommRing R] (f : PowerSeries R) : f = PowerSeries.mk fun (n : ℕ) => (PowerSeries.coeff n) f

The family (aₙ x^n)_{n ∈ ℕ} represents the FPS with coefficients (aₙ). This is essentially saying PowerSeries.mk a = ∑ a n * X^n (Corollary cor.fps.sumakxk)

theorem AlgebraicCombinatorics.FPS.coeff_monomial_mul_X_pow {R : Type u_1} [CommRing R] (a : R) (k n : ℕ) : (PowerSeries.coeff n) (PowerSeries.C a * PowerSeries.X ^ k) = if n = k then a else 0

aₙ x^n has coefficient aₙ in position n and 0 elsewhere

Summable Families of FPS (Definition def.fps.summable)

A family (fᵢ)_{i ∈ I} of FPS is summable (or entrywise essentially finite) if for each n ∈ ℕ, all but finitely many i ∈ I satisfy [x^n] fᵢ = 0.

In this case, the sum ∑{i ∈ I} fᵢ is defined as the FPS with [x^n](∑{i ∈ I} fᵢ) = ∑_{i ∈ I} [x^n] fᵢ (an essentially finite sum).

In Mathlib, this is captured by the topology on power series where convergence means eventual stability of each coefficient. See PowerSeries.WithPiTopology for details.

def AlgebraicCombinatorics.FPS.SummableFPS {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → PowerSeries R) : Prop

A family of FPS is summable if for each coefficient index n, all but finitely many family members have that coefficient equal to zero. (Definition def.fps.summable)

Equations

• AlgebraicCombinatorics.FPS.SummableFPS f = ∀ (n : ℕ), {i : ι | (PowerSeries.coeff n) (f i) ≠ 0}.Finite

noncomputable def AlgebraicCombinatorics.FPS.summableFPSSum {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → PowerSeries R) (_hf : SummableFPS f) : PowerSeries R

The sum of a summable family of FPS. (Definition def.fps.summable, eq. eq.def.fps.summable.sum)

For a summable family (fᵢ){i ∈ I}, the sum ∑{i ∈ I} fᵢ is the FPS whose n-th coefficient is ∑_{i ∈ I} [x^n] fᵢ (an essentially finite sum).

Equations

• AlgebraicCombinatorics.FPS.summableFPSSum f _hf = PowerSeries.mk fun (n : ℕ) => ∑ᶠ (i : ι), (PowerSeries.coeff n) (f i)

theorem AlgebraicCombinatorics.FPS.coeff_summableFPSSum {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → PowerSeries R) (hf : SummableFPS f) (n : ℕ) : (PowerSeries.coeff n) (summableFPSSum f hf) = ∑ᶠ (i : ι), (PowerSeries.coeff n) (f i)

The n-th coefficient of a summable sum is the sum of n-th coefficients. (eq. eq.def.fps.summable.sum)

theorem AlgebraicCombinatorics.FPS.summableFPS_finsum_finite {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → PowerSeries R) (hf : SummableFPS f) (n : ℕ) : (Function.support fun (i : ι) => (PowerSeries.coeff n) (f i)).Finite

The sum of the coefficients is finite (since the family is summable).

theorem AlgebraicCombinatorics.FPS.summableFPS_subfamily {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → PowerSeries R} (J : Set ι) (hf : SummableFPS f) : SummableFPS fun (i : ↑J) => f ↑i

Any subfamily of a summable family of FPS is summable. (Proposition prop.fps.summable.sub)

theorem AlgebraicCombinatorics.FPS.summableFPS_of_finite {R : Type u_1} [CommRing R] {ι : Type u_2} [Finite ι] (f : ι → PowerSeries R) : SummableFPS f

A finite family of FPS is always summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_zero {R : Type u_1} [CommRing R] {ι : Type u_2} : SummableFPS fun (x : ι) => 0

The zero family is summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_single {R : Type u_1} [CommRing R] (f : PowerSeries R) : SummableFPS fun (x : Unit) => f

A singleton family is summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_add {R : Type u_1} [CommRing R] {ι : Type u_2} {f g : ι → PowerSeries R} (hf : SummableFPS f) (hg : SummableFPS g) : SummableFPS fun (i : ι) => f i + g i

Sum of two summable families is summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_neg {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → PowerSeries R} (hf : SummableFPS f) : SummableFPS fun (i : ι) => -f i

Negation of a summable family is summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_sub {R : Type u_1} [CommRing R] {ι : Type u_2} {f g : ι → PowerSeries R} (hf : SummableFPS f) (hg : SummableFPS g) : SummableFPS fun (i : ι) => f i - g i

Subtraction of two summable families is summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_smul {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → PowerSeries R} (c : R) (hf : SummableFPS f) : SummableFPS fun (i : ι) => c • f i

Scalar multiple of a summable family is summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_of_essentiallyFinite {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → PowerSeries R) (hf : {i : ι | f i ≠ 0}.Finite) : SummableFPS f

An essentially finite family of FPS is summable.

theorem AlgebraicCombinatorics.FPS.summableFPS_monomial_family {R : Type u_1} [CommRing R] (a : ℕ → R) : SummableFPS fun (n : ℕ) => PowerSeries.C (a n) * PowerSeries.X ^ n

The family (C(aₙ) * X^n){n ∈ ℕ} is summable for any sequence (aₙ). This is the canonical example showing that any FPS can be written as an infinite sum ∑{n ∈ ℕ} aₙ x^n.

Essentially Finite Sums (Definition def.infsum.essfin)

A family (aᵢ)_{i ∈ I} of ring elements is essentially finite if all but finitely many i satisfy aᵢ = 0.

Note: This is equivalent to (Function.support f).Finite in Mathlib.

Part (a): Definition of essentially finite families

A family (aᵢ)_{i ∈ I} ∈ K^I of elements of K is essentially finite if all but finitely many i ∈ I satisfy aᵢ = 0 (in other words, if the set {i ∈ I | aᵢ ≠ 0} is finite).

Part (b): Sum of essentially finite families

Let (aᵢ){i ∈ I} ∈ K^I be an essentially finite family of elements of K. Then, the infinite sum ∑{i ∈ I} aᵢ is defined to equal the finite sum ∑_{i ∈ I, aᵢ ≠ 0} aᵢ. Such an infinite sum is said to be essentially finite.

@[reducible, inline]

abbrev AlgebraicCombinatorics.FPS.EssentiallyFinite {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) : Prop

A family is essentially finite if its support is finite. (Definition def.infsum.essfin (a))

This is an alias for the canonical EssentiallyFinite defined in FPS/InfiniteProducts2.lean. Both definitions are definitionally equal: {i | f i ≠ 0}.Finite = (Function.support f).Finite by definition.

For the full API (including _root_.EssentiallyFinite.add, _root_.EssentiallyFinite.neg, _root_.EssentiallyFinite.toFinsupp, etc.), see FPS/InfiniteProducts2.lean.

Equations

• AlgebraicCombinatorics.FPS.EssentiallyFinite f = EssentiallyFinite f

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_iff_support_finite {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) : EssentiallyFinite f ↔ (Function.support f).Finite

EssentiallyFinite is equivalent to having finite support.

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_subfamily {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → R} (J : Set ι) (hf : EssentiallyFinite f) : EssentiallyFinite fun (i : ↑J) => f ↑i

Any subfamily of an essentially finite family is essentially finite. (Delegates to _root_.EssentiallyFinite.subfamily)

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_of_finite {R : Type u_1} [CommRing R] {ι : Type u_2} [Finite ι] (f : ι → R) : EssentiallyFinite f

Any finite family is essentially finite. (Delegates to _root_.EssentiallyFinite.of_finite)

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_fintype {R : Type u_1} [CommRing R] {ι : Type u_2} [Fintype ι] (f : ι → R) : EssentiallyFinite f

A family indexed by a finite type is essentially finite. (Delegates to _root_.EssentiallyFinite.of_fintype)

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_zero {R : Type u_1} [CommRing R] {ι : Type u_2} : EssentiallyFinite fun (x : ι) => 0

The constant zero family is essentially finite. (Delegates to _root_.EssentiallyFinite.zero)

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_add {R : Type u_1} [CommRing R] {ι : Type u_2} {f g : ι → R} (hf : EssentiallyFinite f) (hg : EssentiallyFinite g) : EssentiallyFinite fun (i : ι) => f i + g i

Sum of two essentially finite families is essentially finite. (Delegates to _root_.EssentiallyFinite.add)

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_neg {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → R} (hf : EssentiallyFinite f) : EssentiallyFinite fun (i : ι) => -f i

Negation of an essentially finite family is essentially finite. (Delegates to _root_.EssentiallyFinite.neg)

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_sub {R : Type u_1} [CommRing R] {ι : Type u_2} {f g : ι → R} (hf : EssentiallyFinite f) (hg : EssentiallyFinite g) : EssentiallyFinite fun (i : ι) => f i - g i

Subtraction of two essentially finite families is essentially finite. (Delegates to _root_.EssentiallyFinite.sub)

theorem AlgebraicCombinatorics.FPS.essentiallyFinite_smul {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → R} (c : R) (hf : EssentiallyFinite f) : EssentiallyFinite fun (i : ι) => c * f i

Scalar multiple of an essentially finite family is essentially finite. Note: Uses _root_.EssentiallyFinite.const_mul with NoZeroDivisors assumption.

Sum of an essentially finite family (Definition def.infsum.essfin (b))

For an essentially finite family (aᵢ){i ∈ I}, the infinite sum ∑{i ∈ I} aᵢ is defined to equal the finite sum ∑_{i ∈ I, aᵢ ≠ 0} aᵢ.

We connect this to Mathlib's Finsupp.sum infrastructure.

noncomputable def AlgebraicCombinatorics.FPS.essFinSum {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) (hf : EssentiallyFinite f) : R

The sum of an essentially finite family, defined as the finite sum over non-zero elements. (Definition def.infsum.essfin (b))

Equations

• AlgebraicCombinatorics.FPS.essFinSum f hf = ∑ i ∈ Set.Finite.toFinset hf, f i

theorem AlgebraicCombinatorics.FPS.essFinSum_eq_finset_sum {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) (hf : EssentiallyFinite f) : essFinSum f hf = ∑ i ∈ Set.Finite.toFinset hf, f i

The essentially finite sum equals the Finset sum over the support

theorem AlgebraicCombinatorics.FPS.essFinSum_eq_sum_of_support_subset {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) (hf : EssentiallyFinite f) (S : Finset ι) (hS : Set.Finite.toFinset hf ⊆ S) : essFinSum f hf = ∑ i ∈ S, f i

If a family has finite support contained in a finset S, the essentially finite sum equals the sum over S

theorem AlgebraicCombinatorics.FPS.essFinSum_zero {R : Type u_1} [CommRing R] {ι : Type u_2} (hf : EssentiallyFinite fun (x : ι) => 0) : essFinSum (fun (x : ι) => 0) hf = 0

The essentially finite sum of a zero family is zero

theorem AlgebraicCombinatorics.FPS.essFinSum_eq_zero_of_forall_zero {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → R} (hf : EssentiallyFinite f) (h : ∀ (i : ι), f i = 0) : essFinSum f hf = 0

The essentially finite sum of a family that is zero everywhere is zero

theorem AlgebraicCombinatorics.FPS.essFinSum_eq_sum_finset {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) (hf : EssentiallyFinite f) (S : Finset ι) (hS : ∀ (i : ι), f i ≠ 0 → i ∈ S) : essFinSum f hf = ∑ i ∈ S, f i

The essentially finite sum can be computed using any finset containing the support

theorem AlgebraicCombinatorics.FPS.essFinSum_single {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] (i : ι) (a : R) : EssentiallyFinite fun (j : ι) => if j = i then a else 0

The essentially finite sum of a single nonzero element

noncomputable def AlgebraicCombinatorics.FPS.essentiallyFiniteToFinsupp {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) (hf : EssentiallyFinite f) : ι →₀ R

Connection to Finsupp: an essentially finite family can be converted to a Finsupp

Equations

• AlgebraicCombinatorics.FPS.essentiallyFiniteToFinsupp f hf = Finsupp.ofSupportFinite f hf

theorem AlgebraicCombinatorics.FPS.essentiallyFiniteToFinsupp_apply {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) (hf : EssentiallyFinite f) (i : ι) : (essentiallyFiniteToFinsupp f hf) i = f i

theorem AlgebraicCombinatorics.FPS.essFinSum_eq_finsupp_sum {R : Type u_1} [CommRing R] {ι : Type u_2} (f : ι → R) (hf : EssentiallyFinite f) : essFinSum f hf = (essentiallyFiniteToFinsupp f hf).sum fun (x : ι) (r : R) => r

The essentially finite sum equals the Finsupp sum

theorem AlgebraicCombinatorics.FPS.essFinSum_add {R : Type u_1} [CommRing R] {ι : Type u_2} [DecidableEq ι] {f g : ι → R} (hf : EssentiallyFinite f) (hg : EssentiallyFinite g) (hfg : EssentiallyFinite fun (i : ι) => f i + g i) : essFinSum (fun (i : ι) => f i + g i) hfg = essFinSum f hf + essFinSum g hg

Additivity: the essentially finite sum of a sum is the sum of essentially finite sums

theorem AlgebraicCombinatorics.FPS.essFinSum_smul {R : Type u_1} [CommRing R] {ι : Type u_2} {f : ι → R} (c : R) (hf : EssentiallyFinite f) (hcf : EssentiallyFinite fun (i : ι) => c * f i) : essFinSum (fun (i : ι) => c * f i) hcf = c * essFinSum f hf

Scalar multiplication: c * (∑ aᵢ) = ∑ (c * aᵢ)

Rules for Summable Sums (Proposition prop.fps.summable-sums-rule)

Sums of summable families of FPS satisfy the usual rules for sums:

• Breaking-apart rule: if S = X ∪ Y (disjoint), then ∑{i ∈ S} fᵢ = ∑{i ∈ X} fᵢ + ∑_{i ∈ Y} fᵢ
• Fubini rule: ∑{i ∈ I} ∑{j ∈ J} fᵢⱼ = ∑{(i,j) ∈ I×J} fᵢⱼ = ∑{j ∈ J} ∑{i ∈ I} fᵢⱼ (when the family (fᵢⱼ){(i,j) ∈ I×J} is summable)

These properties follow from the corresponding properties of essentially finite sums applied coefficient-wise.

theorem AlgebraicCombinatorics.FPS.summableFPS_fubini {R : Type u_1} [CommRing R] {ι : Type u_2} {κ : Type u_3} {f : ι × κ → PowerSeries R} (hf : SummableFPS f) : (∀ (i : ι), SummableFPS fun (j : κ) => f (i, j)) ∧ ∀ (j : κ), SummableFPS fun (i : ι) => f (i, j)

The Fubini rule for summable FPS families: interchange of summation is valid when the family indexed by the product is summable. (Proposition prop.fps.summable-sums-rule, discrete Fubini rule)

Note: The actual sum computation requires Mathlib's topological sum machinery. This theorem states that the summability condition on the product implies summability of the iterated sums.

Generating Functions

The (ordinary) generating function of a sequence (a₀, a₁, a₂, ...) is the FPS (a₀, a₁, a₂, ...) = a₀ + a₁x + a₂x² + ...

def AlgebraicCombinatorics.FPS.generatingFunction {R : Type u_1} (a : ℕ → R) : PowerSeries R

The generating function of a sequence is just the FPS with those coefficients

Equations

• AlgebraicCombinatorics.FPS.generatingFunction a = PowerSeries.mk a

theorem AlgebraicCombinatorics.FPS.generatingFunction_coeff {R : Type u_1} [CommRing R] (a : ℕ → R) (n : ℕ) : (PowerSeries.coeff n) (generatingFunction a) = a n

@[simp]

theorem AlgebraicCombinatorics.FPS.generatingFunction_zero {R : Type u_1} [CommRing R] : generatingFunction 0 = 0

The generating function of the zero sequence is 0

@[simp]

theorem AlgebraicCombinatorics.FPS.generatingFunction_add {R : Type u_1} [CommRing R] (a b : ℕ → R) : generatingFunction (a + b) = generatingFunction a + generatingFunction b

The generating function of a sum is the sum of generating functions

@[simp]

theorem AlgebraicCombinatorics.FPS.generatingFunction_neg {R : Type u_1} [CommRing R] (a : ℕ → R) : generatingFunction (-a) = -generatingFunction a

The generating function of a negation is the negation of the generating function

@[simp]

theorem AlgebraicCombinatorics.FPS.generatingFunction_smul {R : Type u_1} [CommRing R] (c : R) (a : ℕ → R) : generatingFunction (c • a) = c • generatingFunction a

The generating function of a scalar multiple is the scalar multiple of the generating function

@[simp]

theorem AlgebraicCombinatorics.FPS.generatingFunction_sub {R : Type u_1} [CommRing R] (a b : ℕ → R) : generatingFunction (a - b) = generatingFunction a - generatingFunction b

Subtraction of generating functions

@[simp]

theorem AlgebraicCombinatorics.FPS.generatingFunction_one {R : Type u_1} [CommRing R] : (generatingFunction fun (n : ℕ) => if n = 0 then 1 else 0) = 1

The generating function of the indicator function at 0 is 1

Vandermonde / Chu-Vandermonde Identity

For Natural Numbers (Proposition prop.binom.vandermonde.NN)

For a, b, n ∈ ℕ: C(a+b, n) = ∑_{k=0}^n C(a,k) C(b, n-k)

theorem AlgebraicCombinatorics.FPS.vandermonde_nat (a b n : ℕ) : (a + b).choose n = ∑ ij ∈ Finset.antidiagonal n, a.choose ij.1 * b.choose ij.2

Vandermonde's identity for natural numbers (Proposition prop.binom.vandermonde.NN) Label: eq.prop.binom.vandermonde.NN.eq

theorem AlgebraicCombinatorics.FPS.vandermonde_nat' (a b n : ℕ) : (a + b).choose n = ∑ k ∈ Finset.range (n + 1), a.choose k * b.choose (n - k)

Alternative form using range

For Complex Numbers (Theorem thm.binom.vandermonde.CC)

The Chu-Vandermonde identity extends to all complex numbers (or any binomial ring). For a, b ∈ ℂ and n ∈ ℕ: C(a+b, n) = ∑_{k=0}^n C(a,k) C(b, n-k)

The proof uses the polynomial identity trick: both sides are polynomials in a and b that agree on ℕ × ℕ, hence they agree everywhere.

theorem AlgebraicCombinatorics.FPS.chuVandermonde {S : Type u_2} [CommRing S] [BinomialRing S] (a b : S) (n : ℕ) : Ring.choose (a + b) n = ∑ ij ∈ Finset.antidiagonal n, Ring.choose a ij.1 * Ring.choose b ij.2

Chu-Vandermonde identity for binomial rings (Theorem thm.binom.vandermonde.CC) Label: eq.prop.binom.vandermonde.CC.eq

This generalizes Vandermonde's identity from natural numbers to any binomial ring (including ℚ, ℝ, ℂ, and polynomial rings).