Minimal permutations with given descents

TheoremCharacterization of minimal permutations with a given number of descents#✓fully proved

Let \(\sigma\) be a permutation of \(\{1, \dots, n\}\) and let \(d\) be a natural number. A descent of a permutation \(\tau\) of \(\{1, \dots, k\}\) is an index \(1 \le i \le k - 1\) with \(\tau(i+1) < \tau(i)\), and \(\tau\) occurs in \(\sigma\) if there are positions \(\varphi(1) < \dots < \varphi(k)\) in \(\{1, \dots, n\}\) with \(\tau(a) < \tau(b)\) exactly when \(\sigma(\varphi(a)) < \sigma(\varphi(b))\). Then \(\sigma\) has exactly \(d\) descents and no permutation \(\tau\) of \(\{1, \dots, k\}\) with \(0 < k < n\) occurring in \(\sigma\) has exactly \(d\) descents if and only if \(\sigma\) has exactly \(d\) descents and every ascent \(i\) of \(\sigma\) (an index \(1 \le i \le n - 1\) with \(\sigma(i) < \sigma(i+1)\)) satisfies \(2 \le i \le n - 2\) and either \(\sigma(i) < \sigma(i-1) < \sigma(i+2) < \sigma(i+1)\) or \(\sigma(i) < \sigma(i+2) < \sigma(i-1) < \sigma(i+1)\); that is, the entries at positions \(i-1, i, i+1, i+2\) form the pattern \(2143\) or \(3142\).

theorem descent_minimal_iff (n d : ℕ) (σ : ℕ → ℕ)
    (hσ : Set.BijOn σ (Set.Icc 1 n) (Set.Icc 1 n)) :
    ((Finset.filter (fun i => σ (i + 1) < σ i) (Finset.Icc 1 (n - 1))).card = d ∧
      ∀ (k : ℕ) (τ : ℕ → ℕ), 0 < k → k < n → Set.BijOn τ (Set.Icc 1 k) (Set.Icc 1 k) →
        (∃ φ : ℕ → ℕ, Set.MapsTo φ (Set.Icc 1 k) (Set.Icc 1 n) ∧
          (∀ a ∈ Set.Icc 1 k, ∀ b ∈ Set.Icc 1 k, a < b → φ a < φ b) ∧
          ∀ a ∈ Set.Icc 1 k, ∀ b ∈ Set.Icc 1 k, (τ a < τ b ↔ σ (φ a) < σ (φ b))) →
        (Finset.filter (fun i => τ (i + 1) < τ i) (Finset.Icc 1 (k - 1))).card ≠ d) ↔
    ((Finset.filter (fun i => σ (i + 1) < σ i) (Finset.Icc 1 (n - 1))).card = d ∧
      ∀ i ∈ Finset.Icc 1 (n - 1), σ i < σ (i + 1) →
        2 ≤ i ∧ i ≤ n - 2 ∧
          (σ i < σ (i - 1) ∧ σ (i - 1) < σ (i + 2) ∧ σ (i + 2) < σ (i + 1) ∨
            σ i < σ (i + 2) ∧ σ (i + 2) < σ (i - 1) ∧ σ (i - 1) < σ (i + 1)))
Sources

TheoremMinimal permutations of length two more than their number of descents#✓fully proved

For every natural number \(d\), the number of permutations \(\sigma\) of \(\{0, 1, \dots, d + 1\}\) such that \(\sigma\) has exactly \(d\) descents (positions \(0 \le i \le d\) with \(\sigma(i) > \sigma(i + 1)\)) and, for every position \(j\), deleting the entry at position \(j\) leaves a sequence of \(d + 1\) entries with fewer than \(d\) descents, equals \(2^{d+2} - (d + 1)(d + 2) - 2\).

public theorem minimal_permutations_card (d : ℕ) :
    (Finset.univ.filter fun σ : Equiv.Perm (Fin (d + 2)) =>
      (Finset.univ.filter fun i : Fin (d + 1) =>
        σ i.castSucc > σ i.succ).card = d ∧
      ∀ j : Fin (d + 2),
        (Finset.univ.filter fun i : Fin d =>
          σ (j.succAbove i.castSucc) > σ (j.succAbove i.succ)).card < d).card =
      2 ^ (d + 2) - (d + 1) * (d + 2) - 2
Sources
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.