Skip to content

Classical permutation statistics

15 fully proved

Left-to-right and right-to-left extrema

DefinitionNumber of left-to-right maxima#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n-1\}\), \(\mathrm{lmax}(\sigma)\) is the number of positions \(i\) such that \(\sigma(j) < \sigma(i)\) for every position \(j < i\), that is, the number of entries larger than every entry to their left.

def permLeftToRightMaxCount (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter fun i : Fin n => ∀ j : Fin n, j < i → σ j < σ i).card
Sources
  • Dan Li and Sergey Kitaev, King Permutations and Partially Ordered Patterns, INTEGERS 26 (2026), Article A59, Section 1 (statistics).
Used by 6
Used byConstant term of \(A_{P_{j+1}}\) · Generating function of king permutations avoiding \(P_{j+1}\) · Statistics of the permutation \(123\) · Statistics of the permutation \(321\) · Generating function of ten classical statistics over a pair of patterns · Left-to-right and right-to-left extrema of \(132\) and \(213\)

DefinitionNumber of right-to-left maxima#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n - 1\}\) written in one-line notation, \(\operatorname{rmax}(\sigma)\) is the number of positions \(i\) such that \(\sigma(j) < \sigma(i)\) for every position \(j > i\), that is, the number of entries larger than every entry to their right.

def permRightToLeftMaxCount (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter fun i : Fin n => ∀ j : Fin n, i < j → σ j < σ i).card
Sources
  • Dan Li and Sergey Kitaev, King Permutations and Partially Ordered Patterns, INTEGERS 26 (2026), Article A59, Section 1 (statistics).
Used by 6
Used byConstant term of \(A_{P_{j+1}}\) · Generating function of king permutations avoiding \(P_{j+1}\) · Statistics of the permutation \(123\) · Statistics of the permutation \(321\) · Generating function of ten classical statistics over a pair of patterns · Left-to-right and right-to-left extrema of \(132\) and \(213\)

DefinitionNumber of left-to-right minima#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n - 1\}\) written in one-line notation, \(\operatorname{lmin}(\sigma)\) is the number of positions \(i\) such that \(\sigma(i) < \sigma(j)\) for every position \(j < i\), that is, the number of entries smaller than every entry to their left.

def permLeftToRightMinCount (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter fun i : Fin n => ∀ j : Fin n, j < i → σ i < σ j).card
Sources
  • Dan Li and Sergey Kitaev, King Permutations and Partially Ordered Patterns, INTEGERS 26 (2026), Article A59, Section 1 (statistics).
Used by 6
Used byConstant term of \(\bar A_{Q_{j+1}}\) · Generating function of king permutations avoiding \(Q_{j+1}\) · Statistics of the permutation \(123\) · Statistics of the permutation \(321\) · Generating function of ten classical statistics over a pair of patterns · Left-to-right and right-to-left extrema of \(132\) and \(213\)

DefinitionNumber of right-to-left minima#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n - 1\}\) written in one-line notation, \(\operatorname{rmin}(\sigma)\) is the number of positions \(i\) such that \(\sigma(i) < \sigma(j)\) for every position \(j > i\), that is, the number of entries smaller than every entry to their right.

def permRightToLeftMinCount (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter fun i : Fin n => ∀ j : Fin n, i < j → σ i < σ j).card
Sources
  • Dan Li and Sergey Kitaev, King Permutations and Partially Ordered Patterns, INTEGERS 26 (2026), Article A59, Section 1 (statistics).
Used by 6
Used byConstant term of \(\bar A_{Q_{j+1}}\) · Generating function of king permutations avoiding \(Q_{j+1}\) · Statistics of the permutation \(123\) · Statistics of the permutation \(321\) · Generating function of ten classical statistics over a pair of patterns · Left-to-right and right-to-left extrema of \(132\) and \(213\)

Double ascents, double descents, peaks and valleys

DefinitionDouble ascent of a permutation#✓fully proved

Let \(\sigma\) be a permutation of \(\{0, 1, \dots, n-1\}\). A position \(i\) is a double ascent of \(\sigma\) if \(i + 2 < n\) and \(\sigma(i) < \sigma(i+1) < \sigma(i+2)\).

def IsDoubleAscentAt (σ : Equiv.Perm (Fin n)) (i : Fin n) : Prop :=
  ∃ h : i.val + 2 < n, σ i < σ ⟨i.val + 1, by omega⟩ ∧ σ ⟨i.val + 1, by omega⟩ < σ ⟨i.val + 2, h⟩
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (dasc).
Used by 3
Used byLocal shape of a position in a permutation · Number of double ascents · Sum of the four local statistics of a permutation

DefinitionDouble descent of a permutation#✓fully proved

Let \(\sigma\) be a permutation of \(\{0, 1, \dots, n-1\}\). A position \(i\) is a double descent of \(\sigma\) if \(i + 2 < n\) and \(\sigma(i) > \sigma(i+1) > \sigma(i+2)\).

def IsDoubleDescentAt (σ : Equiv.Perm (Fin n)) (i : Fin n) : Prop :=
  ∃ h : i.val + 2 < n, σ ⟨i.val + 1, by omega⟩ < σ i ∧ σ ⟨i.val + 2, h⟩ < σ ⟨i.val + 1, by omega⟩
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (ddes).
Used by 3
Used byLocal shape of a position in a permutation · Sum of the four local statistics of a permutation · Number of double descents

DefinitionPeak of a permutation#✓fully proved

Let \(\sigma\) be a permutation of \(\{0, 1, \dots, n-1\}\). A position \(i\) is a peak of \(\sigma\) if \(i + 2 < n\) and \(\sigma(i) < \sigma(i+1) > \sigma(i+2)\). Thus the peak entry is \(\sigma(i+1)\), and the position recorded is \(i\), that of the first of the three entries.

def IsPeakAt (σ : Equiv.Perm (Fin n)) (i : Fin n) : Prop :=
  ∃ h : i.val + 2 < n, σ i < σ ⟨i.val + 1, by omega⟩ ∧ σ ⟨i.val + 2, h⟩ < σ ⟨i.val + 1, by omega⟩
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (pk).
Used by 3
Used byLocal shape of a position in a permutation · Sum of the four local statistics of a permutation · Number of peaks of a permutation

DefinitionValley of a permutation#✓fully proved

Let \(\sigma\) be a permutation of \(\{0, 1, \dots, n-1\}\). A position \(i\) is a valley of \(\sigma\) if \(i + 2 < n\) and \(\sigma(i) > \sigma(i+1) < \sigma(i+2)\). Thus the valley entry is \(\sigma(i+1)\), and the position recorded is \(i\), that of the first of the three entries.

def IsValleyAt (σ : Equiv.Perm (Fin n)) (i : Fin n) : Prop :=
  ∃ h : i.val + 2 < n, σ ⟨i.val + 1, by omega⟩ < σ i ∧ σ ⟨i.val + 1, by omega⟩ < σ ⟨i.val + 2, h⟩
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (vl).
Used by 3
Used byLocal shape of a position in a permutation · Sum of the four local statistics of a permutation · Number of valleys of a permutation

DefinitionNumber of double ascents#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n-1\}\), \(\mathrm{dasc}(\sigma)\) is the number of positions \(i\) that are double ascents of \(\sigma\).

def permDoubleAscents (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter (IsDoubleAscentAt σ)).card
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (dasc).
Uses 1 · Used by 4
Statement usesDouble ascent of a permutation
Used byGenerating function of ten classical statistics over a pair of patterns · Double ascent–double descent generating function of a pair of patterns · Double ascents, double descents, peaks and valleys in length three · Sum of the four local statistics of a permutation

DefinitionNumber of double descents#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n-1\}\), \(\mathrm{ddes}(\sigma)\) is the number of positions \(i\) that are double descents of \(\sigma\).

def permDoubleDescents (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter (IsDoubleDescentAt σ)).card
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (ddes).
Uses 1 · Used by 4
Statement usesDouble descent of a permutation
Used byGenerating function of ten classical statistics over a pair of patterns · Double ascent–double descent generating function of a pair of patterns · Double ascents, double descents, peaks and valleys in length three · Sum of the four local statistics of a permutation

DefinitionNumber of peaks of a permutation#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n - 1\}\) written in one-line notation, \(\operatorname{pk}(\sigma)\) is the number of positions \(i\) with \(i + 2 < n\) and \(\sigma(i) < \sigma(i + 1) > \sigma(i + 2)\), that is, the number of peaks of \(\sigma\).

def permPeaks (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter (IsPeakAt σ)).card
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (pk).
Uses 1 · Used by 3
Statement usesPeak of a permutation
Used byGenerating function of ten classical statistics over a pair of patterns · Double ascents, double descents, peaks and valleys in length three · Sum of the four local statistics of a permutation

DefinitionNumber of valleys of a permutation#✓fully proved

For a permutation \(\sigma\) of \(\{0, 1, \dots, n - 1\}\) written in one-line notation, \(\operatorname{vl}(\sigma)\) is the number of positions \(i\) with \(i + 2 < n\) and \(\sigma(i) > \sigma(i + 1) < \sigma(i + 2)\), that is, the number of valleys of \(\sigma\).

def permValleys (σ : Equiv.Perm (Fin n)) : ℕ :=
  (Finset.univ.filter (IsValleyAt σ)).card
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1 (vl).
Uses 1 · Used by 3
Statement usesValley of a permutation
Used byGenerating function of ten classical statistics over a pair of patterns · Double ascents, double descents, peaks and valleys in length three · Sum of the four local statistics of a permutation

TheoremNumber of positions with two successors#✓fully proved

For every natural number \(n\), exactly \(n - 2\) of the positions \(i \in \{0, 1, \dots, n-1\}\) satisfy \(i + 2 < n\), where \(n - 2\) is truncated subtraction (it is \(0\) when \(n < 2\)).

These are the positions at which a permutation of \(\{0, 1, \dots, n-1\}\) can have a double ascent, a double descent, a peak or a valley.

theorem card_filter_add_two_lt (n : ℕ) :
    (Finset.univ.filter fun i : Fin n => i.val + 2 < n).card = n - 2
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1.
Used by 1
Used bySum of the four local statistics of a permutation

TheoremLocal shape of a position in a permutation#✓fully proved

Let \(\sigma\) be a permutation of \(\{0, 1, \dots, n-1\}\) and let \(i\) be a position. If \(i + 2 < n\), then \(i\) is exactly one of a double ascent, a double descent, a peak or a valley of \(\sigma\); otherwise \(i\) is none of them. That is, the number of these four properties that \(i\) has is \(1\) when \(i + 2 < n\) and \(0\) otherwise.

theorem ite_isDoubleAscentAt_add_ite_isDoubleDescentAt_add_ite_isPeakAt_add_ite_isValleyAt
    (σ : Equiv.Perm (Fin n)) (i : Fin n) :
    ((if IsDoubleAscentAt σ i then 1 else 0) + (if IsDoubleDescentAt σ i then 1 else 0) +
        (if IsPeakAt σ i then 1 else 0) + (if IsValleyAt σ i then 1 else 0) : ℕ) =
      if i.val + 2 < n then 1 else 0
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1.
Uses 4 · Used by 1
Statement usesDouble ascent of a permutation · Double descent of a permutation · Peak of a permutation · Valley of a permutation
Used bySum of the four local statistics of a permutation

TheoremSum of the four local statistics of a permutation#✓fully proved

Let \(\sigma\) be a permutation of \(\{0, 1, \dots, n-1\}\), and write \(\mathrm{dasc}(\sigma)\), \(\mathrm{ddes}(\sigma)\), \(\mathrm{pk}(\sigma)\) and \(\mathrm{vl}(\sigma)\) for its numbers of double ascents, double descents, peaks and valleys. Then \(\mathrm{dasc}(\sigma) + \mathrm{ddes}(\sigma) + \mathrm{pk}(\sigma) + \mathrm{vl}(\sigma) = n - 2\), where \(n - 2\) is truncated subtraction (it is \(0\) when \(n < 2\)).

theorem permDoubleAscents_add_permDoubleDescents_add_permPeaks_add_permValleys
    (σ : Equiv.Perm (Fin n)) :
    permDoubleAscents σ + permDoubleDescents σ + permPeaks σ + permValleys σ = n - 2
Sources
  • Han, Joint Distributions of 10 Classical Statistics over Permutations Avoiding Two Patterns of Length 3, INTEGERS 26 (2026), Article A18, Section 1.
Uses 10
Statement usesNumber of double ascents · Number of double descents · Number of peaks of a permutation · Number of valleys of a permutation
Proof usesDouble ascent of a permutation · Double descent of a permutation · Peak of a permutation · Valley of a permutation · Number of positions with two successors · Local shape of a position in a permutation

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.