MC-finite sequences

DefinitionMC-finite sequences#✓fully proved

An integer sequence \(s\) is MC-finite if for every natural number \(m > 0\) it eventually satisfies, modulo \(m\), a linear recurrence with constant integer coefficients: there are natural numbers \(p > 0\) and \(q > 0\) and integers \(c_0, \dots, c_{p-1}\) such that \(s(n + p) \equiv \sum_{i=0}^{p-1} c_i\, s(n + i) \pmod{m}\) for all \(n \ge q\).

def IsMCFinite (s : ℕ → ℤ) : Prop :=
  ∀ m : ℕ, 0 < m →
    ∃ p q : ℕ, 0 < p ∧ 0 < q ∧
      ∃ c : Fin p → ℤ, ∀ n : ℕ, q ≤ n →
        (s (n + p) - ∑ i : Fin p, c i * s (n + i.val)) % (↑m : ℤ) = 0

Sources

• Filmus, Fischer, Makowsky, and Rakita, "MC-Finiteness of Restricted Set Partition Functions," Journal of Integer Sequences 26 (2023), Article 23.7.4, lines 281–286.

Used by 2

Used byP-recursive sequences with leading coefficient 1 are MC-finite · Polynomial recursions give MC-finite sequences

TheoremPolynomial recursions give MC-finite sequences#✓fully proved

Let \(u_0, \dots, u_k\) be integer sequences and let \(P_0, \dots, P_k\) be polynomials with integer coefficients in \(k + 2\) variables such that \(u_i(n+1) = P_i(u_0(n), \dots, u_k(n), n)\) for every \(i \le k\) and every \(n \ge 0\). Then the sequence \(u_0\) is MC-finite.

theorem isMCFinite_of_mvPolynomial_recursion {k : ℕ} (u : Fin (k + 1) → ℕ → ℤ)
    (P : Fin (k + 1) → MvPolynomial (Fin (k + 1) ⊕ Unit) ℤ)
    (hrec : ∀ i : Fin (k + 1), ∀ n : ℕ,
      u i (n + 1) = MvPolynomial.eval
        (Sum.elim (fun j : Fin (k + 1) => u j n) (fun _ : Unit => (↑n : ℤ))) (P i)) :
    IsMCFinite (u 0)

Uses 3 · Used by 1

Statement usesMC-finite sequences

Proof usesEventually periodic sequences · Orbits in a finite set are eventually periodic

Used byPolynomially recursive integer sequences are MC-finite

TheoremP-recursive sequences with leading coefficient 1 are MC-finite#✓fully proved

Let \(s\) be an integer sequence that is P-recursive of order \(k\) with coefficient polynomials \(Q_0, \dots, Q_k\) with integer coefficients, that is, \(Q_0(n)\, s_n = \sum_{i=1}^{k} Q_i(n)\, s_{n-i}\) for every \(n \ge k\). If \(Q_0 = 1\), then \(s\) is MC-finite.

theorem IsPRecursiveSequence.isMCFinite {k : ℕ} {Q : Fin (k + 1) → Polynomial ℤ} {s : ℕ → ℤ}
    (hs : IsPRecursiveSequence k Q s) (hQ : Q 0 = 1) : IsMCFinite s

Uses 5 · Used by 1

Statement usesMC-finite sequences · P-recursive sequences

Proof usesEventually periodic sequences · Orbits in a finite set are eventually periodic · Periodic sequences are eventually periodic

Used byPolynomially recursive integer sequences are MC-finite

TheoremPolynomially recursive integer sequences are MC-finite#✓fully proved

Call an integer sequence \(s\) MC-finite if for every natural number \(m > 0\) there are natural numbers \(p > 0\) and \(q > 0\) and integers \(c_0, \dots, c_{p-1}\) such that \(m\) divides \(s(n + p) - \sum_{i=0}^{p-1} c_i\, s(n + i)\) for all \(n \ge q\). Every integer sequence \(s\) has the following two properties.

(1) If there are \(k \ge 0\), integer sequences \(u_0, \dots, u_k\) with \(s = u_0\), and polynomials \(P_0, \dots, P_k\) with integer coefficients in \(k + 2\) variables such that \(u_i(n+1) = P_i(u_0(n), \dots, u_k(n), n)\) for all \(i \le k\) and all \(n \ge 0\), then \(s\) is MC-finite.

(2) Holonomic case: if there are \(k > 0\) and polynomials \(P_1, \dots, P_k\) with integer coefficients such that \(P_1 \ne 0\), \(P_k \ne 0\) and \(s(n) = \sum_{i=1}^{k} P_i(n)\, s(n - i)\) for all \(n \ge k\), then \(s\) is MC-finite.

MetaMathlibExt.polynomially_recursive_MC_finite · 20 lines

theorem polynomially_recursive_MC_finite
    (s : ℕ → ℤ) :
    ((∃ k : ℕ, ∃ u : Fin (k + 1) → ℕ → ℤ,
        ∃ P : Fin (k + 1) → MvPolynomial (Fin (k + 1) ⊕ Unit) ℤ,
        s = u 0 ∧
        ∀ i : Fin (k + 1), ∀ n : ℕ,
          u i (n + 1) = MvPolynomial.eval
            (Sum.elim (fun j : Fin (k + 1) => u j n) (fun _ : Unit => (↑n : ℤ))) (P i)) →
      ∀ m : ℕ, 0 < m →
        ∃ p q : ℕ, 0 < p ∧ 0 < q ∧
          ∃ c : Fin p → ℤ, ∀ n : ℕ, q ≤ n →
            (s (n + p) - ∑ i : Fin p, c i * s (n + i.val)) % (↑m : ℤ) = 0) ∧
    ((∃ k : ℕ, ∃ P : ℕ → Polynomial ℤ,
        0 < k ∧ P 1 ≠ 0 ∧ P k ≠ 0 ∧
        ∀ n : ℕ, k ≤ n →
          s n = ∑ i : Fin k, (P (i.val + 1)).eval (↑n : ℤ) * s (n - (i.val + 1))) →
      ∀ m : ℕ, 0 < m →
        ∃ p q : ℕ, 0 < p ∧ 0 < q ∧
          ∃ c : Fin p → ℤ, ∀ n : ℕ, q ≤ n →
            (s (n + p) - ∑ i : Fin p, c i * s (n + i.val)) % (↑m : ℤ) = 0)

Sources

• Yuval Filmus, Eldar Fischer, and Johann A. Makowsky, with Vsevolod Rakita, "MC-Finiteness of Restricted Set Partition Functions," Journal of Integer Sequences 26 (2023), Article 23.7.4, Theorem, lines 422–427, with the MC-finite definition at lines 281–286 and the holonomic/PRS definitions at lines 387–412, https://cs.uwaterloo.ca/journals/JIS/VOL26/Makowsky/makowsky16.tex. It follows from isMCFinite_of_mvPolynomial_recursion and IsPRecursiveSequence.isMCFinite; in the holonomic premise the conditions 0 < k, P 1 ≠ 0 and P k ≠ 0 are unused and keep the source's shape.

Uses 2

Proof usesP-recursive sequences with leading coefficient 1 are MC-finite · Polynomial recursions give MC-finite sequences

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.