Integer Compositions

This file formalizes integer compositions and weak compositions, following Section sec.fps.intcomps of the source text.

Main definitions

• Composition - A composition as a List ℕ+ (tuple of positive integers)
• Composition.append - Concatenation of two compositions
• Composition.ofSize n - The subtype of compositions with size n
• Composition.ofSizeIntoParts n k - The subtype of compositions with size n and length k
• WeakComposition - A weak composition as a List ℕ (tuple of nonnegative integers)
• WeakComposition.ofSizeIntoParts n k - Weak compositions of n into k parts
• BoundedWeakComposition n k p - Weak compositions with entries in {0, 1, ..., p-1}

Main results

• Composition.card_ofSizeIntoParts_pos - The number of compositions of n into k parts is Nat.choose (n-1) (k-1) for n > 0 and k > 0 (Theorem thm.fps.comps.num-comps-n-k)
• Composition.card_ofSizeIntoParts_zero - The number of compositions of 0 into k parts is 1 if k = 0, else 0
• Composition.card_ofSizeIntoParts_k_zero - The number of compositions of n > 0 into 0 parts is 0
• Composition.card_ofSize - The number of compositions of n is 2^(n-1) for n > 0 (Theorem thm.fps.comps.num-comps-n)
• WeakComposition.card_ofSizeIntoParts - The number of weak compositions of n into k parts is Nat.choose (n+k-1) n (Theorem thm.fps.comps.num-wcomps-n-k)
• BoundedWeakComposition.card - The number of weak compositions with bounded entries (Theorem thm.fps.comps.num-wpcomps-n-k)
• binom_sum_identity - An identity involving binomial coefficients (Proposition prop.fps.comps.num-w2comps-n-k-id)

Implementation notes

This file defines Composition as List ℕ+, which is an alternative representation to Mathlib's Mathlib.Combinatorics.Enumerative.Composition which uses Composition n as a structure with blocks : List ℕ and proofs of positivity and sum. Both representations are equivalent; we use List ℕ+ here to follow the source text's presentation more directly.

References

See the source LaTeX file AlgebraicCombinatorics/tex/FPS/IntegerCompositions.tex

Integer Compositions

def AlgebraicCombinatorics.Composition : Type

An integer composition is a finite tuple of positive integers. We represent it as a list of positive integers.

(Definition def.fps.comps, part (a))

Equations

• AlgebraicCombinatorics.Composition = List ℕ+

instance AlgebraicCombinatorics.Composition.instInhabited : Inhabited Composition

Equations

• AlgebraicCombinatorics.Composition.instInhabited = { default := [] }

def AlgebraicCombinatorics.Composition.size (α : Composition) : ℕ

The size of a composition is the sum of its entries.

(Definition def.fps.comps, part (b))

Equations

• α.size = (List.map (fun (x : ℕ+) => ↑x) α).sum

def AlgebraicCombinatorics.Composition.len (α : Composition) : ℕ

The length of a composition is the number of parts. (We use len to avoid conflict with List.length.)

(Definition def.fps.comps, part (c))

Equations

• α.len = List.length α

Basic @[simp] lemmas for size and len

@[simp]

theorem AlgebraicCombinatorics.Composition.size_nil : size [] = 0

The size of the empty composition is 0.

@[simp]

theorem AlgebraicCombinatorics.Composition.len_nil : len [] = 0

The length of the empty composition is 0.

@[simp]

theorem AlgebraicCombinatorics.Composition.size_cons (a : ℕ+) (α : Composition) : size (a :: α) = ↑a + α.size

The size of a cons composition is the head value plus the tail size.

@[simp]

theorem AlgebraicCombinatorics.Composition.len_cons (a : ℕ+) (α : Composition) : len (a :: α) = α.len + 1

The length of a cons composition is the tail length plus 1.

theorem AlgebraicCombinatorics.Composition.size_ge_len (α : Composition) : α.len ≤ α.size

The size of a composition is at least its length, since each part is positive.

Singleton constructor

def AlgebraicCombinatorics.Composition.singleton (n : ℕ+) : Composition

A composition with a single part.

Equations

• AlgebraicCombinatorics.Composition.singleton n = [n]

@[simp]

theorem AlgebraicCombinatorics.Composition.size_singleton (n : ℕ+) : (singleton n).size = ↑n

The size of a singleton composition is the value of its single part.

@[simp]

theorem AlgebraicCombinatorics.Composition.len_singleton (n : ℕ+) : (singleton n).len = 1

The length of a singleton composition is 1.

Append operation

def AlgebraicCombinatorics.Composition.append (α β : Composition) : Composition

Concatenation of two compositions.

Equations

• α.append β = List.append α β

instance AlgebraicCombinatorics.Composition.instAppend : Append Composition

Equations

• AlgebraicCombinatorics.Composition.instAppend = { append := AlgebraicCombinatorics.Composition.append }

@[simp]

theorem AlgebraicCombinatorics.Composition.size_append (α β : Composition) : (α ++ β).size = α.size + β.size

The size of the concatenation of two compositions equals the sum of their sizes.

@[simp]

theorem AlgebraicCombinatorics.Composition.len_append (α β : Composition) : (α ++ β).len = α.len + β.len

The length of the concatenation of two compositions equals the sum of their lengths.

def AlgebraicCombinatorics.Composition.ofSize (n : ℕ) : Type

A composition of n is a composition whose size is n.

(Definition def.fps.comps, part (d))

Equations

• AlgebraicCombinatorics.Composition.ofSize n = { α : AlgebraicCombinatorics.Composition // α.size = n }

def AlgebraicCombinatorics.Composition.ofSizeIntoParts (n k : ℕ) : Type

A composition of n into k parts is a composition with size n and length k.

(Definition def.fps.comps, part (e))

Equations

• AlgebraicCombinatorics.Composition.ofSizeIntoParts n k = { α : AlgebraicCombinatorics.Composition // α.size = n ∧ α.len = k }

Equivalence with Mathlib's Composition type

def AlgebraicCombinatorics.Composition.toBlocks (α : Composition) : List ℕ

Convert a composition (List ℕ+) to a blocks list (List ℕ)

Equations

• α.toBlocks = List.map (fun (x : ℕ+) => ↑x) α

def AlgebraicCombinatorics.Composition.ofBlocks (blocks : List ℕ) (hpos : ∀ {i : ℕ}, i ∈ blocks → 0 < i) : Composition

Convert a blocks list with positivity proof to a composition (List ℕ+)

Equations

• AlgebraicCombinatorics.Composition.ofBlocks blocks hpos = List.pmap (fun (i : ℕ) (hi : 0 < i) => ⟨i, hi⟩) blocks ⋯

theorem AlgebraicCombinatorics.Composition.toBlocks_ofBlocks (blocks : List ℕ) (hpos : ∀ {i : ℕ}, i ∈ blocks → 0 < i) : (ofBlocks blocks ⋯).toBlocks = blocks

theorem AlgebraicCombinatorics.Composition.ofBlocks_toBlocks (α : Composition) : ofBlocks α.toBlocks ⋯ = α

theorem AlgebraicCombinatorics.Composition.size_eq_sum_toBlocks (α : Composition) : α.size = α.toBlocks.sum

theorem AlgebraicCombinatorics.Composition.len_eq_toBlocks_length (α : Composition) : α.len = α.toBlocks.length

def AlgebraicCombinatorics.Composition.equivMathlib (n : ℕ) : ofSize n ≃ _root_.Composition n

Equivalence between our Composition.ofSize n and Mathlib's Composition n. This allows us to use Mathlib's composition_card theorem.

Equations

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

def AlgebraicCombinatorics.Composition.equivMathlibFiltered (n k : ℕ) : ofSizeIntoParts n k ≃ ↑{c : _root_.Composition n | c.length = k}

Equivalence between Composition.ofSizeIntoParts n k and the filtered set of Mathlib compositions of n with length k.

Equations

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

theorem AlgebraicCombinatorics.Composition.empty_of_size_zero (α : Composition) (h : α.size = 0) : α = []

The empty list is the only composition of size 0.

instance AlgebraicCombinatorics.Composition.fintypeOfSizeIntoParts (n k : ℕ) : Fintype (ofSizeIntoParts n k)

The set of all compositions of n into k parts is finite.

Equations

• AlgebraicCombinatorics.Composition.fintypeOfSizeIntoParts n k = Fintype.ofEquiv (↑{c : Composition n | c.length = k}) (AlgebraicCombinatorics.Composition.equivMathlibFiltered n k).symm

Counting Compositions via Mathlib

We prove the main counting theorem using Mathlib's Composition n type, which has a well-developed API including an equivalence with subsets of Fin (n-1).

The key insight is that compositions of n into k parts correspond bijectively to (k-1)-element subsets of {1, ..., n-1}, giving the count C(n-1, k-1).

def AlgebraicCombinatorics.MathlibComposition.compositionToFinset (n : ℕ) : _root_.Composition n ≃ Finset (Fin (n - 1))

Equivalence between Mathlib's Composition n and subsets of Fin (n-1).

Equations

• AlgebraicCombinatorics.MathlibComposition.compositionToFinset n = (compositionEquiv n).trans (compositionAsSetEquiv n)

theorem AlgebraicCombinatorics.MathlibComposition.compositionAsSetEquiv_card_eq_length_sub_one (n : ℕ) (hn : 0 < n) (c : CompositionAsSet n) : ((compositionAsSetEquiv n) c).card + 1 = c.length

Key lemma: for n > 0, the cardinality of the finset associated to a composition equals the length minus 1.

This follows from the structure of the compositionAsSetEquiv: it extracts the "interior" boundary points of a composition (those between 0 and n), and a composition of length k has exactly k-1 such interior points.

theorem AlgebraicCombinatorics.MathlibComposition.compositionToFinset_card_add_one (n : ℕ) (hn : 0 < n) (c : _root_.Composition n) : ((compositionToFinset n) c).card + 1 = c.length

The cardinality of the associated finset plus 1 equals the composition length.

theorem AlgebraicCombinatorics.MathlibComposition.card_compositions_of_length (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : {c : _root_.Composition n | c.length = k}.card = (n - 1).choose (k - 1)

Theorem thm.fps.comps.num-comps-n-k (using Mathlib's Composition): For n > 0 and k > 0, the number of compositions of n into k parts is C(n-1, k-1).

The proof establishes a bijection between compositions of length k and (k-1)-subsets of Fin (n-1), then uses the formula for counting subsets of a given size.

theorem AlgebraicCombinatorics.Composition.card_ofSizeIntoParts_pos (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : Fintype.card (ofSizeIntoParts n k) = (n - 1).choose (k - 1)

Theorem thm.fps.comps.num-comps-n-k: For n > 0 and k > 0, the number of compositions of n into k parts is Nat.choose (n-1) (k-1).

Note: The source text states this as C(n-1, n-k) = C(n-1, k-1) for n > 0, but C(n-1, n-k) uses integer binomial coefficients where C(-1, -k) = 0 for k > 0. In Lean's Nat.choose with truncating subtraction, Nat.choose (0-1) (0-k) = Nat.choose 0 0 = 1, which is incorrect for the case n = 0, k > 0. Additionally, when n > 0 and k = 0, the formula Nat.choose (n-1) (k-1) = Nat.choose (n-1) 0 = 1, but there are no compositions of n > 0 into 0 parts (the count should be 0).

Therefore, we require both n > 0 and k > 0, and handle edge cases separately.

theorem AlgebraicCombinatorics.Composition.card_ofSizeIntoParts_k_zero (n : ℕ) (hn : 0 < n) : Fintype.card (ofSizeIntoParts n 0) = 0

For n > 0 and k = 0, there are no compositions (since compositions have positive parts, and the sum of zero positive integers is 0, not n).

theorem AlgebraicCombinatorics.Composition.card_ofSizeIntoParts_zero (k : ℕ) : Fintype.card (ofSizeIntoParts 0 k) = if k = 0 then 1 else 0

For n = 0, the only composition is the empty one (into 0 parts). There are no compositions of 0 into k > 0 parts (since all parts must be positive).

instance AlgebraicCombinatorics.Composition.fintypeOfSize (n : ℕ) : Fintype (ofSize n)

The set of all compositions of n is finite.

Equations

• AlgebraicCombinatorics.Composition.fintypeOfSize n = Fintype.ofEquiv (Composition n) (AlgebraicCombinatorics.Composition.equivMathlib n).symm

theorem AlgebraicCombinatorics.Composition.card_ofSize (n : ℕ) : Fintype.card (ofSize n) = if n = 0 then 1 else 2 ^ (n - 1)

Theorem thm.fps.comps.num-comps-n: The number of compositions of n is 2^(n-1) when n > 0, and 1 when n = 0.

This is proved by establishing an equivalence with Mathlib's Composition n and using composition_card from Mathlib.

theorem AlgebraicCombinatorics.Composition.card_ofSize_pos (n : ℕ) (hn : 0 < n) : Fintype.card (ofSize n) = 2 ^ (n - 1)

For n > 0, the number of compositions of n is 2^(n-1).

Weak Compositions

def AlgebraicCombinatorics.WeakComposition : Type

A weak composition is a finite tuple of nonnegative integers.

(Definition def.fps.wcomps, part (a))

Equations

• AlgebraicCombinatorics.WeakComposition = List ℕ

instance AlgebraicCombinatorics.WeakComposition.instInhabited : Inhabited WeakComposition

Equations

• AlgebraicCombinatorics.WeakComposition.instInhabited = { default := [] }

def AlgebraicCombinatorics.WeakComposition.size (α : WeakComposition) : ℕ

The size of a weak composition is the sum of its entries.

(Definition def.fps.wcomps, part (b))

Equations

• α.size = List.sum α

def AlgebraicCombinatorics.WeakComposition.len (α : WeakComposition) : ℕ

The length of a weak composition is the number of parts. (We use len to avoid conflict with List.length.)

(Definition def.fps.wcomps, part (c))

Equations

• α.len = List.length α

Basic @[simp] lemmas for size and len

@[simp]

theorem AlgebraicCombinatorics.WeakComposition.size_nil : size [] = 0

The size of the empty weak composition is 0.

@[simp]

theorem AlgebraicCombinatorics.WeakComposition.len_nil : len [] = 0

The length of the empty weak composition is 0.

@[simp]

theorem AlgebraicCombinatorics.WeakComposition.size_cons (a : ℕ) (α : WeakComposition) : size (a :: α) = a + α.size

The size of a cons weak composition is the head value plus the tail size.

@[simp]

theorem AlgebraicCombinatorics.WeakComposition.len_cons (a : ℕ) (α : WeakComposition) : len (a :: α) = α.len + 1

The length of a cons weak composition is the tail length plus 1.

def AlgebraicCombinatorics.WeakComposition.ofSize (n : ℕ) : Type

A weak composition of n is a weak composition whose size is n.

(Definition def.fps.wcomps, part (d))

Equations

• AlgebraicCombinatorics.WeakComposition.ofSize n = { α : AlgebraicCombinatorics.WeakComposition // α.size = n }

def AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts (n k : ℕ) : Type

A weak composition of n into k parts is a tuple of k nonnegative integers summing to n.

(Definition def.fps.wcomps, part (e))

Equations

• AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts n k = { α : AlgebraicCombinatorics.WeakComposition // α.size = n ∧ α.len = k }

Function representation of weak compositions

def AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts' (n k : ℕ) : Type

Alternative representation of weak compositions as functions Fin k → ℕ. This is equivalent to ofSizeIntoParts n k but easier to work with for cardinality proofs.

Equations

• AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts' n k = { f : Fin k → ℕ // ∑ i : Fin k, f i = n }

theorem AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.ext {n k : ℕ} {x y : ofSizeIntoParts' n k} (h : ↑x = ↑y) : x = y

theorem AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.ext_iff {n k : ℕ} {x y : ofSizeIntoParts' n k} : x = y ↔ ↑x = ↑y

theorem AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.sum_count_eq_card (k : ℕ) (m : Multiset (Fin k)) : ∑ i : Fin k, Multiset.count i m = m.card

Key lemma: sum of counts over a finite type equals cardinality.

def AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.fromSym (n k : ℕ) : Sym (Fin k) n → ofSizeIntoParts' n k

Bijection from Sym (Fin k) n to ofSizeIntoParts' n k.

Equations

• AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.fromSym n k s = ⟨fun (i : Fin k) => Multiset.count i ↑s, ⋯⟩

def AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.toSym (n k : ℕ) : ofSizeIntoParts' n k → Sym (Fin k) n

Bijection from ofSizeIntoParts' n k to Sym (Fin k) n.

Equations

• AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.toSym n k ⟨f, hf⟩ = ⟨∑ i : Fin k, Multiset.replicate (f i) i, ⋯⟩

def AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.equivSym (n k : ℕ) : ofSizeIntoParts' n k ≃ Sym (Fin k) n

Equivalence between ofSizeIntoParts' n k and Sym (Fin k) n.

Equations

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

instance AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.fintype (n k : ℕ) : Fintype (ofSizeIntoParts' n k)

Fintype instance via the equivalence with Sym.

Equations

• AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.fintype n k = Fintype.ofEquiv (Sym (Fin k) n) (AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.equivSym n k).symm

theorem AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts'.card_eq (n k : ℕ) : Fintype.card (ofSizeIntoParts' n k) = (n + k - 1).choose n

Theorem thm.fps.comps.num-wcomps-n-k: The number of weak compositions of n into k parts is Nat.choose (n+k-1) n.

The proof uses the "stars and bars" technique: weak compositions of n into k parts are in bijection with multisets of size n from an alphabet of size k (i.e., Sym (Fin k) n), which are counted by Nat.choose (n+k-1) n.

Equivalence between list and function representations

def AlgebraicCombinatorics.WeakComposition.toFun (α : WeakComposition) (k : ℕ) (hlen : α.len = k) : Fin k → ℕ

Convert a list-based weak composition to a function-based one.

Equations

• α.toFun k hlen i = List.get α (Fin.cast ⋯ i)

def AlgebraicCombinatorics.WeakComposition.ofFun {k : ℕ} (f : Fin k → ℕ) : WeakComposition

Convert a function to a list.

Equations

• AlgebraicCombinatorics.WeakComposition.ofFun f = List.ofFn f

theorem AlgebraicCombinatorics.WeakComposition.ofFun_length {k : ℕ} (f : Fin k → ℕ) : List.length (ofFun f) = k

theorem AlgebraicCombinatorics.WeakComposition.ofFun_get {k : ℕ} (f : Fin k → ℕ) (i : Fin k) : List.get (ofFun f) (Fin.cast ⋯ i) = f i

theorem AlgebraicCombinatorics.WeakComposition.ofFun_sum {k : ℕ} (f : Fin k → ℕ) : List.sum (ofFun f) = ∑ i : Fin k, f i

theorem AlgebraicCombinatorics.WeakComposition.toFun_ofFun {k : ℕ} (f : Fin k → ℕ) : (ofFun f).toFun k ⋯ = f

theorem AlgebraicCombinatorics.WeakComposition.list_sum_eq_finset_sum (l : List ℕ) : l.sum = ∑ i : Fin l.length, l.get i

The sum of a list equals the Finset sum over its indices.

theorem AlgebraicCombinatorics.WeakComposition.ofFun_toFun (α : WeakComposition) (k : ℕ) (hlen : α.len = k) : ofFun (α.toFun k hlen) = α

def AlgebraicCombinatorics.WeakComposition.ofSizeIntoParts_equiv (n k : ℕ) : ofSizeIntoParts n k ≃ ofSizeIntoParts' n k

The two representations (list-based and function-based) are equivalent. The forward direction converts a list [a₀, a₁, ..., aₖ₋₁] to the function i ↦ aᵢ. The backward direction converts a function f : Fin k → ℕ to the list [f(0), f(1), ..., f(k-1)].

Equations

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

instance AlgebraicCombinatorics.WeakComposition.fintypeOfSizeIntoParts (n k : ℕ) : Fintype (ofSizeIntoParts n k)

The set of all weak compositions of n into k parts is finite.

Equations

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

theorem AlgebraicCombinatorics.WeakComposition.card_ofSizeIntoParts (n k : ℕ) : Fintype.card (ofSizeIntoParts n k) = (n + k - 1).choose n

Theorem thm.fps.comps.num-wcomps-n-k (first form): The number of weak compositions of n into k parts is Nat.choose (n+k-1) n.

theorem AlgebraicCombinatorics.WeakComposition.card_ofSizeIntoParts_pos (n k : ℕ) (hk : 0 < k) : Fintype.card (ofSizeIntoParts n k) = (n + k - 1).choose (k - 1)

Alternative form: for k > 0, the number of weak compositions of n into k parts is Nat.choose (n+k-1) (k-1).

theorem AlgebraicCombinatorics.WeakComposition.card_ofSizeIntoParts_zero (n : ℕ) : Fintype.card (ofSizeIntoParts n 0) = if n = 0 then 1 else 0

For k = 0, the only weak composition is the empty one (which has size 0).

def AlgebraicCombinatorics.WeakComposition.toComposition (n k : ℕ) : ofSizeIntoParts n k ≃ Composition.ofSizeIntoParts (n + k) k

Bijection between weak compositions of n into k parts and compositions of n+k into k parts. Adding 1 to each entry of a weak composition gives a composition.

This is the key bijection used in the proof of Theorem thm.fps.comps.num-wcomps-n-k.

Equations

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

Bounded Weak Compositions

def AlgebraicCombinatorics.BoundedWeakComposition (n k p : ℕ) : Type

A weak composition of n into k parts with entries bounded by p (i.e., each entry is in {0, 1, ..., p-1}).

This is used in Theorem thm.fps.comps.num-wpcomps-n-k.

Equations

• AlgebraicCombinatorics.BoundedWeakComposition n k p = { α : Fin k → Fin p // ∑ i : Fin k, ↑(α i) = n }

instance AlgebraicCombinatorics.BoundedWeakComposition.fintype (n k p : ℕ) : Fintype (BoundedWeakComposition n k p)

The set of bounded weak compositions is finite.

Equations

• AlgebraicCombinatorics.BoundedWeakComposition.fintype n k p = Fintype.subtype {α : Fin k → Fin p | ∑ i : Fin k, ↑(α i) = n} ⋯

Generating Function Approach

The proof of Theorem thm.fps.comps.num-wpcomps-n-k uses generating functions. The generating function for bounded weak compositions is W_{k,p} = (∑_{i=0}^{p-1} x^i)^k, which equals ((1-x^p)/(1-x))^k = (1-x^p)^k * (1-x)^{-k}.

Using binomial expansions:

• (1-x^p)^k = ∑_{j=0}^k (-1)^j C(k,j) x^{pj}
• (1-x)^{-k} = ∑_{m≥0} C(m+k-1, m) x^m (via PowerSeries.invOneSubPow)

Convolving these gives the formula.

noncomputable def AlgebraicCombinatorics.BoundedWeakComposition.genFun (k p : ℕ) : PowerSeries ℤ

The generating function for bounded weak compositions.

Equations

• AlgebraicCombinatorics.BoundedWeakComposition.genFun k p = (∑ i ∈ Finset.range p, PowerSeries.X ^ i) ^ k

theorem AlgebraicCombinatorics.BoundedWeakComposition.geom_series_mul_one_sub (p : ℕ) : (∑ i ∈ Finset.range p, PowerSeries.X ^ i) * (1 - PowerSeries.X) = 1 - PowerSeries.X ^ p

The geometric series identity: (∑_{i=0}^{p-1} x^i) * (1 - x) = 1 - x^p.

theorem AlgebraicCombinatorics.BoundedWeakComposition.invOneSubPow_pow (k : ℕ) : PowerSeries.invOneSubPow ℤ 1 ^ k = PowerSeries.invOneSubPow ℤ k

Power of invOneSubPow: (invOneSubPow ℤ 1)^k = invOneSubPow ℤ k.

theorem AlgebraicCombinatorics.BoundedWeakComposition.geom_series_eq_mul_inv (p : ℕ) : ∑ i ∈ Finset.range p, PowerSeries.X ^ i = (1 - PowerSeries.X ^ p) * ↑(PowerSeries.invOneSubPow ℤ 1)

The geometric series equals (1 - X^p) * (1 - X)^{-1}.

theorem AlgebraicCombinatorics.BoundedWeakComposition.genFun_eq (k p : ℕ) : genFun k p = (1 - PowerSeries.X ^ p) ^ k * ↑(PowerSeries.invOneSubPow ℤ k)

The generating function equals (1-X^p)^k * (1-X)^{-k}.

theorem AlgebraicCombinatorics.BoundedWeakComposition.coeff_invOneSubPow (k n : ℕ) (hk : 0 < k) : (PowerSeries.coeff n) ↑(PowerSeries.invOneSubPow ℤ k) = ↑((k - 1 + n).choose (k - 1))

The coefficient of x^n in (1-x)^{-k} for k > 0.

theorem AlgebraicCombinatorics.BoundedWeakComposition.coeff_genFun (n k p : ℕ) : (PowerSeries.coeff n) (genFun k p) = ↑(Fintype.card (BoundedWeakComposition n k p))

Key lemma: the coefficient of x^n in the generating function equals the count.

This is the standard fact that [x^n](∑_{i<p} x^i)^k counts k-tuples in {0,...,p-1}^k summing to n. The proof uses the product rule for power series coefficients.

theorem AlgebraicCombinatorics.BoundedWeakComposition.coeff_genFun_formula (n k p : ℕ) : (PowerSeries.coeff n) (genFun k p) = ∑ j ∈ Finset.range (k + 1) with p * j ≤ n, (-1) ^ j * ↑(k.choose j) * ↑((n - p * j + k - 1).choose (n - p * j))

theorem AlgebraicCombinatorics.BoundedWeakComposition.card (n k p : ℕ) : ↑(Fintype.card (BoundedWeakComposition n k p)) = ∑ j ∈ Finset.range (k + 1) with p * j ≤ n, (-1) ^ j * ↑(k.choose j) * ↑((n - p * j + k - 1).choose (n - p * j))

Theorem thm.fps.comps.num-wpcomps-n-k: The number of k-tuples (α₁, α₂, ..., αₖ) ∈ {0, 1, ..., p-1}^k satisfying α₁ + α₂ + ... + αₖ = n is ∑_{j : p*j ≤ n} (-1)^j * C(k,j) * C(n - p*j + k - 1, n - p*j).

Note: The sum is restricted to j with p * j ≤ n because when p * j > n, the mathematical binomial coefficient C(n - p*j + k - 1, n - p*j) should be 0 (as there are no compositions with negative sum), but Nat.choose with truncating subtraction would give a non-zero value.

Proof Strategy

The proof uses generating functions. The generating function for bounded weak compositions is W_{k,p} = (∑_{i=0}^{p-1} x^i)^k, which equals ((1-x^p)/(1-x))^k = (1-x^p)^k * (1-x)^{-k}.

Using binomial expansions:

• (1-x^p)^k = ∑_{j=0}^k (-1)^j C(k,j) x^{pj}
• (1-x)^{-k} = ∑_{m≥0} C(m+k-1, m) x^m

Convolving these gives the formula.

Binary Strings Identity

theorem AlgebraicCombinatorics.card_boundedWeakComposition_2 (k n : ℕ) : Fintype.card (BoundedWeakComposition n k 2) = k.choose n

The cardinality of BoundedWeakComposition n k 2 (binary k-strings with n ones) is C(k, n). This is because choosing a binary string with n ones is equivalent to choosing which n of the k positions will be 1.

theorem AlgebraicCombinatorics.binom_sum_identity (n k : ℕ) : ↑(k.choose n) = ∑ j ∈ Finset.range (k + 1) with 2 * j ≤ n, (-1) ^ j * ↑(k.choose j) * ↑((n - 2 * j + k - 1).choose (n - 2 * j))

Proposition prop.fps.comps.num-w2comps-n-k-id: For n, k ∈ ℕ, we have C(k, n) = ∑_{j : 2*j ≤ n} (-1)^j * C(k,j) * C(n - 2j + k - 1, n - 2j).

This identity arises from the special case p = 2 of Theorem thm.fps.comps.num-wpcomps-n-k, where we count binary strings (k-tuples of 0s and 1s) with exactly n ones.

Proof Strategy

The proof uses generating functions:

1. Binary k-strings with n ones are counted by C(k, n) (choosing which n positions are 1s)
2. By Theorem thm.fps.comps.num-wpcomps-n-k with p = 2, the count also equals the sum formula
3. The generating function identity (1+X)^k = (1-X²)^k / (1-X)^k underlies this:
   • (1-X²) = (1-X)(1+X), so (1-X²)^k / (1-X)^k = (1+X)^k
   • Coefficient of X^n in (1+X)^k is C(k, n)
   • Coefficient of X^n in (1-X²)^k * (1-X)^{-k} gives the sum formula via convolution

Note: The sum is restricted to j with 2 * j ≤ n because when 2j > n, the term contributes 0 (no valid compositions exist with negative sum).