Mesh patterns in permutations

TheoremProduct formula from the mesh-pattern recurrence#✓fully proved

Let \(R\) be a commutative semiring, let \(x \in R\), let \(0 < k \le n\) be natural numbers, and let \(P(m, r) \in R\) for natural numbers \(m, r\). Natural numbers are mapped into \(R\). Suppose that \(P(k-1, k) = (k-1)!\) and that \(P(m, k) = (x + (m - 1))\,P(m-1, k)\) for every natural number \(m \ge k\). Then

\[P(n, k) = (k-1)! \prod_{i=0}^{n-k} \bigl(x + (k - 1 + i)\bigr).\]

With \(R\) the polynomials over \(\mathbb{N}\) and \(x\) the variable, this is the product formula for the mesh-pattern counting polynomial.

theorem meshPatternGeneratingFunction_eq_factorial_mul_prod_general {R : Type*} [CommSemiring R]
    (P : ℕ → ℕ → R) (n k : ℕ) (x : R)
    (hk : 0 < k) (hnk : k ≤ n)
    (hbase : P (k - 1) k = (Nat.factorial (k - 1) : R))
    (hstep : ∀ m : ℕ, k ≤ m →
      P m k = (x + ((m - 1 : ℕ) : R)) * P (m - 1) k) :
    P n k =
      (Nat.factorial (k - 1) : R) *
        ∏ i ∈ Finset.range (n - k + 1),
          (x + ((k - 1 + i : ℕ) : R))
Sources
Used by 2
Used byDistribution of the canonical mesh-pattern statistic · Product formula from the mesh-pattern recurrence, real case

TheoremProduct formula from the mesh-pattern recurrence, real case#✓fully proved

Let \(0 < k \le n\) be natural numbers, let \(x\) be a real number, and let \(P(m, r, y)\) be real numbers indexed by natural numbers \(m, r\) and a real number \(y\). Suppose that \(P(k-1, k, x) = (k-1)!\) and that \(P(m, k, x) = (x + m - 1)\,P(m-1, k, x)\) for every natural number \(m \ge k\). Then

\[P(n, k, x) = (k-1)! \prod_{i=0}^{n-k} (x + k - 1 + i).\]
theorem meshPatternGeneratingFunction_eq_factorial_mul_prod
    (P : ℕ → ℕ → ℝ → ℝ) (n k : ℕ) (x : ℝ)
    (hk : 0 < k) (hnk : k ≤ n)
    (hbase : P (k - 1) k x = (Nat.factorial (k - 1) : ℝ))
    (hstep : ∀ m : ℕ, k ≤ m →
      P m k x = (x + ((m - 1 : ℕ) : ℝ)) * P (m - 1) k x) :
    P n k x =
      (Nat.factorial (k - 1) : ℝ) *
        ∏ i ∈ Finset.range (n - k + 1),
          (x + ((k - 1 + i : ℕ) : ℝ))
Sources
Uses 1
Proof usesProduct formula from the mesh-pattern recurrence

DefinitionMesh-pattern match#✓fully proved

Let \(\sigma\) be a permutation of \(m\) elements, with positions numbered \(1, \dots, m\), let \(p\) be the position of the largest value of \(\sigma\), and let \(r\) be a natural number. A position \(i\) is a mesh-pattern match of \(\sigma\) with parameter \(r\) when \(\sigma(t) < \sigma(i)\) for every position \(t < i\) and at least \(r - 1\) positions \(t\) with \(i < t < p\) have \(\sigma(t) > \sigma(i)\).

def MatchPred {m : ℕ} (r : ℕ) (σ : Equiv.Perm (Fin m)) (i : Fin m) : Prop :=
  ∃ maxIndex : Fin m,
    (∀ t : Fin m, σ t ≤ σ maxIndex) ∧
    r - 1 ≤ (Finset.univ.filter fun t : Fin m =>
      i < t ∧ t < maxIndex ∧ σ i < σ t).card ∧
    ∀ t : Fin m, t < i → σ t < σ i
Used by 3
Used byCanonical mesh-pattern statistic · Counting permutations by mesh-pattern matches · Stirling-type recursion for the mesh-pattern counting polynomial

DefinitionMesh-pattern zero condition#✓fully proved

Let \(\sigma\) be a permutation of \(m\) elements, with positions numbered \(1, \dots, m\), and let \(r\) be a natural number. The zero condition holds for \(\sigma\) with parameter \(r\) when some position \(p \ge r\) holds the largest value of \(\sigma\).

def ZeroPred {m : ℕ} (r : ℕ) (σ : Equiv.Perm (Fin m)) : Prop :=
  ∃ maxIndex : Fin m,
    (∀ t : Fin m, σ t ≤ σ maxIndex) ∧ r ≤ maxIndex.val + 1
Used by 3
Used byCanonical mesh-pattern statistic · Counting permutations by mesh-pattern matches · Stirling-type recursion for the mesh-pattern counting polynomial

DefinitionCanonical mesh-pattern statistic#✓fully proved

Let \(\sigma\) be a permutation of \(m\) elements, with positions numbered \(1, \dots, m\), and let \(r\) be a natural number. The statistic \(N_r(\sigma)\) is the number of mesh-pattern matches of \(\sigma\) with parameter \(r\), plus \(1\) if the mesh-pattern zero condition holds, that is, if the largest value of \(\sigma\) sits at a position \(p \ge r\).

def meshN {m : ℕ} (r : ℕ) (σ : Equiv.Perm (Fin m)) : ℕ :=
  (Finset.univ.filter (MatchPred r σ)).card + if ZeroPred r σ then 1 else 0
Uses 2 · Used by 4
Statement usesMesh-pattern match · Mesh-pattern zero condition
Used byDistribution of the canonical mesh-pattern statistic · Counting permutations by mesh-pattern matches · Stirling-type recursion for the mesh-pattern counting polynomial · Mesh-pattern counting polynomial

DefinitionMesh-pattern counting polynomial#✓fully proved

For natural numbers \(m\) and \(r\), the polynomial \(P_{m,r}(X) \in \mathbb{N}[X]\) is the sum of \(X^{N_r(\sigma)}\) over all permutations \(\sigma\) of \(m\) elements, where \(N_r(\sigma)\) is the canonical mesh-pattern statistic with parameter \(r\).

noncomputable def PolyN : ℕ → ℕ → Polynomial ℕ := fun m r =>
  ∑ σ : Equiv.Perm (Fin m), (Polynomial.X : Polynomial ℕ) ^ meshN r σ
Uses 1 · Used by 2
Statement usesCanonical mesh-pattern statistic
Used byDistribution of the canonical mesh-pattern statistic · Stirling-type recursion for the mesh-pattern counting polynomial

TheoremStirling-type recursion for the mesh-pattern counting polynomial#✓fully proved

Let \(1 < k \le n\) and \(j > 0\). For a permutation \(\sigma\) of \(m\) elements, with positions numbered \(1, \dots, m\), let \(p\) be the position of its largest value and let \(N_r(\sigma)\) be the number of positions \(i\) such that \(\sigma(t) < \sigma(i)\) for all \(t < i\) and at least \(r - 1\) positions \(t\) with \(i < t < p\) have \(\sigma(t) > \sigma(i)\), plus \(1\) if \(p \ge r\). Let \(P_{m,r}(X) \in \mathbb{N}[X]\) be the sum of \(X^{N_r(\sigma)}\) over all permutations \(\sigma\) of \(m\) elements, and let \(c_{m,r}(s)\) be its coefficient of \(X^s\). Then \(c_{n,k}(j) = (n-1)\,c_{n-1,k}(j) + c_{n-1,k}(j-1)\), \(P_{n,k}(X) = (X + n - 1)\,P_{n-1,k}(X)\), \(c_{n,k}(0) = (n-1)\,c_{n-1,k}(0)\), and \(P_{k-1,k}(X) = (k-1)!\).

MetaMathlibExt.meshPatternCount_stirlingRecursion · 23 lines 
theorem meshPatternCount_stirlingRecursion
    (k n j : ℕ) (hk : 1 < k) (hn : k ≤ n) (hj : 0 < j) :
    let isMeshMatch : {m : ℕ} → ℕ → Equiv.Perm (Fin m) → Fin m → Prop :=
      fun {m} r σ i =>
        ∃ maxIndex : Fin m,
          (∀ t : Fin m, σ t ≤ σ maxIndex) ∧
          r - 1 ≤ (Finset.univ.filter fun t : Fin m =>
            i < t ∧ t < maxIndex ∧ σ i < σ t).card ∧
          ∀ t : Fin m, t < i → σ t < σ i
    let zeroMatches : {m : ℕ} → ℕ → Equiv.Perm (Fin m) → Prop :=
      fun {m} r σ =>
        ∃ maxIndex : Fin m,
          (∀ t : Fin m, σ t ≤ σ maxIndex) ∧ r ≤ maxIndex.val + 1
    let meshCount : {m : ℕ} → ℕ → Equiv.Perm (Fin m) → ℕ :=
      fun {_m} r σ =>
        (Finset.univ.filter (isMeshMatch r σ)).card + if zeroMatches r σ then 1 else 0
    let P : ℕ → ℕ → Polynomial ℕ := fun m r =>
      ∑ σ : Equiv.Perm (Fin m), Polynomial.X ^ meshCount r σ
    let C : ℕ → ℕ → ℕ → ℕ := fun m r s => (P m r).coeff s
    C n k j = (n - 1) * C (n - 1) k j + C (n - 1) k (j - 1) ∧
      P n k = (Polynomial.X + Polynomial.C (n - 1)) * P (n - 1) k ∧
      C n k 0 = (n - 1) * C (n - 1) k 0 ∧
      P (k - 1) k = Polynomial.C (Nat.factorial (k - 1))
Sources
Uses 4 · Used by 1
Proof usesMesh-pattern match · Mesh-pattern counting polynomial · Mesh-pattern zero condition · Canonical mesh-pattern statistic
Used byDistribution of the canonical mesh-pattern statistic

TheoremDistribution of the canonical mesh-pattern statistic#✓fully proved

Let \(2 \le k \le n\) and let \(j\) be a natural number. For a permutation \(\sigma\) of \(\{1, \dots, n\}\) with positions numbered \(1, \dots, n\), let \(p\) be the position of its largest value, and let \(N_k(\sigma)\) be the canonical mesh-pattern statistic: the number of positions \(i\) such that \(\sigma(t) < \sigma(i)\) for all \(t < i\) and at least \(k - 1\) positions \(t\) with \(i < t < p\) have \(\sigma(t) > \sigma(i)\), plus \(1\) if \(p \ge k\). Then the number of permutations \(\sigma\) of \(\{1, \dots, n\}\) with \(N_k(\sigma) = j\) equals \((k-1)!\, c_{k-1}(n, j + k - 1)\), where the unsigned \(r\)-Stirling number of the first kind \(c_r(n, m)\) is the coefficient of \(X^m\) in \(X^r (X + r)(X + r + 1) \cdots (X + n - 1)\).

theorem meshPatternCount_eq_factorial_mul_rStirlingNumber_general
    (n k j : ℕ) (hkn : k ≤ n) (hk : 2 ≤ k) :
    Fintype.card {σ : Equiv.Perm (Fin n) // meshN k σ = j} =
      (k - 1).factorial * rStirlingFirst n (j + k - 1) (k - 1)
Uses 5 · Used by 1
Statement usesCanonical mesh-pattern statistic · Unsigned r-Stirling numbers of the first kind
Proof usesMesh-pattern counting polynomial · Stirling-type recursion for the mesh-pattern counting polynomial · Product formula from the mesh-pattern recurrence
Used byCounting permutations by mesh-pattern matches

TheoremCounting permutations by mesh-pattern matches#✓fully proved

Let \(2 \le k \le n\) and let \(j\) be a natural number. For a permutation \(\sigma\) of \(\{1, \dots, n\}\), let \(p\) be the position of its largest entry, and call a position \(i\) a match if \(\sigma(t) < \sigma(i)\) for every position \(t < i\) and at least \(k - 1\) positions \(q\) with \(i < q < p\) have \(\sigma(q) > \sigma(i)\). Let \(N(\sigma)\) be the number of matches, plus \(1\) if \(p \ge k\). Then the number of permutations \(\sigma\) of \(\{1, \dots, n\}\) with \(N(\sigma) = j\) equals \((k-1)!\, c_{k-1}(n, j + k - 1)\), where the unsigned \(r\)-Stirling number of the first kind \(c_r(n, m)\) is the coefficient of \(X^m\) in \(X^r (X + r)(X + r + 1) \cdots (X + n - 1)\).

MetaMathlibExt.meshPatternCount_eq_factorial_mul_rStirlingNumber · 16 lines 
theorem meshPatternCount_eq_factorial_mul_rStirlingNumber
    (n k j : ℕ) (hkn : k ≤ n) (hk : 2 ≤ k) :
    let isLeftToRightMaximum := fun (σ : Equiv.Perm (Fin n)) (i : Fin n) =>
      ∀ h : Fin n, h < i → σ h < σ i
    let isGlobalMaximum := fun (σ : Equiv.Perm (Fin n)) (i : Fin n) =>
      ∀ h : Fin n, σ h ≤ σ i
    let matchesMeshPattern := fun (σ : Equiv.Perm (Fin n)) (i : Fin n) =>
      isLeftToRightMaximum σ i ∧
        k - 1 ≤ (Finset.univ.filter fun q : Fin n =>
          i < q ∧
            (∀ m : Fin n, isGlobalMaximum σ m → q < m) ∧
            σ i < σ q).card
    Fintype.card {σ : Equiv.Perm (Fin n) //
        (Finset.univ.filter (matchesMeshPattern σ)).card +
          (if ∃ m : Fin n, isGlobalMaximum σ m ∧ k ≤ m.val + 1 then 1 else 0) = j} =
      (k - 1).factorial * rStirlingFirst n (j + k - 1) (k - 1)
Sources
Uses 5
Statement usesUnsigned r-Stirling numbers of the first kind
Proof usesMesh-pattern match · Mesh-pattern zero condition · Canonical mesh-pattern statistic · Distribution of the canonical mesh-pattern statistic
9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.