Permutations counted by odd-indexed Fibonacci numbers

DefinitionClassical pattern containment in a permutation#✓fully proved

Let \(\sigma\) be a permutation of \(\{0, 1, \dots, n-1\}\) and let \(\pi\) be a map from \(\{0, 1, \dots, k-1\}\) to itself. Then \(\sigma\) contains the pattern \(\pi\) if there are positions \(e_0 < e_1 < \dots < e_{k-1}\) in \(\{0, 1, \dots, n-1\}\) such that for all \(i, j < k\), \(\sigma(e_i) < \sigma(e_j)\) holds exactly when \(\pi(i) < \pi(j)\).

def HasPattern {n k : ℕ} (σ : Equiv.Perm (Fin n))
    (π : Fin k → Fin k) : Prop :=
  ∃ e : Fin k → Fin n, (∀ i j : Fin k, i < j → e i < e j) ∧
    ∀ i j : Fin k, σ (e i) < σ (e j) ↔ π i < π j

Used by 12

Used byKing permutations of length at least \(2\) contain \(12\), \(21\), \(132\), \(213\), \(231\) and \(312\) · No king permutation of length at least \(2\) is separable · Ascent–descent generating function of a pair of patterns · Generating function of ten classical statistics over a pair of patterns · Double ascent–double descent generating function of a pair of patterns · Number of permutations avoiding two patterns of length three · \((231, 3124)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Position of the smallest entry in \((231, 3124)\)-avoiding permutations · \((321, 3412)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Smallest entry in the first two positions of \((321, 3412)\)-avoiding permutations · \((321, 4123)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Position of the smallest entry in \((321, 4123)\)-avoiding permutations

DefinitionThe pattern \(321\)#✓fully proved

The pattern \(321\) written with values \(0, 1, 2\): the map from \(\{0, 1, 2\}\) to itself sending \(0 \mapsto 2\), \(1 \mapsto 1\) and \(2 \mapsto 0\).

def pat321 : Fin 3 → Fin 3 := ![2, 1, 0]

Used by 4

Used by\((321, 3412)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Smallest entry in the first two positions of \((321, 3412)\)-avoiding permutations · \((321, 4123)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Position of the smallest entry in \((321, 4123)\)-avoiding permutations

DefinitionThe pattern \(231\)#✓fully proved

The pattern \(231\) written with values \(0, 1, 2\): the map from \(\{0, 1, 2\}\) to itself sending \(0 \mapsto 1\), \(1 \mapsto 2\) and \(2 \mapsto 0\).

def pat231 : Fin 3 → Fin 3 := ![1, 2, 0]

Used by 2

Used by\((231, 3124)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Position of the smallest entry in \((231, 3124)\)-avoiding permutations

DefinitionThe permutation pattern \(4123\)#✓fully proved

The pattern \(4123\) with its values shifted down by one: the map \(\{0, 1, 2, 3\} \to \{0, 1, 2, 3\}\) sending \(0, 1, 2, 3\) to \(3, 0, 1, 2\) respectively.

def pat4123 : Fin 4 → Fin 4 := ![3, 0, 1, 2]

Used by 2

Used by\((321, 4123)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Position of the smallest entry in \((321, 4123)\)-avoiding permutations

DefinitionThe permutation pattern \(3412\)#✓fully proved

The pattern \(3412\) with its values shifted down by one: the map \(\{0, 1, 2, 3\} \to \{0, 1, 2, 3\}\) sending \(0, 1, 2, 3\) to \(2, 3, 0, 1\) respectively.

def pat3412 : Fin 4 → Fin 4 := ![2, 3, 0, 1]

Used by 2

Used by\((321, 3412)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Smallest entry in the first two positions of \((321, 3412)\)-avoiding permutations

DefinitionThe pattern \(3124\)#✓fully proved

The pattern \(3124\) written with values \(0, 1, 2, 3\): the map from \(\{0, 1, 2, 3\}\) to itself sending \(0 \mapsto 2\), \(1 \mapsto 0\), \(2 \mapsto 1\) and \(3 \mapsto 3\).

def pat3124 : Fin 4 → Fin 4 := ![2, 0, 1, 3]

Used by 2

Used by\((231, 3124)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers · Position of the smallest entry in \((231, 3124)\)-avoiding permutations

Theorem\((321, 4123)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers#●ready to prove

For every \(n \ge 1\), the number of permutations of \(\{0, 1, \dots, n-1\}\) that avoid both patterns \(321\) and \(4123\), that is, contain neither of them, is the Fibonacci number \(F_{2n-1}\), where \(F_0 = 0\) and \(F_1 = 1\).

theorem_wanted card_avoid_321_4123 (n : ℕ) (hn : 1 ≤ n) :
    Nat.card {σ : Equiv.Perm (Fin n) //
      ¬ HasPattern σ pat321 ∧ ¬ HasPattern σ pat4123} =
      Nat.fib (2 * n - 1)

Sources

• Juan B. Gil, Felix H. Xu, and William Y. Zhu, "Odd-Indexed Fibonacci Numbers via Pattern-Avoiding Permutations", Proposition 1.

Uses 3

Statement usesClassical pattern containment in a permutation · The pattern \(321\) · The permutation pattern \(4123\)

Theorem\((321, 3412)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers#●ready to prove

For every \(n \ge 1\), the number of permutations of \(\{0, 1, \dots, n-1\}\) that avoid both patterns \(321\) and \(3412\), that is, contain neither of them, is the Fibonacci number \(F_{2n-1}\), where \(F_0 = 0\) and \(F_1 = 1\).

theorem_wanted card_avoid_321_3412 (n : ℕ) (hn : 1 ≤ n) :
    Nat.card {σ : Equiv.Perm (Fin n) //
      ¬ HasPattern σ pat321 ∧ ¬ HasPattern σ pat3412} =
      Nat.fib (2 * n - 1)

Sources

• Juan B. Gil, Felix H. Xu, and William Y. Zhu, "Odd-Indexed Fibonacci Numbers via Pattern-Avoiding Permutations", Proposition 7.

Uses 3

Statement usesClassical pattern containment in a permutation · The pattern \(321\) · The permutation pattern \(3412\)

Theorem\((231, 3124)\)-avoiding permutations are counted by odd-indexed Fibonacci numbers#●ready to prove

For every \(n \ge 1\), the number of permutations of \(\{0, 1, \dots, n-1\}\) that avoid both patterns \(231\) and \(3124\), that is, contain neither of them, is the Fibonacci number \(F_{2n-1}\), where \(F_0 = 0\) and \(F_1 = 1\).

theorem_wanted card_avoid_231_3124 (n : ℕ) (hn : 1 ≤ n) :
    Nat.card {σ : Equiv.Perm (Fin n) //
      ¬ HasPattern σ pat231 ∧ ¬ HasPattern σ pat3124} =
      Nat.fib (2 * n - 1)

Sources

• Juan B. Gil, Felix H. Xu, and William Y. Zhu, "Odd-Indexed Fibonacci Numbers via Pattern-Avoiding Permutations", Proposition 10.

Uses 3

Statement usesClassical pattern containment in a permutation · The pattern \(231\) · The pattern \(3124\)

TheoremPosition of the smallest entry in \((321, 4123)\)-avoiding permutations#●ready to prove

For a natural number \(m\), write \(S_m(321, 4123)\) for the set of permutations of \(\{0, 1, \dots, m-1\}\) that avoid both patterns \(321\) and \(4123\), that is, contain neither of them. Let \(n \ge 1\) and let \(j\) be a position with \(j + 1 < n\). Then the number of permutations \(\sigma \in S_n(321, 4123)\) with \(\sigma(j) = 0\) equals \((j + 1) \cdot |S_{n-j-1}(321, 4123)|\).

In the source, positions and values start at \(1\): with \(k = j + 1\), the number of such permutations with \(\sigma(k) = 1\) is \(k \cdot |S_{n-k}(321, 4123)|\) for \(1 \le k < n\).

theorem_wanted card_avoid_321_4123_pos_zero (n : ℕ)
    (hn : 1 ≤ n) (j : Fin n) (hj : j.val + 1 < n) :
    Nat.card {σ : Equiv.Perm (Fin n) //
      ¬ HasPattern σ pat321 ∧ ¬ HasPattern σ pat4123 ∧
        σ j = ⟨0, hn⟩} =
      (j.val + 1) * Nat.card
        {σ : Equiv.Perm (Fin (n - j.val - 1)) //
          ¬ HasPattern σ pat321 ∧ ¬ HasPattern σ pat4123}

Sources

• Juan B. Gil, Felix H. Xu, and William Y. Zhu, "Odd-Indexed Fibonacci Numbers via Pattern-Avoiding Permutations", Proposition 2.

Uses 3

Statement usesClassical pattern containment in a permutation · The pattern \(321\) · The permutation pattern \(4123\)

TheoremPosition of the smallest entry in \((231, 3124)\)-avoiding permutations#●ready to prove

For a natural number \(m\), write \(S_m(231, 3124)\) for the set of permutations of \(\{0, 1, \dots, m-1\}\) that avoid both patterns \(231\) and \(3124\), that is, contain neither of them. Let \(n \ge 1\) and let \(j\) be a position with \(j + 1 < n\). Then the number of permutations \(\sigma \in S_n(231, 3124)\) with \(\sigma(j) = 0\) equals \((j + 1) \cdot |S_{n-j-1}(231, 3124)|\).

In the source, positions and values start at \(1\): with \(k = j + 1\), the number of such permutations with \(\sigma(k) = 1\) is \(k \cdot |S_{n-k}(231, 3124)|\) for \(1 \le k < n\).

theorem_wanted card_avoid_231_3124_pos_zero (n : ℕ)
    (hn : 1 ≤ n) (j : Fin n) (hj : j.val + 1 < n) :
    Nat.card {σ : Equiv.Perm (Fin n) //
      ¬ HasPattern σ pat231 ∧ ¬ HasPattern σ pat3124 ∧
        σ j = ⟨0, hn⟩} =
      (j.val + 1) * Nat.card
        {σ : Equiv.Perm (Fin (n - j.val - 1)) //
          ¬ HasPattern σ pat231 ∧ ¬ HasPattern σ pat3124}

Sources

• Juan B. Gil, Felix H. Xu, and William Y. Zhu, "Odd-Indexed Fibonacci Numbers via Pattern-Avoiding Permutations", Proposition 11.

Uses 3

Statement usesClassical pattern containment in a permutation · The pattern \(231\) · The pattern \(3124\)

TheoremSmallest entry in the first two positions of \((321, 3412)\)-avoiding permutations#●ready to prove

Let \(n \ge 2\). Among the permutations \(\sigma\) of \(\{0, 1, \dots, n-1\}\) that avoid both patterns \(321\) and \(3412\), that is, contain neither of them, the number with \(\sigma(0) = 0\) and the number with \(\sigma(1) = 0\) are both equal to the Fibonacci number \(F_{2n-3}\), where \(F_0 = 0\) and \(F_1 = 1\).

In the source's indexing from \(1\), these are the permutations with \(\sigma(1) = 1\) and with \(\sigma(2) = 1\).

theorem_wanted card_avoid_321_3412_pos_zero_le (n : ℕ)
    (hn : 2 ≤ n) :
    Nat.card {σ : Equiv.Perm (Fin n) //
      ¬ HasPattern σ pat321 ∧ ¬ HasPattern σ pat3412 ∧
        σ ⟨0, by omega⟩ = ⟨0, by omega⟩} =
      Nat.fib (2 * n - 3) ∧
    Nat.card {σ : Equiv.Perm (Fin n) //
      ¬ HasPattern σ pat321 ∧ ¬ HasPattern σ pat3412 ∧
        σ ⟨1, hn⟩ = ⟨0, by omega⟩} =
      Nat.fib (2 * n - 3)

Sources

• Juan B. Gil, Felix H. Xu, and William Y. Zhu, "Odd-Indexed Fibonacci Numbers via Pattern-Avoiding Permutations", Proposition 8.

Uses 3

Statement usesClassical pattern containment in a permutation · The pattern \(321\) · The permutation pattern \(3412\)

6 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.