Consecutive patterns in words

DefinitionWords avoiding the consecutive pattern \(z, z+1, z\)#✓fully proved

For natural numbers \(k\) and \(n\), \(f_k(n)\) is the number of words \(w_0 w_1 \cdots w_{n-1}\) of length \(n\) over the alphabet \(\{0, 1, \dots, k-1\}\) with no position \(i\) such that \(i + 2 < n\), \(w_{i+1} = w_i + 1\) and \(w_{i+2} = w_i\).

def avoidZZ1Z (k n : ℕ) : ℕ :=
  ((Finset.univ : Finset (Fin n → Fin k)).filter (fun w =>
    ∀ i : Fin n, ∀ h1 : (i : ℕ) + 1 < n,
      ∀ h2 : (i : ℕ) + 2 < n,
        ¬ (w ⟨(i : ℕ) + 2, h2⟩ = w i ∧
          (w ⟨(i : ℕ) + 1, h1⟩ : ℕ) = (w i : ℕ) + 1))).card

Used by 1

Used byRecurrence for words avoiding the pattern \(z, z+1, z\)

TheoremRecurrence for words avoiding the pattern \(z, z+1, z\)#●ready to prove

Let \(k \ge 1\) and, for each natural number \(n\), let \(f_k(n)\) be the number of words of length \(n\) over the alphabet \(\{0, 1, \dots, k-1\}\) that avoid the consecutive pattern \(z, z+1, z\). Then \(f_k(0) = 1\), \(f_k(1) = k\), \(f_k(2) = k^2\), and \(f_k(n) = k f_k(n-1) - f_k(n-2) + f_k(n-3)\) for every \(n \ge 3\).

At \(k = 0\) the recurrence would read \(0 = 1\) at \(n = 3\).

theorem_wanted avoidZZ1Z_spec (k : ℕ) (hk : 1 ≤ k) :
    avoidZZ1Z k 0 = 1 ∧ avoidZZ1Z k 1 = k ∧
      avoidZZ1Z k 2 = k ^ 2 ∧
      ∀ n : ℕ, 3 ≤ n →
        (avoidZZ1Z k n : ℤ) =
          (k : ℤ) * avoidZZ1Z k (n - 1) -
            avoidZZ1Z k (n - 2) + avoidZZ1Z k (n - 3)

Sources

• Sela Fried, "Proofs of Several Conjectures From the OEIS", Theorem 3.

Uses 1

Statement usesWords avoiding the consecutive pattern \(z, z+1, z\)

TheoremBit length of \(\binom{2^n}{2^{n-1}}\)#●ready to prove

For every integer \(n \ge 1\), the binary expansion of the binomial coefficient \(\binom{2^n}{2^{n-1}}\) has exactly \(2^n - \lfloor n/2 \rfloor\) digits.

theorem_wanted size_choose_two_pow (n : ℕ) (hn : 1 ≤ n) :
    Nat.size (Nat.choose (2 ^ n) (2 ^ (n - 1))) =
      2 ^ n - n / 2

Sources

• Sela Fried, "Proofs of Several Conjectures From the OEIS", Theorem 6.

TheoremFloor of a sum of cube roots#●ready to prove

For every integer \(m \ge 1\), the sum \(S_m = \sum_{i=1}^{10^{3m}} i^{1/3}\) of the real cube roots of \(1, 2, \dots, 10^{3m}\) satisfies

\[\lfloor S_m \rfloor = \frac{3 \cdot 10^{4m}}{4} + 5 \cdot 10^{m-1} - 1.\]

theorem_wanted floor_sum_cbrt (m : ℕ) (hm : 1 ≤ m) :
    Nat.floor (∑ i ∈ Finset.Icc (1 : ℕ) (10 ^ (3 * m)),
        (i : ℝ) ^ (1 / 3 : ℝ)) =
      3 * 10 ^ (4 * m) / 4 + 5 * 10 ^ (m - 1) - 1

Sources

• Sela Fried, "Proofs of Several Conjectures From the OEIS", Theorem 7.

1 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.