Peaks in set partitions

DefinitionSurjective restricted-growth strings#✓fully proved

A word \(w = w_0 w_1 \cdots w_{n-1}\) of length \(n\) with letters in \(\{0, 1, \dots, k-1\}\) is a surjective restricted-growth string if every letter \(0, \dots, k-1\) occurs in \(w\) and, for every position \(i\) and every letter \(m < w_i\), some position \(j < i\) has \(w_j = m\).

def IsSurjectiveRestrictedGrowthString {n k : ℕ} (w : Fin n → Fin k) : Prop :=
  Function.Surjective w ∧
    ∀ i : Fin n, ∀ m : Fin k,
      m.val < (w i).val → ∃ j : Fin n, j.val < i.val ∧ w j = m
Used by 5
Used byGenerating function for the total number of non-symmetric peaks in set partitions · Peak generating function for set partitions · Total number of non-symmetric peaks over set partitions with \(k\) blocks · Total number of symmetric peaks over set partitions with \(k\) blocks · Generating function for the total number of symmetric peaks in set partitions

TheoremPeak generating function for set partitions#✓fully proved

Let \(k \ge 1\). Work in the fraction field of the ring \(\mathbb{Z}[q][[x]]\) of power series in \(x\) with coefficients in \(\mathbb{Z}[q]\). For a word \(w = w_0 \cdots w_{n-1}\), let \(\mathrm{pk}(w)\) be the number of positions \(a\) with \(a + 2 < n\) and \(w_a < w_{a+1} > w_{a+2}\), and let \(W_{n,k}\) be the set of surjective restricted-growth strings of length \(n\) with letters in \(\{0, \dots, k-1\}\). Let \(t = 1 + x^2 (1-q)/2\), let \(U_m = U_m(t)\) for \(m \in \mathbb{Z}\), where \(U_m\) is the Chebyshev polynomial of the second kind extended to negative indices by its recurrence (so \(U_{-1} = 0\) and \(U_{-2} = -1\)), and let \(R_j = (U_j - U_{j-1})/(U_{j-1} - U_{j-2})\). Then

\[\sum_{n \ge 0} \sum_{w \in W_{n,k}} q^{\mathrm{pk}(w)} x^n = x^k (1-q)^k \prod_{j=1}^{k} \frac{1 + x + x^2 (1-q) - R_j}{1 + x (1-q) - R_j}.\]

Set partitions of \(\{1, \dots, n\}\) with \(k\) blocks are encoded by the strings in \(W_{n,k}\), and \(\mathrm{pk}(w)\) counts the peaks of the encoded partition. Division is total in the fraction field, so the statement carries no nonvanishing hypotheses.

Proof: Following Mansour and Shattuck, Lemmas 2.1, 2.2, and 2.6 and Theorem 2.7, the proof combines first-occurrence decompositions with the Chebyshev recurrence.

MetaMathlibExt.peak_generating_function_set_partitions · 23 lines 
public theorem peak_generating_function_set_partitions
    (k : ℕ) (hk : 1 ≤ k)
    (t x q : FractionRing (PowerSeries (Polynomial ℤ)))
    (hx : x = algebraMap (PowerSeries (Polynomial ℤ))
      (FractionRing (PowerSeries (Polynomial ℤ))) PowerSeries.X)
    (hq : q = algebraMap (PowerSeries (Polynomial ℤ))
      (FractionRing (PowerSeries (Polynomial ℤ))) (PowerSeries.C Polynomial.X))
    (ht : t = 1 + x ^ 2 * (1 - q) / 2) :
    let U : ℤ → FractionRing (PowerSeries (Polynomial ℤ)) := fun m =>
      (Polynomial.Chebyshev.U (FractionRing (PowerSeries (Polynomial ℤ))) m).eval t
    algebraMap (PowerSeries (Polynomial ℤ))
      (FractionRing (PowerSeries (Polynomial ℤ)))
      (PowerSeries.mk (fun n => ∑ w ∈ Finset.univ.filter
        (fun w : Fin n → Fin k => IsSurjectiveRestrictedGrowthString w),
        Polynomial.X ^ (Finset.filter
          (fun s : Fin n × Fin n × Fin n =>
            s.1.val + 1 = s.2.1.val ∧ s.2.1.val + 1 = s.2.2.val ∧
            w s.1 < w s.2.1 ∧ w s.2.2 < w s.2.1) Finset.univ).card)) =
    x ^ k * (1 - q) ^ k * ∏ j ∈ Finset.Icc 1 k,
      (1 + x + x ^ 2 * (1 - q) -
        (U (j : ℤ) - U ((j : ℤ) - 1)) / (U ((j : ℤ) - 1) - U ((j : ℤ) - 2))) /
      (1 + x * (1 - q) -
        (U (j : ℤ) - U ((j : ℤ) - 1)) / (U ((j : ℤ) - 1) - U ((j : ℤ) - 2)))
Sources
Uses 1
Statement usesSurjective restricted-growth strings

TheoremTotal number of peaks over set partitions#✓fully proved

For natural numbers \(n\) and \(k\), call a word \(\pi = \pi_1 \cdots \pi_n\) on the alphabet \(\{0, \dots, k-1\}\) a restricted growth word if it uses every letter and, for every position \(i\), every letter smaller than \(\pi_i\) occurs among \(\pi_1, \dots, \pi_{i-1}\); these words encode the partitions of \([n]\) into \(k\) blocks. A peak of \(\pi\) is a position \(i\) with \(1 < i < n\) and \(\pi_{i-1} < \pi_i > \pi_{i+1}\). Then the total number of peaks, summed over all restricted growth words of length \(n\) on \(k\) letters, equals

\[\binom{k}{2} S(n-1, k) + \sum_{j=2}^{k} \left(j \binom{j}{2} - \binom{j+1}{3}\right) \sum_{i=3}^{n-k} j^{i-3}\, S(n-i, k),\]

where \(S(m, k)\) is the Stirling number of the second kind, \(n - 1\) is read as \(0\) when \(n = 0\), and the inner sum is empty when \(n - k < 3\).

MetaMathlibExt.total_peaks_canonical · 17 lines 
theorem total_peaks_canonical (n k : ℕ)
    : (∑ f ∈ Finset.univ.filter (fun f : Fin n → Fin k =>
          Function.Surjective f ∧
          ∀ i : Fin n, ∀ m : Fin k,
            m.val < (f i).val → ∃ j : Fin n, j.val < i.val ∧ f j = m),
        (Finset.univ.filter (fun i : Fin n =>
          i.val ≠ 0 ∧
          if h : i.val + 1 < n then
            (f ⟨i.val - 1, lt_of_le_of_lt (Nat.sub_le i.val 1) i.isLt⟩).val <
                (f i).val ∧
              (f ⟨i.val + 1, h⟩).val < (f i).val
          else False)).card) =
      Nat.choose k 2 * Nat.stirlingSecond (n - 1) k +
        ∑ j ∈ Finset.Icc 2 k,
          (j * Nat.choose j 2 - Nat.choose (j + 1) 3) *
            ∑ i ∈ Finset.Icc 3 (n - k),
              j ^ (i - 3) * Nat.stirlingSecond (n - i) k
Sources

DefinitionNon-symmetric peaks of a word#✓fully proved

For a word \(w = w_1 w_2 \cdots w_\ell\) of natural numbers, a non-symmetric peak is a position \(i\) with \(1 < i < \ell\) such that \(w_{i-1} < w_i\), \(w_{i+1} < w_i\) and \(w_{i-1} \ne w_{i+1}\). The non-symmetric peak count of \(w\) is the number of such positions; in particular it is \(0\) when \(\ell < 3\).

A peak with \(w_{i-1} = w_{i+1}\) is a symmetric peak instead.

def nonSymmetricPeakCount : List ℕ → ℕ
  | a :: b :: c :: t =>
      (if a < b ∧ c < b ∧ a ≠ c then 1 else 0) + nonSymmetricPeakCount (b :: c :: t)
  | _ => 0
Sources
  • Walaa Asakly and Noor Kezil, Counting Symmetric and Non-Symmetric Peaks in a Set Partition, INTEGERS 26 (2026), Article A8, Section 1.
Used by 3
Used byGenerating function for the total number of non-symmetric peaks in set partitions · Total number of non-symmetric peaks over set partitions with \(k\) blocks · Peaks of the word \(1322141251\)

TheoremPeaks of the word \(1322141251\)#✓fully proved

The word \(1322141251\) (the list \(1, 3, 2, 2, 1, 4, 1, 2, 5, 1\)) has exactly one symmetric peak, the factor \(141\), and exactly two non-symmetric peaks, the factors \(132\) and \(251\).

theorem symmetricPeakCount_nonSymmetricPeakCount_example :
    symmetricPeakCount [1, 3, 2, 2, 1, 4, 1, 2, 5, 1] = 1 ∧
      nonSymmetricPeakCount [1, 3, 2, 2, 1, 4, 1, 2, 5, 1] = 2
Sources
  • Walaa Asakly and Noor Kezil, Counting Symmetric and Non-Symmetric Peaks in a Set Partition, INTEGERS 26 (2026), Article A8, Section 1.
Uses 2
Statement usesNon-symmetric peaks of a word · Number of symmetric peaks

TheoremGenerating function for the total number of symmetric peaks in set partitions#●ready to prove

Fix \(k \in \mathbb{N}\) and, for each \(n\), let \(P_{n,k}\) be the set of surjective restricted-growth strings of length \(n\) with letters in \(\{0, \dots, k-1\}\); these encode the partitions of \(\{1, \dots, n\}\) into exactly \(k\) blocks. For \(w \in P_{n,k}\) let \(\operatorname{sp}(w)\) be the number of symmetric peaks of \(w\). In the ring \(\mathbb{Z}[[x]]\) of formal power series let \(F_k(x) = \sum_{n \ge 0} |P_{n,k}| x^n\). Then

\[ \sum_{n \ge 0} \Big(\sum_{w \in P_{n,k}} \operatorname{sp}(w)\Big) x^n = \max(k - 1, 0)\, x F_k(x) + F_k(x) \sum_{m=1}^{k} \binom{m}{2} \frac{x^3}{1 - m x}, \]

where \(1/(1 - m x)\) is the inverse of \(1 - m x\) in \(\mathbb{Z}[[x]]\).

If \(SP_k(x, q) = \sum_{n \ge 0} \sum_{w \in P_{n,k}} q^{\operatorname{sp}(w)} x^n\), then \(F_k(x) = SP_k(x, 1)\) and the left side is the derivative of \(SP_k(x, q)\) in \(q\) at \(q = 1\).

public theorem_wanted symmetricPeaks_derivative_generatingFunction (k : ℕ) :
    let SP : ℤ⟦X⟧ := PowerSeries.mk fun n =>
      ((univ.filter fun w : Fin n → Fin k => IsSurjectiveRestrictedGrowthString w).card : ℤ)
    PowerSeries.mk (fun n => ((∑ w ∈ univ.filter
        (fun w : Fin n → Fin k => IsSurjectiveRestrictedGrowthString w),
        symmetricPeakCount (List.ofFn fun i => (w i : ℕ)) : ℕ) : ℤ)) =
      ((k - 1 : ℕ) : ℤ⟦X⟧) * X * SP +
        SP * ∑ m ∈ Icc 1 k, X ^ 3 * ((m.choose 2 : ℕ) : ℤ⟦X⟧) *
          invOfUnit (1 - ((m : ℕ) : ℤ⟦X⟧) * X) 1
Sources
  • Walaa Asakly and Noor Kezil, Counting Symmetric and Non-Symmetric Peaks in a Set Partition, INTEGERS 26 (2026), Article A8, Lemma 1.
Uses 2
Statement usesSurjective restricted-growth strings · Number of symmetric peaks

TheoremGenerating function for the total number of non-symmetric peaks in set partitions#●ready to prove

Fix \(k \in \mathbb{N}\) and, for each \(n\), let \(P_{n,k}\) be the set of surjective restricted-growth strings of length \(n\) with letters in \(\{0, \dots, k-1\}\); these encode the partitions of \(\{1, \dots, n\}\) into exactly \(k\) blocks. For \(w \in P_{n,k}\) let \(\operatorname{nsp}(w)\) be the number of non-symmetric peaks of \(w\). In the ring \(\mathbb{Z}[[x]]\) of formal power series let \(F_k(x) = \sum_{n \ge 0} |P_{n,k}| x^n\). Then

\[ \sum_{n \ge 0} \Big(\sum_{w \in P_{n,k}} \operatorname{nsp}(w)\Big) x^n = \binom{k - 1}{2} x F_k(x) + F_k(x) \sum_{m=3}^{k} 2 \binom{m}{3} \frac{x^3}{1 - m x}, \]

where \(k - 1\) is read as \(0\) when \(k = 0\) and \(1/(1 - m x)\) is the inverse of \(1 - m x\) in \(\mathbb{Z}[[x]]\).

If \(NSP_k(x, q) = \sum_{n \ge 0} \sum_{w \in P_{n,k}} q^{\operatorname{nsp}(w)} x^n\), then \(F_k(x) = NSP_k(x, 1)\) and the left side is the derivative of \(NSP_k(x, q)\) in \(q\) at \(q = 1\).

public theorem_wanted nonSymmetricPeaks_derivative_generatingFunction (k : ℕ) :
    let NSP : ℤ⟦X⟧ := PowerSeries.mk fun n =>
      ((univ.filter fun w : Fin n → Fin k => IsSurjectiveRestrictedGrowthString w).card : ℤ)
    PowerSeries.mk (fun n => ((∑ w ∈ univ.filter
        (fun w : Fin n → Fin k => IsSurjectiveRestrictedGrowthString w),
        nonSymmetricPeakCount (List.ofFn fun i => (w i : ℕ)) : ℕ) : ℤ)) =
      (((k - 1).choose 2 : ℕ) : ℤ⟦X⟧) * X * NSP +
        NSP * ∑ m ∈ Icc 3 k, 2 * X ^ 3 * ((m.choose 3 : ℕ) : ℤ⟦X⟧) *
          invOfUnit (1 - ((m : ℕ) : ℤ⟦X⟧) * X) 1
Sources
  • Walaa Asakly and Noor Kezil, Counting Symmetric and Non-Symmetric Peaks in a Set Partition, INTEGERS 26 (2026), Article A8, Lemma 2.
Uses 2
Statement usesSurjective restricted-growth strings · Non-symmetric peaks of a word

TheoremTotal number of symmetric peaks over set partitions with \(k\) blocks#●ready to prove

For natural numbers \(n\) and \(k\), let \(P_{n,k}\) be the set of surjective restricted-growth strings of length \(n\) with letters in \(\{0, \dots, k-1\}\) (these encode the partitions of \(\{1, \dots, n\}\) into exactly \(k\) blocks). For \(w \in P_{n,k}\) let \(\operatorname{sp}(w)\) be the number of symmetric peaks of \(w\), and denote by \(S(a, b)\) the Stirling numbers of the second kind. Then

\[ \sum_{w \in P_{n,k}} \operatorname{sp}(w) = (k - 1)\, S(n - 1, k) + \sum_{j=2}^{k} \binom{j}{2} \sum_{i=3}^{n-k} j^{i-3}\, S(n - i, k), \]

where the differences \(k - 1\), \(n - 1\) and \(n - k\) of natural numbers are truncated at \(0\).

public theorem_wanted sum_symmetricPeakCount_setPartitions (n k : ℕ) :
    ∑ w ∈ univ.filter (fun w : Fin n → Fin k => IsSurjectiveRestrictedGrowthString w),
        symmetricPeakCount (List.ofFn fun i => (w i : ℕ)) =
      (k - 1) * Nat.stirlingSecond (n - 1) k +
        ∑ j ∈ Icc 2 k, j.choose 2 * ∑ i ∈ Icc 3 (n - k), j ^ (i - 3) * Nat.stirlingSecond (n - i) k
Sources
  • Walaa Asakly and Noor Kezil, Counting Symmetric and Non-Symmetric Peaks in a Set Partition, INTEGERS 26 (2026), Article A8, Corollary 1.
Uses 2
Statement usesSurjective restricted-growth strings · Number of symmetric peaks

TheoremTotal number of non-symmetric peaks over set partitions with \(k\) blocks#●ready to prove

For natural numbers \(n\) and \(k\), let \(P_{n,k}\) be the set of surjective restricted-growth strings of length \(n\) with letters in \(\{0, \dots, k-1\}\) (these encode the partitions of \(\{1, \dots, n\}\) into exactly \(k\) blocks). For \(w \in P_{n,k}\) let \(\operatorname{nsp}(w)\) be the number of non-symmetric peaks of \(w\), and denote by \(S(a, b)\) the Stirling numbers of the second kind. Then

\[ \sum_{w \in P_{n,k}} \operatorname{nsp}(w) = \binom{k - 1}{2} S(n - 1, k) + 2 \sum_{j=3}^{k} \binom{j}{3} \sum_{i=3}^{n-k} j^{i-3}\, S(n - i, k), \]

where the differences \(k - 1\), \(n - 1\) and \(n - k\) of natural numbers are truncated at \(0\).

public theorem_wanted sum_nonSymmetricPeakCount_setPartitions (n k : ℕ) :
    ∑ w ∈ univ.filter (fun w : Fin n → Fin k => IsSurjectiveRestrictedGrowthString w),
        nonSymmetricPeakCount (List.ofFn fun i => (w i : ℕ)) =
      (k - 1).choose 2 * Nat.stirlingSecond (n - 1) k +
        2 * ∑ j ∈ Icc 3 k, j.choose 3 *
          ∑ i ∈ Icc 3 (n - k), j ^ (i - 3) * Nat.stirlingSecond (n - i) k
Sources
  • Walaa Asakly and Noor Kezil, Counting Symmetric and Non-Symmetric Peaks in a Set Partition, INTEGERS 26 (2026), Article A8, Corollary 2.
Uses 2
Statement usesSurjective restricted-growth strings · Non-symmetric peaks of a word
5 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.