Schreier sets

DefinitionNumber of (p, q)-Schreier sets with given maximum#✓fully proved

For natural numbers \(p\), \(q\) and \(n\), \(|S^{p/q}_n|\) is the number of \((p, q)\)-Schreier sets with maximum \(n\), that is, of subsets \(F \subseteq \{1, \dots, n\}\) with \(n \in F\) and \(p|F| \le qx\) for every \(x \in F\) (equivalently, \(p|F| \le q \min F\)).

def schreierCount (p q n : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter fun F => n ∈ F ∧ ∀ x ∈ F, p * F.card ≤ q * x).card

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 1.

Used by 5

Used byMaximal \((1, q)\)-Schreier sets counted by \((1, q)\)-Schreier sets · Counting \((p, 1)\)-Schreier sets by maximal \((p, 1)\)-Schreier sets · Schreier counts as Padovan-like sequences · Closed formula and recurrence for Schreier counts · Small values of the (1, 2)-Schreier counts

DefinitionNumber of maximal \((p, q)\)-Schreier sets#✓fully proved

For natural numbers \(p\), \(q\) and \(n\), \(|M^{p/q}_n|\) is the number of maximal \((p, q)\)-Schreier sets with maximum \(n\), that is, of sets \(F \subseteq \{1, \dots, n\}\) with \(n \in F\) and \(q \min F = p |F|\).

def maximalSchreierCount (p q n : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter fun F =>
    n ∈ F ∧ (∀ x ∈ F, p * F.card ≤ q * x) ∧ ∃ x ∈ F, q * x = p * F.card).card

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 1.

Used by 5

Used byMaximal \((1, q)\)-Schreier sets counted by \((1, q)\)-Schreier sets · Closed form and recurrence for maximal \((p, q)\)-Schreier sets · Counting \((p, 1)\)-Schreier sets by maximal \((p, 1)\)-Schreier sets · Schreier counts as Padovan-like sequences · Small values of the (1, 2)-Schreier counts

DefinitionPadovan-like sequence for Schreier sets#✓fully proved

For natural numbers \(p\) and \(q\), the sequence \(a_{p,q,n}\), \(n \ge 0\), is defined as follows. If \(q \ge 1\) and \(n \ge p + q\), then \(a_{p,q,n} = a_{p,q,n-q} + a_{p,q,n-p-q}\). Otherwise, if \(p \ge q\), then \(a_{p,q,n} = 0\) for \(n < p - q\) and \(a_{p,q,n} = 1\) for \(n \ge p - q\); and if \(p < q\), then \(a_{p,q,n} = 1\) for \(n < 2p\) and \(a_{p,q,n} = 2\) for \(n \ge 2p\).

def schreierPadovan (p q : ℕ) : ℕ → ℕ
  | n =>
    if _h : p + q ≤ n ∧ 0 < q then
      schreierPadovan p q (n - q) + schreierPadovan p q (n - p - q)
    else if q ≤ p then (if n + q < p then 0 else 1) else (if n < 2 * p then 1 else 2)
  decreasing_by all_goals omega

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 1.

Used by 3

Used bySchreier counts as Padovan-like sequences · Recurrence for the Padovan-like sequence · Small values of the Padovan-like sequences

DefinitionPadovan-like sequence of maximal Schreier sets#✓fully proved

For natural numbers \(p\) and \(q\), the sequence \(a^{(m)}_{p,q,n}\), \(n \ge 0\), is defined as follows. If \(q \ge 1\) and \(n \ge p + q\), then \(a^{(m)}_{p,q,n} = a^{(m)}_{p,q,n-q} + a^{(m)}_{p,q,n-p-q}\). Otherwise, if \(q \le p\), then \(a^{(m)}_{p,q,n}\) is \(1\) for \(n = p - q\) and \(0\) for every other \(n\), and if \(p < q\), then \(a^{(m)}_{p,q,n}\) is \(1\) for \(n = 2p\) and \(0\) for every other \(n\).

def maximalSchreierPadovan (p q : ℕ) : ℕ → ℕ
  | n =>
    if _h : p + q ≤ n ∧ 0 < q then
      maximalSchreierPadovan p q (n - q) + maximalSchreierPadovan p q (n - p - q)
    else if q ≤ p then (if n + q = p then 1 else 0) else (if n = 2 * p then 1 else 0)
  decreasing_by all_goals omega

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 1.

Used by 3

Used byRecurrence for the Padovan-like sequence of maximal Schreier sets · First values of the Padovan-like sequences of maximal Schreier sets · Schreier counts as Padovan-like sequences

TheoremRecurrence for the Padovan-like sequence#✓fully proved

For natural numbers \(p\), \(q\) and \(n\) with \(q \ge 1\) and \(n \ge p + q\), the Padovan-like sequence satisfies \(a_{p,q,n} = a_{p,q,n-q} + a_{p,q,n-p-q}\).

theorem schreierPadovan_rec {p q n : ℕ} (hq : 0 < q) (hn : p + q ≤ n) :
    schreierPadovan p q n = schreierPadovan p q (n - q) + schreierPadovan p q (n - p - q)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 1.

Uses 1

Statement usesPadovan-like sequence for Schreier sets

TheoremRecurrence for the Padovan-like sequence of maximal Schreier sets#✓fully proved

For natural numbers \(p\), \(q\) and \(n\) with \(q \ge 1\) and \(n \ge p + q\), the Padovan-like sequence \(a^{(m)}_{p,q,n}\) of maximal Schreier sets satisfies \(a^{(m)}_{p,q,n} = a^{(m)}_{p,q,n-q} + a^{(m)}_{p,q,n-p-q}\).

theorem maximalSchreierPadovan_rec {p q n : ℕ} (hq : 0 < q) (hn : p + q ≤ n) :
    maximalSchreierPadovan p q n =
      maximalSchreierPadovan p q (n - q) + maximalSchreierPadovan p q (n - p - q)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 1.

Uses 1

Statement usesPadovan-like sequence of maximal Schreier sets

TheoremSmall values of the Padovan-like sequences#✓fully proved

For \(n = 0, 1, \dots, 7\), the Padovan-like sequence \(a_{1,2,n}\) takes the values \(1, 1, 2, 2, 3, 4, 5, 7\), and \(a_{2,1,n}\) takes the values \(0, 1, 1, 1, 2, 3, 4, 6\).

theorem schreierPadovan_small :
    (List.range 8).map (schreierPadovan 1 2) = [1, 1, 2, 2, 3, 4, 5, 7] ∧
      (List.range 8).map (schreierPadovan 2 1) = [0, 1, 1, 1, 2, 3, 4, 6]

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Table 3.

Uses 1

Statement usesPadovan-like sequence for Schreier sets

TheoremFirst values of the Padovan-like sequences of maximal Schreier sets#✓fully proved

For \(n = 0, 1, \dots, 7\), the Padovan-like sequence \(a^{(m)}_{1,2,n}\) of maximal Schreier sets takes the values \(0, 0, 1, 0, 1, 1, 1, 2\), and \(a^{(m)}_{2,1,n}\) takes the values \(0, 1, 0, 0, 1, 1, 1, 2\).

theorem maximalSchreierPadovan_small :
    (List.range 8).map (maximalSchreierPadovan 1 2) = [0, 0, 1, 0, 1, 1, 1, 2] ∧
      (List.range 8).map (maximalSchreierPadovan 2 1) = [0, 1, 0, 0, 1, 1, 1, 2]

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Table 4.

Uses 1

Statement usesPadovan-like sequence of maximal Schreier sets

TheoremSmall values of the (1, 2)-Schreier counts#✓fully proved

For \(n = 1, 2, 3, 4\), the number \(|S^{1/2}_n|\) of \((1, 2)\)-Schreier sets with maximum \(n\) takes the values \(1, 2, 3, 5\), and the number \(|M^{1/2}_n|\) of maximal \((1, 2)\)-Schreier sets with maximum \(n\) takes the values \(0, 1, 1, 1\).

theorem schreierCount_one_two_small :
    (List.range 4).map (fun n => schreierCount 1 2 (n + 1)) = [1, 2, 3, 5] ∧
      (List.range 4).map (fun n => maximalSchreierCount 1 2 (n + 1)) = [0, 1, 1, 1]

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Tables 1 and 2.

Uses 2

Statement usesNumber of maximal \((p, q)\)-Schreier sets · Number of (p, q)-Schreier sets with given maximum

DefinitionSequences satisfying a polynomial#✓fully proved

Let \(P = c_0 + c_1 x + \dots + c_r x^r\) be a real polynomial, where \(r\) is the degree of \(P\) (and \(r = 0\) for \(P = 0\)). A real sequence \((a_n)_{n \ge 0}\) satisfies \(P\) if \(c_0 a_n + c_1 a_{n-1} + \dots + c_r a_{n-r} = 0\) for every \(n \ge r\).

def SatisfiesPoly (P : Polynomial ℝ) (a : ℕ → ℝ) : Prop :=
  ∀ n, P.natDegree ≤ n → ∑ i ∈ Finset.range (P.natDegree + 1), P.coeff i * a (n - i) = 0

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 4, Definition 4.

Used by 2

Used byA sequence satisfying a polynomial satisfies its multiples · Every sequence satisfies the zero polynomial

TheoremEvery sequence satisfies the zero polynomial#✓fully proved

Every real sequence \((a_n)_{n \ge 0}\) satisfies the zero polynomial.

theorem satisfiesPoly_zero (a : ℕ → ℝ) : SatisfiesPoly 0 a

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Section 4, Definition 4.

Uses 1

Statement usesSequences satisfying a polynomial

TheoremSchreier counts as Padovan-like sequences#●ready to prove

Write \(a_{p,q,k}\) and \(a^{(m)}_{p,q,k}\) for the Padovan-like sequences for Schreier sets and for maximal Schreier sets. For positive integers \(p\), \(q\) and \(n\), the number \(|S^{p/q}_n|\) of \((p, q)\)-Schreier sets with maximum \(n\) equals \(a_{p,q,(n-1)q}\), and the number \(|M^{p/q}_n|\) of maximal \((p, q)\)-Schreier sets with maximum \(n\) equals \(a^{(m)}_{p,q,(n-1)q}\).

public theorem_wanted schreierCount_eq_schreierPadovan {p q n : ℕ} (hp : 1 ≤ p) (hq : 1 ≤ q)
    (hn : 1 ≤ n) :
    schreierCount p q n = schreierPadovan p q ((n - 1) * q) ∧
      maximalSchreierCount p q n = maximalSchreierPadovan p q ((n - 1) * q)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Theorem 1 (jis-2026-26.2.2-thm-1).

Uses 4

Statement usesNumber of maximal \((p, q)\)-Schreier sets · Padovan-like sequence of maximal Schreier sets · Number of (p, q)-Schreier sets with given maximum · Padovan-like sequence for Schreier sets

TheoremClosed formula and recurrence for Schreier counts#●ready to prove

Let \(p\) and \(q\) be positive integers, and write \(|S^{p/q}_n|\) for the number of \((p, q)\)-Schreier sets with maximum \(n\). For every natural number \(n\),

\[|S^{p/q}_n| = \sum_{i=1}^{\lfloor (n+1)q/(p+q) \rfloor} \binom{n - \lceil pi/q \rceil}{i - 1},\]

and for every \(n \ge p + q + 1\),

\[|S^{p/q}_n| = \sum_{i=1}^{q} (-1)^{i+1} \binom{q}{i} |S^{p/q}_{n-i}| + |S^{p/q}_{n-(p+q)}|.\]

The printed initial-term formula has \(\lceil ni/q \rceil\) in place of \(\lceil pi/q \rceil\), which is false (for \(p = 1\), \(q = 2\), \(n = 2\) one has \(|S^{1/2}_2| = 2\) but the printed sum is \(1\)); \(\lceil pi/q \rceil\) is the paper's own formula (Section 3, equation for \(|S^{p/q}_n|\)). The corollary states the formula for \(1 \le n \le p + q\); it holds for every \(n\), so the range restriction is dropped.

public theorem_wanted schreierCount_formula_and_recurrence {p q : ℕ} (hp : 1 ≤ p) (hq : 1 ≤ q) :
    (∀ n, schreierCount p q n =
      ∑ i ∈ Finset.Icc 1 ((n + 1) * q / (p + q)), (n - (p * i + q - 1) / q).choose (i - 1)) ∧
    ∀ n, p + q + 1 ≤ n →
      (schreierCount p q n : ℤ) =
        ∑ i ∈ Finset.Icc 1 q, (-1) ^ (i + 1) * (q.choose i : ℤ) * schreierCount p q (n - i) +
          schreierCount p q (n - (p + q))

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Corollary 2 (jis-2026-26.2.2-cor-2).

Uses 1

Statement usesNumber of (p, q)-Schreier sets with given maximum

TheoremClosed form and recurrence for maximal \((p, q)\)-Schreier sets#●ready to prove

Let \(p\) and \(q\) be positive integers, put \(p' = p / \gcd(p, q)\) and \(q' = q / \gcd(p, q)\), and for each \(n\) let \(|M^{p/q}_n|\) be the number of maximal \((p, q)\)-Schreier sets with maximum \(n\), that is, of sets \(F \subseteq \{1, \dots, n\}\) with \(n \in F\) and \(q \min F = p |F|\). For each \(n\), let \(K_n\) be the set of integers \(k\) with \(1 \le k \le \lfloor (n+1)/(p'+q') \rfloor\) and \(q'k \ge 2\), and let \(\delta_n\) be \(1\) if \(q' = 1\) and \(n = p'\), and \(0\) otherwise. Then for every \(n \ge 0\),

\[|M^{p/q}_n| = \sum_{k \in K_n} \binom{n - p'k - 1}{q'k - 2} + \delta_n,\]

and for every \(n \ge p + q + 1\),

\[|M^{p/q}_n| = \sum_{i=1}^{q} (-1)^{i+1} \binom{q}{i} |M^{p/q}_{n-i}| + |M^{p/q}_{n-(p+q)}|.\]

The paper prints the first formula as a sum over all \(1 \le k \le \lfloor (n+1)/(p'+q') \rfloor\), without \(\delta_n\), and only for \(1 \le n \le p + q\). Read with binomial coefficients vanishing at negative lower index, it fails at \(p = q = n = 1\), where \(|M^{1/1}_1| = 1\) but the sum is \(0\); the term \(\delta_n\) counts the singleton \(\{n\}\), as in equation (10) of the paper's proof of Theorem 1.

public theorem_wanted maximalSchreierCount_formula_and_recurrence {p q : ℕ} (hp : 1 ≤ p)
    (hq : 1 ≤ q) :
    (∀ n, maximalSchreierCount p q n =
      ∑ k ∈ (Finset.Icc 1 ((n + 1) / (p / p.gcd q + q / p.gcd q))).filter
          (fun k => 2 ≤ q / p.gcd q * k),
        (n - p / p.gcd q * k - 1).choose (q / p.gcd q * k - 2) +
      if q / p.gcd q = 1 ∧ n = p / p.gcd q then 1 else 0) ∧
    ∀ n, p + q + 1 ≤ n →
      (maximalSchreierCount p q n : ℤ) =
        ∑ i ∈ Finset.Icc 1 q,
            (-1) ^ (i + 1) * (q.choose i : ℤ) * maximalSchreierCount p q (n - i) +
          maximalSchreierCount p q (n - (p + q))

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Corollary 3 (jis-2026-26.2.2-cor-3).

Uses 1

Statement usesNumber of maximal \((p, q)\)-Schreier sets

TheoremA sequence satisfying a polynomial satisfies its multiples#●ready to prove

Let \(P\) and \(Q\) be real polynomials with \(P \mid Q\). If a real sequence \((a_n)_{n \ge 0}\) satisfies \(P\), then it satisfies \(Q\).

public theorem_wanted SatisfiesPoly.of_dvd {P Q : Polynomial ℝ} {a : ℕ → ℝ}
    (h : SatisfiesPoly P a) (hPQ : P ∣ Q) : SatisfiesPoly Q a

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Lemma 5 (jis-2026-26.2.2-lem-5).

Uses 1

Statement usesSequences satisfying a polynomial

TheoremCounting \((p, 1)\)-Schreier sets by maximal \((p, 1)\)-Schreier sets#●ready to prove

Fix a positive integer \(p\). For each \(m\), let \(|S^{p/1}_m|\) be the number of sets \(F \subseteq \{1, \dots, m\}\) with \(m \in F\) and \(\min F \ge p |F|\), and let \(|M^{p/1}_m|\) be the number of those with \(\min F = p |F|\). Then \(|S^{p/1}_n| = |M^{p/1}_{n+p+1}|\) for every natural number \(n\).

The paper states this for \(n \ge 1\); at \(n = 0\) both sides are \(0\).

public theorem_wanted schreierCount_eq_maximalSchreierCount_add {p : ℕ} (hp : 1 ≤ p) (n : ℕ) :
    schreierCount p 1 n = maximalSchreierCount p 1 (n + p + 1)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Theorem 8 (jis-2026-26.2.2-thm-8).

Uses 2

Statement usesNumber of maximal \((p, q)\)-Schreier sets · Number of (p, q)-Schreier sets with given maximum

TheoremMaximal \((1, q)\)-Schreier sets counted by \((1, q)\)-Schreier sets#●ready to prove

Fix a positive integer \(q\). For each \(m\), let \(|S^{1/q}_m|\) be the number of sets \(F \subseteq \{1, \dots, m\}\) with \(m \in F\) and \(q \min F \ge |F|\), and let \(|M^{1/q}_m|\) be the number of those with \(q \min F = |F|\). Then \(|M^{1/q}_n| = 2|S^{1/q}_n| - |S^{1/q}_{n+1}|\) for every positive integer \(n\).

public theorem_wanted maximalSchreierCount_eq_two_mul_sub {q n : ℕ} (hq : 1 ≤ q) (hn : 1 ≤ n) :
    (maximalSchreierCount 1 q n : ℤ) = 2 * schreierCount 1 q n - schreierCount 1 q (n + 1)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Linear Recurrences of Generalized Schreier Sets Revisited, Journal of Integer Sequences 29 (2026), Article 26.2.2, Theorem 9 (jis-2026-26.2.2-thm-9).

Uses 2

Statement usesNumber of maximal \((p, q)\)-Schreier sets · Number of (p, q)-Schreier sets with given maximum

DefinitionSchreier sets#✓fully proved

A finite set \(A\) of natural numbers is Schreier if \(|A| \le a\) for every \(a \in A\); equivalently, \(A\) is empty or \(\min A \ge |A|\).

def IsSchreier (A : Finset ℕ) : Prop := ∀ a ∈ A, A.card ≤ a

Used by 3

Used bySchreier sets avoiding multiples · Number of Schreier sparse sets with maximum \(n\) · Number of Schreier sparse sets with given minimum and maximum

DefinitionStrong Schreier sets#✓fully proved

For a natural number \(\ell\), a finite set \(A\) of natural numbers is \(\ell\)-strong Schreier if \(\ell |A| + 1 \le a + \ell\) for every \(a \in A\); equivalently, \(A\) is empty or \(\min A \ge \ell |A| - \ell + 1\).

def IsStrongSchreier (l : ℕ) (A : Finset ℕ) : Prop :=
  ∀ a ∈ A, l * A.card + 1 ≤ a + l

Used by 8

Used byThe refined Schreier family \(F_{n,\ell}\) · Refined Schreier sets with a given number of elements · Refined Schreier sets with a given size and minimum · Refined Schreier count · Number of sparse strong Schreier sets with maximum \(n\) · Number of strong Schreier sets of given size with maximum \(n\) · Number of strong Schreier sets with a given maximum · Number of strongly sparse strong Schreier sets with a given maximum

DefinitionSparse sets#✓fully proved

A finite set of natural numbers is sparse if the differences between consecutive elements in increasing order are non-decreasing.

def IsSparse (A : Finset ℕ) : Prop :=
  ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a < b → b < c →
    (∀ x ∈ A, a < x → b ≤ x) → (∀ x ∈ A, b < x → c ≤ x) →
      b - a ≤ c - b

Used by 7

Used byThe refined Schreier family \(F_{n,\ell}\) · Refined Schreier sets with a given number of elements · Refined Schreier sets with a given size and minimum · Refined Schreier count · Number of Schreier sparse sets with maximum \(n\) · Number of Schreier sparse sets with given minimum and maximum · Number of sparse strong Schreier sets with maximum \(n\)

DefinitionStrongly sparse sets#✓fully proved

A finite set of natural numbers is strongly sparse if the differences between consecutive elements in increasing order are strictly increasing.

def IsStronglySparse (A : Finset ℕ) : Prop :=
  ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, a < b → b < c →
    (∀ x ∈ A, a < x → b ≤ x) → (∀ x ∈ A, b < x → c ≤ x) →
      b - a < c - b

Used by 1

Used byNumber of strongly sparse strong Schreier sets with a given maximum

DefinitionPartitions into exactly \(k\) parts#✓fully proved

For natural numbers \(u\) and \(k\), \(p(u, k)\) is the number of partitions of \(u\) into exactly \(k\) parts.

def partitionExactCount (u k : ℕ) : ℕ :=
  (Finset.univ.filter (fun P : Nat.Partition u =>
    P.parts.card = k)).card

Used by 1

Used bySchreier sparse sets with given minimum and maximum

DefinitionThe partition number \(p(u)\)#✓fully proved

For a natural number \(u\), \(p(u)\) is the number of partitions of \(u\), that is, of multisets of positive integers summing to \(u\); in particular \(p(0) = 1\).

def partitionCount (u : ℕ) : ℕ := Fintype.card (Nat.Partition u)

Used by 1

Used byCounting Schreier sparse sets by partition numbers

DefinitionNumber of Schreier sparse sets with given minimum and maximum#✓fully proved

For natural numbers \(n\) and \(m\), \(|F_{n,m}|\) is the number of sets \(F \subseteq \{1, \dots, n\}\) that are Schreier and sparse, contain \(n\), and have minimum \(m\).

def schreierSparseMinCount (n m : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter (fun F => IsSchreier F ∧
    IsSparse F ∧ n ∈ F ∧ m ∈ F ∧ ∀ a ∈ F, m ≤ a)).card

Uses 2 · Used by 1

Statement usesSchreier sets · Sparse sets

Used bySchreier sparse sets with given minimum and maximum

DefinitionNumber of Schreier sparse sets with maximum \(n\)#✓fully proved

For a natural number \(n\), \(|F_n|\) is the number of sets \(F \subseteq \{1, \dots, n\}\) with \(n \in F\) that are Schreier and sparse.

def schreierSparseCount (n : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter (fun F => IsSchreier F ∧
    IsSparse F ∧ n ∈ F)).card

Uses 2 · Used by 1

Statement usesSchreier sets · Sparse sets

Used byCounting Schreier sparse sets by partition numbers

DefinitionNumber of sparse strong Schreier sets with maximum \(n\)#✓fully proved

For natural numbers \(n\) and \(\ell\), \(|A_{n,\ell}|\) is the number of sets \(A \subseteq \{1, \dots, n\}\) with \(n \in A\) that are sparse and \(\ell\)-strong Schreier.

def sparseStrongCount (n l : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter (fun A => n ∈ A ∧
    IsSparse A ∧ IsStrongSchreier l A)).card

Uses 2 · Used by 2

Statement usesSparse sets · Strong Schreier sets

Used bySparse strong Schreier sets and partitions avoiding small parts · Sparse strong Schreier sets as a sum of partition counts

DefinitionNumber of strongly sparse strong Schreier sets with a given maximum#✓fully proved

For natural numbers \(n\) and \(\ell\), \(|A^s_{n,\ell}|\) is the number of sets \(A \subseteq \{1, \dots, n\}\) with \(n \in A\) that are strongly sparse, meaning that the differences between consecutive elements of \(A\) in increasing order are strictly increasing, and \(\ell\)-strong Schreier, meaning that every element of \(A\) is at least \(\ell|A| - \ell + 1\).

def stronglySparseStrongCount (n l : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter (fun A => n ∈ A ∧
    IsStronglySparse A ∧ IsStrongSchreier l A)).card

Uses 2 · Used by 2

Statement usesStrong Schreier sets · Strongly sparse sets

Used byStrongly sparse strong Schreier sets and partitions with restricted parts · Strongly sparse strong Schreier sets and partitions into distinct parts

DefinitionNumber of strong Schreier sets with a given maximum#✓fully proved

For natural numbers \(n\) and \(\ell\), \(|B_{n,\ell}|\) is the number of sets \(B \subseteq \{1, \dots, n\}\) with \(n \in B\) that are \(\ell\)-strong Schreier, that is, every element of \(B\) is at least \(\ell|B| - \ell + 1\).

def strongSchreierCount (n l : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter (fun B => n ∈ B ∧
    IsStrongSchreier l B)).card

Uses 1 · Used by 1

Statement usesStrong Schreier sets

Used byStrong Schreier sets with a given maximum are counted by compositions

DefinitionNumber of strong Schreier sets of given size with maximum \(n\)#✓fully proved

For natural numbers \(n\), \(\ell\) and \(m\), \(|B_{n,\ell,m}|\) is the number of \(\ell\)-strong Schreier sets \(B \subseteq \{1, \dots, n\}\) with \(n \in B\) and exactly \(m\) elements.

def strongSchreierCardCount (n l m : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter (fun B => n ∈ B ∧
    B.card = m ∧ IsStrongSchreier l B)).card

Uses 1 · Used by 1

Statement usesStrong Schreier sets

Used byStrong Schreier sets of given size and compositions

DefinitionPartitions with all parts at least a given size#✓fully proved

For natural numbers \(n\) and \(\ell\), \(|E_{n,\ell}|\) is the number of partitions of \(n\) all of whose parts are at least \(\ell\).

def partitionMinPartCount (n l : ℕ) : ℕ :=
  (Nat.Partition.restricted n (fun x => l ≤ x)).card

Used by 2

Used byPartitions into large parts and the refined Schreier family · Sparse strong Schreier sets as a sum of partition counts

DefinitionPartitions into distinct parts at least \(\ell\)#✓fully proved

For natural numbers \(n\) and \(\ell\), let \(E^d_{n,\ell}\) be the set of partitions of \(n\) into pairwise distinct parts, each at least \(\ell\). This is its number of elements \(|E^d_{n,\ell}|\).

def partitionDistinctMinPartCount (n l : ℕ) : ℕ :=
  (Nat.Partition.restricted n (fun x => l ≤ x) ∩
    Nat.Partition.distincts n).card

Used by 1

Used byStrongly sparse strong Schreier sets and partitions into distinct parts

DefinitionPartitions with a given number of parts, all at least a given size#✓fully proved

For natural numbers \(n\), \(\ell\) and \(k\), \(|E_{n,\ell,k}|\) is the number of partitions of \(n\) into exactly \(k\) parts, all of which are at least \(\ell\).

def partitionMinPartExactCount (n l k : ℕ) : ℕ :=
  ((Nat.Partition.restricted n (fun x => l ≤ x)).filter
    (fun P => P.parts.card = k)).card

Used by 1

Used byPartitions with a fixed number of large parts and refined Schreier sets

DefinitionPartitions with a given gap between the two largest parts#✓fully proved

For natural numbers \(n\), \(\ell\), \(k\) and \(q\), \(|E_{n,\ell,k,q}|\) is the number of partitions of \(n\) into exactly \(k\) parts, all at least \(\ell\), whose largest part exceeds the second largest part (counted with multiplicity) by exactly \(q\); such a partition has at least two parts, so the count is \(0\) for \(k < 2\).

noncomputable def partitionMinPartGapCount (n l k q : ℕ) : ℕ := by
  classical
  exact ((Nat.Partition.restricted n (fun x => l ≤ x)).filter
    (fun P => P.parts.card = k ∧
      ∃ b : ℕ, ∃ rest : Multiset ℕ,
        P.parts = (b + q) ::ₘ b ::ₘ rest ∧
          ∀ x ∈ rest, x ≤ b)).card

Used by 1

Used byRefined Schreier sets with a given minimum and partitions with a given top gap

DefinitionPartitions avoiding parts from 2 up to a bound#✓fully proved

For natural numbers \(n\) and \(\ell\), \(|G_{n,\ell}|\) is the number of partitions of \(n\) none of whose parts lies in \(\{2, \dots, \ell\}\).

def partitionNoSmallPartCount (n l : ℕ) : ℕ :=
  (Nat.Partition.restricted n (fun x => ¬ (2 ≤ x ∧ x ≤ l))).card

Used by 1

Used bySparse strong Schreier sets and partitions avoiding small parts

DefinitionPartitions avoiding parts from 2 up to a bound and large even parts#✓fully proved

For natural numbers \(n\) and \(\ell\), \(|H_{n,\ell}|\) is the number of partitions of \(n\) none of whose parts lies in \(\{2, \dots, \ell\}\) and none of whose parts is an even number greater than \(2\ell\).

def partitionNoSmallNoEvenCount (n l : ℕ) : ℕ :=
  (Nat.Partition.restricted n
    (fun x => ¬ (2 ≤ x ∧ x ≤ l) ∧ (Even x → x ≤ 2 * l))).card

Used by 1

Used byStrongly sparse strong Schreier sets and partitions with restricted parts

DefinitionCompositions with exactly \(s\) parts, each at least \(v\)#✓fully proved

For natural numbers \(u\), \(v\) and \(s\), \(c(u, v, s)\) is the number of compositions of \(u\) (ordered sequences of positive integers summing to \(u\)) into exactly \(s\) parts, each at least \(v\).

def compositionMinPartExactCount (u v s : ℕ) : ℕ :=
  Fintype.card {c : Composition u //
    (∀ x ∈ c.blocks, v ≤ x) ∧ c.length = s}

Used by 1

Used byStrong Schreier sets of given size and compositions

DefinitionCompositions with parts at least \(v\)#✓fully proved

For natural numbers \(u\) and \(v\), \(c(u, v)\) is the number of compositions of \(u\) (ordered sequences of positive integers summing to \(u\)) all of whose parts are at least \(v\).

def compositionMinPartCount (u v : ℕ) : ℕ :=
  Fintype.card {c : Composition u // ∀ x ∈ c.blocks, v ≤ x}

Used by 1

Used byStrong Schreier sets with a given maximum are counted by compositions

DefinitionThe refined Schreier family \(F_{n,\ell}\)#✓fully proved

For natural numbers \(n\) and \(\ell\), a finite set \(A\) of natural numbers belongs to \(F_{n,\ell}\) if \(n + 1\) is the largest element of \(A\), \(A\) has at least three elements, \(A\) is sparse and \(\ell\)-strong Schreier, and the two largest elements \(a < b\) of \(A\) below \(n + 1\) satisfy \(n + 1 + a = 2b\).

def IsRefinedSchreier (n l : ℕ) (A : Finset ℕ) : Prop :=
  n + 1 ∈ A ∧ (∀ x ∈ A, x ≤ n + 1) ∧ 3 ≤ A.card ∧ IsSparse A ∧
    IsStrongSchreier l A ∧
      ∃ a ∈ A, ∃ b ∈ A, a < b ∧ b < n + 1 ∧
        (∀ x ∈ A, x ≤ b ∨ x = n + 1) ∧
          (∀ x ∈ A, x ≤ a ∨ x = b ∨ x = n + 1) ∧
            n + 1 + a = 2 * b

Uses 2 · Used by 3

Statement usesSparse sets · Strong Schreier sets

Used byRefined Schreier sets with a given number of elements · Refined Schreier sets with a given size and minimum · Refined Schreier count

DefinitionRefined Schreier count#✓fully proved

For natural numbers \(n\) and \(\ell\), \(|F_{n,\ell}|\) is the number of finite sets \(A\) of natural numbers such that \(n + 1 \in A\), every element of \(A\) is at most \(n + 1\), \(A\) has at least three elements, \(A\) is sparse and \(\ell\)-strong Schreier, and the two largest elements \(a < b\) of \(A\) below \(n + 1\) satisfy \(n + 1 + a = 2b\). Every such set is contained in \(\{0, \dots, n + 1\}\).

def refinedSchreierCount (n l : ℕ) : ℕ :=
  ((Finset.Icc 0 (n + 1)).powerset.filter
    (IsRefinedSchreier n l)).card

Uses 3 · Used by 1

Statement usesThe refined Schreier family \(F_{n,\ell}\) · Sparse sets · Strong Schreier sets

Used byPartitions into large parts and the refined Schreier family

DefinitionRefined Schreier sets with a given number of elements#✓fully proved

For natural numbers \(n\) and \(\ell\), let \(F_{n,\ell}\) be the family of finite sets \(A\) of natural numbers such that \(A\) has largest element \(n + 1\) and at least three elements, \(A\) is sparse (the differences of consecutive elements, in increasing order, are non-decreasing) and \(\ell\)-strong Schreier (\(\ell|A| + 1 \le a + \ell\) for every \(a \in A\)), and the second and third largest elements \(b > a\) of \(A\) satisfy \(n + 1 + a = 2b\). For a natural number \(k\), \(|F_{n,\ell,k}|\) is the number of sets in \(F_{n,\ell}\) with exactly \(k\) elements.

def refinedSchreierCardCount (n l k : ℕ) : ℕ :=
  ((Finset.Icc 0 (n + 1)).powerset.filter
    (fun A => IsRefinedSchreier n l A ∧ A.card = k)).card

Uses 3 · Used by 1

Statement usesThe refined Schreier family \(F_{n,\ell}\) · Sparse sets · Strong Schreier sets

Used byPartitions with a fixed number of large parts and refined Schreier sets

DefinitionRefined Schreier sets with a given size and minimum#✓fully proved

For natural numbers \(n\) and \(\ell\), let \(F_{n,\ell}\) be the family of finite sets \(A\) of natural numbers such that \(A\) has largest element \(n + 1\) and at least three elements, \(A\) is sparse (the differences of consecutive elements, in increasing order, are non-decreasing) and \(\ell\)-strong Schreier (\(\ell|A| + 1 \le a + \ell\) for every \(a \in A\)), and the second and third largest elements \(b > a\) of \(A\) satisfy \(n + 1 + a = 2b\). For natural numbers \(k\) and \(q\), \(|F_{n,\ell,k,q}|\) is the number of sets in \(F_{n,\ell}\) with exactly \(k\) elements whose smallest element is \(q\).

def refinedSchreierCardMinCount (n l k q : ℕ) : ℕ :=
  ((Finset.Icc 0 (n + 1)).powerset.filter
    (fun A => IsRefinedSchreier n l A ∧ A.card = k ∧
      q ∈ A ∧ ∀ x ∈ A, q ≤ x)).card

Uses 3 · Used by 1

Statement usesThe refined Schreier family \(F_{n,\ell}\) · Sparse sets · Strong Schreier sets

Used byRefined Schreier sets with a given minimum and partitions with a given top gap

TheoremSchreier sparse sets with given minimum and maximum#●ready to prove

For natural numbers \(m\) and \(n\) with \(m + 1 \le n\), the number of Schreier sparse sets \(F \subseteq \{1, \dots, n\}\) with \(n \in F\) and \(\min F = m + 1\) equals \(p(n - 1, m)\), the number of partitions of \(n - 1\) into exactly \(m\) parts.

theorem_wanted schreierSparseMinCount_eq (m n : ℕ) (hmn : m + 1 ≤ n) :
    schreierSparseMinCount n (m + 1) = partitionExactCount (n - 1) m

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Proposition 2.

Uses 2

Statement usesPartitions into exactly \(k\) parts · Number of Schreier sparse sets with given minimum and maximum

TheoremCounting Schreier sparse sets by partition numbers#●ready to prove

For every integer \(n \ge 1\), the number of Schreier sparse sets \(F \subseteq \{1, \dots, n\}\) with \(n \in F\) equals \(p(n - 1)\), the number of partitions of \(n - 1\).

theorem_wanted schreierSparseCount_eq (n : ℕ) (hn : 1 ≤ n) :
    schreierSparseCount n = partitionCount (n - 1)

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Corollary 3.

Uses 2

Statement usesThe partition number \(p(u)\) · Number of Schreier sparse sets with maximum \(n\)

TheoremSparse strong Schreier sets as a sum of partition counts#●ready to prove

For every integer \(n \ge 1\) and every natural number \(\ell\), the number of sparse \(\ell\)-strong Schreier sets \(A \subseteq \{1, \dots, n\}\) with \(n \in A\) equals \(\sum_{i=0}^{n-1} |E_{i,\ell+1}|\), where \(|E_{i,\ell+1}|\) is the number of partitions of \(i\) into parts that are all at least \(\ell + 1\).

theorem_wanted sparseStrongCount_eq_sum (n l : ℕ) (hn : 1 ≤ n) :
    sparseStrongCount n l =
      ∑ i ∈ Finset.range n, partitionMinPartCount i (l + 1)

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Theorem 6.

Uses 2

Statement usesPartitions with all parts at least a given size · Number of sparse strong Schreier sets with maximum \(n\)

TheoremStrongly sparse strong Schreier sets and partitions into distinct parts#●ready to prove

For all natural numbers \(n \ge 1\) and \(\ell \ge 0\), the number \(|A^s_{n,\ell}|\) of strongly sparse \(\ell\)-strong Schreier sets \(A \subseteq \{1, \dots, n\}\) with \(n \in A\) equals \(\sum_{i=0}^{n-1} |E^d_{i,\ell+1}|\), where \(|E^d_{i,\ell+1}|\) is the number of partitions of \(i\) into distinct parts that are all at least \(\ell + 1\) (so \(|E^d_{0,\ell+1}| = 1\)). Here \(A\) is strongly sparse when the differences between consecutive elements of \(A\), listed in increasing order, are strictly increasing, and \(\ell\)-strong Schreier when every element of \(A\) is at least \(\ell|A| - \ell + 1\).

theorem_wanted stronglySparseStrongCount_eq_sum (n l : ℕ)
    (hn : 1 ≤ n) :
    stronglySparseStrongCount n l =
      ∑ i ∈ Finset.range n, partitionDistinctMinPartCount i (l + 1)

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Theorem 6.

Uses 2

Statement usesPartitions into distinct parts at least \(\ell\) · Number of strongly sparse strong Schreier sets with a given maximum

TheoremSparse strong Schreier sets and partitions avoiding small parts#●ready to prove

For all integers \(n \ge 1\) and \(\ell \ge 1\), the number of sparse \(\ell\)-strong Schreier sets \(A \subseteq \{1, \dots, n\}\) with \(n \in A\) equals the number of partitions of \(n - 1\) with no part in \(\{2, \dots, \ell\}\).

The identity fails at \(\ell = 0\); the paper's \(\mathbb{N}\) is the positive integers.

theorem_wanted sparseStrongCount_eq_noSmall (n l : ℕ) (hn : 1 ≤ n)
    (hl : 1 ≤ l) :
    sparseStrongCount n l = partitionNoSmallPartCount (n - 1) l

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Theorem 7.

Uses 2

Statement usesPartitions avoiding parts from 2 up to a bound · Number of sparse strong Schreier sets with maximum \(n\)

TheoremStrongly sparse strong Schreier sets and partitions with restricted parts#●ready to prove

For all natural numbers \(n \ge 1\) and \(\ell \ge 1\), the number \(|A^s_{n,\ell}|\) of strongly sparse \(\ell\)-strong Schreier sets \(A \subseteq \{1, \dots, n\}\) with \(n \in A\) equals \(|H_{n-1,\ell}|\), the number of partitions of \(n - 1\) with no part in \(\{2, \dots, \ell\}\) and no even part greater than \(2\ell\). Here \(A\) is strongly sparse when the differences between consecutive elements of \(A\), listed in increasing order, are strictly increasing, and \(\ell\)-strong Schreier when every element of \(A\) is at least \(\ell|A| - \ell + 1\).

theorem_wanted stronglySparseStrongCount_eq_noSmallNoEven (n l : ℕ)
    (hn : 1 ≤ n) (hl : 1 ≤ l) :
    stronglySparseStrongCount n l =
      partitionNoSmallNoEvenCount (n - 1) l

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Theorem 7.

Uses 2

Statement usesPartitions avoiding parts from 2 up to a bound and large even parts · Number of strongly sparse strong Schreier sets with a given maximum

TheoremStrong Schreier sets of given size and compositions#●ready to prove

For all integers \(n \ge 1\) and \(m \ge 1\) and every natural number \(\ell\), the number of \(\ell\)-strong Schreier sets \(B \subseteq \{1, \dots, n\}\) with \(n \in B\) and exactly \(m\) elements equals the number of compositions of \(n + \ell\) into exactly \(m\) parts, each at least \(\ell + 1\).

theorem_wanted strongSchreierCardCount_eq (m n l : ℕ) (hn : 1 ≤ n)
    (hm : 1 ≤ m) :
    strongSchreierCardCount n l m =
      compositionMinPartExactCount (n + l) (l + 1) m

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Theorem 9.

Uses 2

Statement usesCompositions with exactly \(s\) parts, each at least \(v\) · Number of strong Schreier sets of given size with maximum \(n\)

TheoremStrong Schreier sets with a given maximum are counted by compositions#●ready to prove

For all natural numbers \(n \ge 1\) and \(\ell \ge 0\), the number \(|B_{n,\ell}|\) of \(\ell\)-strong Schreier sets \(B \subseteq \{1, \dots, n\}\) with \(n \in B\) equals \(c(n + \ell, \ell + 1)\), the number of compositions of \(n + \ell\) into parts that are all at least \(\ell + 1\). Here a set \(B\) is \(\ell\)-strong Schreier when every element of \(B\) is at least \(\ell|B| - \ell + 1\).

theorem_wanted strongSchreierCount_eq (n l : ℕ) (hn : 1 ≤ n) :
    strongSchreierCount n l = compositionMinPartCount (n + l) (l + 1)

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Theorem 9.

Uses 2

Statement usesCompositions with parts at least \(v\) · Number of strong Schreier sets with a given maximum

TheoremRefined Schreier sets with a given minimum and partitions with a given top gap#●ready to prove

Let \(n\), \(\ell\), \(k\) and \(q\) be natural numbers with \(n \ge \ell + 1\), \(k \ge 2\) and \(q \ge 1\). Let \(F_{n,\ell}\) be the family of finite sets \(A\) of natural numbers such that \(A\) has largest element \(n + 1\) and at least three elements, \(A\) is sparse (the differences of consecutive elements, in increasing order, are non-decreasing) and \(\ell\)-strong Schreier (\(\ell|A| + 1 \le a + \ell\) for every \(a \in A\)), and the second and third largest elements \(b > a\) of \(A\) satisfy \(n + 1 + a = 2b\). Then the number \(|F_{n,\ell,k+1,\ell k+q}|\) of sets in \(F_{n,\ell}\) with exactly \(k + 1\) elements and smallest element \(\ell k + q\) equals the number \(|E_{n,\ell+1,k,q-1}|\) of partitions of \(n\) into exactly \(k\) parts, all at least \(\ell + 1\), whose largest part exceeds the second largest part (counted with multiplicity) by exactly \(q - 1\).

theorem_wanted refinedSchreierCardMinCount_eq (n l k q : ℕ)
    (hn : l + 1 ≤ n) (hk : 2 ≤ k) (hq : 1 ≤ q) :
    refinedSchreierCardMinCount n l (k + 1) (l * k + q) =
      partitionMinPartGapCount n (l + 1) k (q - 1)

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Lemma 11.

Uses 2

Statement usesPartitions with a given gap between the two largest parts · Refined Schreier sets with a given size and minimum

TheoremPartitions with a fixed number of large parts and refined Schreier sets#●ready to prove

Let \(n\), \(\ell\) and \(k\) be natural numbers with \(n \ge \ell + 1\) and \(k \ge 2\). Let \(F_{n,\ell}\) be the family of finite sets \(A\) of natural numbers such that \(A\) has largest element \(n + 1\) and at least three elements, \(A\) is sparse (the differences of consecutive elements, in increasing order, are non-decreasing) and \(\ell\)-strong Schreier (\(\ell|A| + 1 \le a + \ell\) for every \(a \in A\)), and the second and third largest elements \(b > a\) of \(A\) satisfy \(n + 1 + a = 2b\). Then the number \(|E_{n,\ell+1,k}|\) of partitions of \(n\) into exactly \(k\) parts, all at least \(\ell + 1\), equals the number \(|F_{n,\ell,k+1}|\) of sets in \(F_{n,\ell}\) with exactly \(k + 1\) elements.

theorem_wanted partitionMinPartExactCount_eq_refined (n l k : ℕ)
    (hn : l + 1 ≤ n) (hk : 2 ≤ k) :
    partitionMinPartExactCount n (l + 1) k =
      refinedSchreierCardCount n l (k + 1)

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Corollary 12.

Uses 2

Statement usesPartitions with a given number of parts, all at least a given size · Refined Schreier sets with a given number of elements

TheoremPartitions into large parts and the refined Schreier family#●ready to prove

Let \(n\) and \(\ell\) be natural numbers with \(n \ge \ell + 1\). Let \(F_{n,\ell}\) be the family of finite sets \(A\) of natural numbers such that \(A\) has largest element \(n + 1\) and at least three elements, \(A\) is sparse (the differences of consecutive elements, in increasing order, are non-decreasing) and \(\ell\)-strong Schreier (\(\ell|A| + 1 \le a + \ell\) for every \(a \in A\)), and the second and third largest elements \(b > a\) of \(A\) satisfy \(n + 1 + a = 2b\). Then the number \(|E_{n,\ell+1}|\) of partitions of \(n\) into parts that are all at least \(\ell + 1\) equals \(|F_{n,\ell}| + 1\).

theorem_wanted partitionMinPartCount_eq_refined_add_one (n l : ℕ)
    (hn : l + 1 ≤ n) :
    partitionMinPartCount n (l + 1) = refinedSchreierCount n l + 1

Sources

• Kevin Beanland and Hùng Việt Chu, "On Schreier-Type Sets, Partitions, and Compositions", Corollary 13.

Uses 2

Statement usesPartitions with all parts at least a given size · Refined Schreier count

DefinitionGround multiset for Schreier-type multisets#✓fully proved

For natural numbers \(s\) and \(n\), this is the multiset \(\{1^s, \dots, (n - 1)^s, n\}\), in which each of \(1, \dots, n - 1\) has multiplicity \(s\) and \(n\) appears once.

def schreierMultisetPool (s n : ℕ) : Multiset ℕ :=
  (∑ k ∈ Finset.Icc 1 (n - 1), Multiset.replicate s k) + {n}

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 1 (definition of A^{(s)}_{p,n}).

Used by 1

Used byNumber of Schreier-type multisets

DefinitionNumber of Schreier-type multisets#✓fully proved

For natural numbers \(s\), \(p\) and \(n\), \(|A^{(s)}_{p,n}|\) is the number of distinct sub-multisets \(F\) of \(\{1^s, \dots, (n - 1)^s, n\}\) (each of \(1, \dots, n - 1\) with multiplicity \(s\), and \(n\) once) such that \(n \in F\) and every element of \(F\) is at least \(p|F|\), where \(|F|\) counts multiplicity.

def schreierMultisetCount (s p n : ℕ) : ℕ :=
  ((schreierMultisetPool s n).powerset.toFinset.filter fun F =>
    n ∈ F ∧ ∀ x ∈ F, p * Multiset.card F ≤ x).card

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 1 (definition of A^{(s)}_{p,n}).

Uses 1 · Used by 2

Statement usesGround multiset for Schreier-type multisets

Used byFormula and recurrence for Schreier-type multisets · Small values of the Schreier multiset count

TheoremSmall values of the Schreier multiset count#✓fully proved

Let \(|A^{(s)}_{p,n}|\) be the number of distinct sub-multisets \(F\) of \(\{1^s, \dots, (n - 1)^s, n\}\) with \(n \in F\) and every element of \(F\) at least \(p|F|\), where \(|F|\) counts multiplicity. Then \(|A^{(2)}_{1,4}| = 4\) and \(|A^{(2)}_{2,5}| = 2\).

theorem schreierMultisetCount_small :
    schreierMultisetCount 2 1 4 = 4 ∧ schreierMultisetCount 2 2 5 = 2

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Table 1.

Uses 1

Statement usesNumber of Schreier-type multisets

DefinitionCounting colored Schreier-type multisets#✓fully proved

For natural numbers \(s\), \(p\) and \(n\), give each of \(1, \dots, n - 1\) the \(s\) colors \(0, \dots, s - 1\), writing \(k_c\) for \(k\) with color \(c\), and let \(n\) appear once, uncolored. Then \(|B^{(s)}_{p,n}|\) is the number of sets \(F\) of colored integers drawn from \(\{1_0, \dots, 1_{s-1}, \dots, (n-1)_0, \dots, (n-1)_{s-1}, n\}\) that contain \(n\) and satisfy \(\min F \ge p|F|\), where the minimum is taken over the underlying integers.

def coloredSchreierMultisetCount (s p n : ℕ) : ℕ :=
  ((Finset.Icc 1 (n - 1) ×ˢ Finset.range s ∪ {(n, 0)}).powerset.filter fun F =>
    (n, 0) ∈ F ∧ ∀ x ∈ F, p * F.card ≤ x.1).card

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 1 (definition of B^{(s)}_{p,n}).

Used by 3

Used byColored Schreier multiset counts are a subsequence of the parent sequence · Closed form and recurrence for colored Schreier multiset counts · Small values of the colored Schreier multiset count

TheoremSmall values of the colored Schreier multiset count#✓fully proved

The numbers of colored Schreier-type multisets satisfy \(|B^{(2)}_{1,4}| = 6\) and \(|B^{(2)}_{2,5}| = 3\) (Table 2 of the paper).

theorem coloredSchreierMultisetCount_small :
    coloredSchreierMultisetCount 2 1 4 = 6 ∧ coloredSchreierMultisetCount 2 2 5 = 3

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Table 2.

Uses 1

Statement usesCounting colored Schreier-type multisets

DefinitionFirst non-multiples of an integer#✓fully proved

For natural numbers \(u\) and \(n\), \(G_{u,n}\) is the set of positive integers \(k \le un\) with \(u \nmid k\) such that at most \(n\) of the integers in \([1, k]\) are not divisible by \(u\). For \(u \ge 1\) the bound \(k \le un\) is automatic, and \(G_{u,n}\) is the set of the first \(n\) positive integers not divisible by \(u\).

def firstNonMultiples (u n : ℕ) : Finset ℕ :=
  (Finset.range (u * n + 1)).filter fun k =>
    0 < k ∧ ¬ u ∣ k ∧ ((Finset.Icc 1 k).filter fun j => ¬ u ∣ j).card ≤ n

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 1 (definition of G_{u,n}).

Used by 2

Used byThe first four positive integers not divisible by 3 · Schreier sets avoiding multiples

TheoremThe first four positive integers not divisible by 3#✓fully proved

The set \(G_{3,4}\) of the first four positive integers not divisible by \(3\) is \(\{1, 2, 4, 5\}\).

theorem firstNonMultiples_three_four : firstNonMultiples 3 4 = {1, 2, 4, 5}

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 1.

Uses 1

Statement usesFirst non-multiples of an integer

DefinitionSchreier sets avoiding multiples#✓fully proved

For natural numbers \(u\) and \(n\), let \(G_{u,n}\) be the set of the first \(n\) positive integers not divisible by \(u\) (taken to be empty when \(u = 0\)), and call a finite set \(F\) of natural numbers Schreier when every element of \(F\) is at least \(|F|\). Then \(|D_{u,n}|\) is the number of Schreier sets \(F \subseteq G_{u,n}\) with \(\lfloor (un - 1)/(u - 1) \rfloor \in F\).

For \(u \le 1\) or \(n = 0\) the set \(G_{u,n}\) is empty and the count is \(0\); otherwise \(un - 1\) and \(u - 1\) are positive, so the natural-number subtraction and floor division agree with the real expression.

def schreierAvoidingMultiplesCount (u n : ℕ) : ℕ :=
  ((firstNonMultiples u n).powerset.filter fun F =>
    (u * n - 1) / (u - 1) ∈ F ∧ IsSchreier F).card

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 1 (definition of D_{u,n}).

Uses 2 · Used by 3

Statement usesSchreier sets · First non-multiples of an integer

Used bySchreier sets avoiding multiples are counted by a subsequence of the parent sequence · Fibonacci values and a recurrence for Schreier sets avoiding multiples · Small values of the count of Schreier sets avoiding multiples

TheoremSmall values of the count of Schreier sets avoiding multiples#✓fully proved

The numbers of Schreier-type sets avoiding multiples satisfy \(|D_{2,6}| = 12\) and \(|D_{3,6}| = 9\) (Table 3 of the paper).

theorem schreierAvoidingMultiplesCount_small :
    schreierAvoidingMultiplesCount 2 6 = 12 ∧ schreierAvoidingMultiplesCount 3 6 = 9

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Table 3.

Uses 1

Statement usesSchreier sets avoiding multiples

DefinitionParent sequence b for Schreier-type multisets#✓fully proved

For natural numbers \(s\) and \(p\), the sequence \(b^{(s)}_{p,n}\), \(n \ge 0\), is defined by \(b^{(s)}_{p,n} = 0\) for \(n \le (p - 1)s\), \(b^{(s)}_{p,n} = 1\) for \((p - 1)s < n \le ps + 1\), and \(b^{(s)}_{p,n} = b^{(s)}_{p,n-1} + b^{(s)}_{p,n-1-ps}\) for \(n \ge ps + 2\), where \(p - 1\) is read as \(0\) when \(p = 0\).

The paper indexes from \(n = 1\); here \(b^{(s)}_{p,0} = 0\).

def schreierParentB (s p : ℕ) (n : ℕ) : ℕ :=
  if n ≤ (p - 1) * s then 0
  else if _h : n ≤ p * s + 1 then 1
  else schreierParentB s p (n - 1) + schreierParentB s p (n - 1 - p * s)
decreasing_by all_goals omega

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 3 (definition of b^{(s)}_{p,n}).

Used by 5

Used byColored Schreier multiset counts are a subsequence of the parent sequence · Binomial-sum formula for the parent sequence b · The parent sequence b vanishes for small indices · The parent sequence b equals one on its initial window · Recurrence for the parent sequence b

TheoremThe parent sequence b vanishes for small indices#✓fully proved

For natural numbers \(s\) and \(p\), let \(b^{(s)}_{p,n}\) be the parent sequence: \(0\) for \(n \le (p - 1)s\), \(1\) for \((p - 1)s < n \le ps + 1\), and \(b^{(s)}_{p,n} = b^{(s)}_{p,n-1} + b^{(s)}_{p,n-1-ps}\) for \(n \ge ps + 2\), where \(p - 1\) is read as \(0\) when \(p = 0\). Then \(b^{(s)}_{p,n} = 0\) for every natural number \(n\) with \(n \le (p - 1)s\).

theorem schreierParentB_of_le {s p n : ℕ} (hn : n ≤ (p - 1) * s) : schreierParentB s p n = 0

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 3.

Uses 1

Statement usesParent sequence b for Schreier-type multisets

TheoremThe parent sequence b equals one on its initial window#✓fully proved

For natural numbers \(s\) and \(p\), let \(b^{(s)}_{p,n}\) be the parent sequence: \(0\) for \(n \le (p - 1)s\), \(1\) for \((p - 1)s < n \le ps + 1\), and \(b^{(s)}_{p,n} = b^{(s)}_{p,n-1} + b^{(s)}_{p,n-1-ps}\) for \(n \ge ps + 2\), where \(p - 1\) is read as \(0\) when \(p = 0\). Then \(b^{(s)}_{p,n} = 1\) for every natural number \(n\) with \((p - 1)s < n \le ps + 1\).

theorem schreierParentB_of_mem {s p n : ℕ} (h₁ : (p - 1) * s < n) (h₂ : n ≤ p * s + 1) :
    schreierParentB s p n = 1

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 3.

Uses 1

Statement usesParent sequence b for Schreier-type multisets

TheoremRecurrence for the parent sequence b#✓fully proved

For natural numbers \(s\) and \(p\), let \(b^{(s)}_{p,n}\) be the parent sequence: \(0\) for \(n \le (p - 1)s\), \(1\) for \((p - 1)s < n \le ps + 1\), and \(b^{(s)}_{p,n} = b^{(s)}_{p,n-1} + b^{(s)}_{p,n-1-ps}\) for \(n \ge ps + 2\), where \(p - 1\) is read as \(0\) when \(p = 0\). Then \(b^{(s)}_{p,n} = b^{(s)}_{p,n-1} + b^{(s)}_{p,n-1-ps}\) for every natural number \(n \ge ps + 2\).

theorem schreierParentB_rec {s p n : ℕ} (hn : p * s + 2 ≤ n) :
    schreierParentB s p n = schreierParentB s p (n - 1) + schreierParentB s p (n - 1 - p * s)

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 3.

Uses 1

Statement usesParent sequence b for Schreier-type multisets

DefinitionThe parent sequence \(d_{u,n}\)#✓fully proved

For natural numbers \(u\) and \(n\), define \(d_{u,n}\) by recursion on \(n\): \(d_{u,n} = 1\) if \(n < 2u\) or \(u = 0\), and otherwise \(d_{u,n} = d_{u,n-u} + d_{u,n-2u+1}\).

The paper takes \(u \ge 2\) and indexes from \(n = 1\), with \(d_{u,n} = 1\) for \(1 \le n \le 2u - 1\); here \(d_{u,0} = 1\) as well, and the degenerate case \(u = 0\) is set to \(1\).

def schreierParentD (u : ℕ) (n : ℕ) : ℕ :=
  if _h : n < 2 * u ∨ u = 0 then 1
  else schreierParentD u (n - u) + schreierParentD u (n - 2 * u + 1)
decreasing_by all_goals omega

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 4 (definition of d_{u,n}).

Used by 4

Used bySchreier sets avoiding multiples are counted by a subsequence of the parent sequence · Binomial sum formula for the parent sequence · Initial values of the parent sequence · Recurrence for the parent sequence

TheoremInitial values of the parent sequence#✓fully proved

For all natural numbers \(u\) and \(n\) with \(n < 2u\), the parent sequence \(d_{u,n}\) satisfies \(d_{u,n} = 1\).

theorem schreierParentD_of_lt {u n : ℕ} (hn : n < 2 * u) : schreierParentD u n = 1

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 4.

Uses 1

Statement usesThe parent sequence \(d_{u,n}\)

TheoremRecurrence for the parent sequence#✓fully proved

For all natural numbers \(u \ge 1\) and \(n \ge 2u\), the parent sequence \(d_{u,n}\) satisfies \(d_{u,n} = d_{u,n-u} + d_{u,n-2u+1}\).

theorem schreierParentD_rec {u n : ℕ} (hu : 1 ≤ u) (hn : 2 * u ≤ n) :
    schreierParentD u n = schreierParentD u (n - u) + schreierParentD u (n - 2 * u + 1)

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Section 4.

Uses 1

Statement usesThe parent sequence \(d_{u,n}\)

TheoremFormula and recurrence for Schreier-type multisets#●ready to prove

Let \(s, p \ge 1\), and for \(n \ge 1\) let \(|A^{(s)}_{p,n}|\) be the number of distinct sub-multisets \(F\) of \(\{1^s, \dots, (n - 1)^s, n\}\) with \(n \in F\) and \(\min F \ge p|F|\), where \(|F|\) counts multiplicity. For \(1 \le n \le sp + 1\),

\[|A^{(s)}_{p,n}| = \sum_{k=1}^{\lfloor (sn+1)/(sp+1) \rfloor} \binom{n - pk + k - 2}{k - 1},\]

and for \(n \ge sp + 2\),

\[|A^{(s)}_{p,n}| = \sum_{i=0}^{s} |A^{(s)}_{p,n-1-ip}|.\]

In the first sum \(pk \le n\), so the top \(n - pk + k - 2\) is negative only for \(k = 1\) and \(n = p\), where the coefficient is \(\binom{-1}{0} = 1\); the natural-number subtraction gives \(\binom{0}{0} = 1\) there as well.

public theorem_wanted schreierMultisetCount_formula_and_recurrence {s p : ℕ} (hs : 1 ≤ s)
    (hp : 1 ≤ p) :
    (∀ n, 1 ≤ n → n ≤ s * p + 1 →
      schreierMultisetCount s p n =
        ∑ k ∈ Finset.Icc 1 ((s * n + 1) / (s * p + 1)), (n - p * k + k - 2).choose (k - 1)) ∧
    ∀ n, s * p + 2 ≤ n →
      schreierMultisetCount s p n = ∑ i ∈ Finset.range (s + 1), schreierMultisetCount s p (n - 1 - i * p)

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Theorem 1.

Uses 1

Statement usesNumber of Schreier-type multisets

TheoremClosed form and recurrence for colored Schreier multiset counts#●ready to prove

Let \(s \ge 1\) and \(p \ge 1\), and write \(|B^{(s)}_{p,n}|\) for the number of colored Schreier-type multisets. For \(1 \le n \le sp + 1\),

\[|B^{(s)}_{p,n}| = \sum_{k=1}^{\lfloor (ns+1)/(ps+1) \rfloor} \binom{(n - kp)s}{k - 1},\]

and for \(n \ge sp + 2\),

\[|B^{(s)}_{p,n}| = \sum_{i=0}^{s} \binom{s}{i} \, |B^{(s)}_{p,n-1-ip}|.\]

public theorem_wanted coloredSchreierMultisetCount_formula_and_recurrence {s p : ℕ} (hs : 1 ≤ s)
    (hp : 1 ≤ p) :
    (∀ n, 1 ≤ n → n ≤ s * p + 1 →
      coloredSchreierMultisetCount s p n =
        ∑ k ∈ Finset.Icc 1 ((n * s + 1) / (p * s + 1)), ((n - k * p) * s).choose (k - 1)) ∧
    ∀ n, s * p + 2 ≤ n →
      coloredSchreierMultisetCount s p n =
        ∑ i ∈ Finset.range (s + 1), s.choose i * coloredSchreierMultisetCount s p (n - 1 - i * p)

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Theorem 2.

Uses 1

Statement usesCounting colored Schreier-type multisets

TheoremBinomial-sum formula for the parent sequence b#●ready to prove

Let \(b^{(s)}_{p,n}\) be the parent sequence: \(0\) for \(n \le (p - 1)s\), \(1\) for \((p - 1)s < n \le ps + 1\), and \(b^{(s)}_{p,n} = b^{(s)}_{p,n-1} + b^{(s)}_{p,n-1-ps}\) for \(n \ge ps + 2\). For positive integers \(s\), \(p\) and \(n\),

\[b^{(s)}_{p,n} = \sum_{i=0}^{\lfloor (n - s(p-1) - 1)/(sp+1) \rfloor} \binom{n - s(p-1) - 1 - spi}{i},\]

where the sum is empty when \(n \le s(p - 1)\).

public theorem_wanted schreierParentB_eq_sum_choose {s p n : ℕ} (hs : 1 ≤ s) (hp : 1 ≤ p)
    (hn : 1 ≤ n) :
    schreierParentB s p n =
      ∑ i ∈ (Finset.range n).filter (fun i => (s * p + 1) * i + s * (p - 1) + 1 ≤ n),
        (n - s * (p - 1) - 1 - s * p * i).choose i

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Proposition 1.

Uses 1

Statement usesParent sequence b for Schreier-type multisets

TheoremColored Schreier multiset counts are a subsequence of the parent sequence#●ready to prove

For all positive integers \(s\), \(p\) and \(n\), the number \(|B^{(s)}_{p,n}|\) of colored Schreier-type multisets equals the term \(b^{(s)}_{p,ns-s+1}\) of the parent sequence \(b^{(s)}_{p,m}\).

public theorem_wanted coloredSchreierMultisetCount_eq_schreierParentB {s p n : ℕ} (hs : 1 ≤ s)
    (hp : 1 ≤ p) (hn : 1 ≤ n) :
    coloredSchreierMultisetCount s p n = schreierParentB s p (n * s - s + 1)

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Lemma 1.

Uses 2

Statement usesCounting colored Schreier-type multisets · Parent sequence b for Schreier-type multisets

TheoremThe non-multiples of an integer as values of a floor function#●ready to prove

For every integer \(u \ge 2\), the set \(\{\lfloor (un - 1)/(u - 1) \rfloor : n \ge 1\}\), with \(n\) ranging over the positive integers, is the set of positive integers not divisible by \(u\).

public theorem_wanted image_floor_eq_nonMultiples {u : ℕ} (hu : 2 ≤ u) :
    (fun n => (u * n - 1) / (u - 1)) '' {n | 1 ≤ n} = {m | 1 ≤ m ∧ ¬ u ∣ m}

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Lemma 2.

TheoremBinomial sum formula for the parent sequence#●ready to prove

For all natural numbers \(u \ge 2\) and \(n \ge 1\), the parent sequence \(d_{u,n}\) satisfies

\[ d_{u,n} = \sum_{i=0}^{\lfloor (n-1)/u \rfloor} \binom{\lfloor (n + (u-1)i - u)/(2u-1) \rfloor}{i}. \]

The numerator \(n + (u-1)i - u\) is negative only when \(i = 0\) and \(n < u\). There it is read as \(0\) (truncated subtraction), so the term is \(\binom{0}{0} = 1\), which agrees with the paper's \(\binom{-1}{0} = 1\).

public theorem_wanted schreierParentD_eq_sum_choose {u n : ℕ} (hu : 2 ≤ u) (hn : 1 ≤ n) :
    schreierParentD u n =
      ∑ i ∈ Finset.range ((n - 1) / u + 1), ((n + (u - 1) * i - u) / (2 * u - 1)).choose i

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Proposition 2.

Uses 1

Statement usesThe parent sequence \(d_{u,n}\)

TheoremSchreier sets avoiding multiples are counted by a subsequence of the parent sequence#●ready to prove

For every integer \(u \ge 2\) and every integer \(n \ge 1\), the number \(|D_{u,n}|\) of Schreier-type sets avoiding multiples of \(u\) equals the term \(d_{u,un-(u-1)}\) of the parent sequence \(d_{u,m}\).

public theorem_wanted schreierAvoidingMultiplesCount_eq_schreierParentD {u n : ℕ} (hu : 2 ≤ u)
    (hn : 1 ≤ n) :
    schreierAvoidingMultiplesCount u n = schreierParentD u (u * n - (u - 1))

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Proposition 3.

Uses 2

Statement usesSchreier sets avoiding multiples · The parent sequence \(d_{u,n}\)

TheoremFibonacci values and a recurrence for Schreier sets avoiding multiples#●ready to prove

Let \(u \ge 2\), write \(|D_{u,n}|\) for the number of Schreier-type sets avoiding multiples of \(u\), and write \(F_n\) for the Fibonacci numbers, with \(F_0 = 0\) and \(F_1 = 1\). For \(1 \le n \le 2u - 1\), \(|D_{u,n}| = F_n\), and for \(n \ge 2u\), as an identity of integers,

\[|D_{u,n}| = \sum_{i=1}^{u} (-1)^{i-1} \binom{u}{i} |D_{u,n-i}| + |D_{u,n-2u+1}|.\]

public theorem_wanted schreierAvoidingMultiplesCount_fib_and_recurrence {u : ℕ} (hu : 2 ≤ u) :
    (∀ n, 1 ≤ n → n ≤ 2 * u - 1 → schreierAvoidingMultiplesCount u n = Nat.fib n) ∧
    ∀ n, 2 * u ≤ n →
      (schreierAvoidingMultiplesCount u n : ℤ) =
        ∑ i ∈ Finset.Icc 1 u,
            (-1 : ℤ) ^ (i - 1) * u.choose i * schreierAvoidingMultiplesCount u (n - i) +
          schreierAvoidingMultiplesCount u (n - 2 * u + 1)

Sources

• Hùng Việt Chu, Yubo Geng, Julian King, Steven J. Miller, Garrett Tresch and Zachary Louis Vasseur, Linear Recurrences from Counting Schreier-Type Multisets, INTEGERS 26 (2026), Article A53, Theorem 3.

Uses 1

Statement usesSchreier sets avoiding multiples

DefinitionWeighted Schreier-type sets#✓fully proved

For natural numbers \(k\) and \(n\), let \(\omega_k(E)\) denote the number of elements of a finite set \(E\) that are different from \(k\). The weighted Schreier count \(a_{k,n}\) is the number of subsets \(E \subseteq \{1, \dots, n\}\) that are empty or satisfy \(\omega_k(E) < \min E\).

public def weightedSchreierCount (k n : ℕ) : ℕ :=
  ((Finset.Icc 1 n).powerset.filter fun E => ∀ m ∈ E, (E.filter (· ≠ k)).card < m).card

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 1 (definition of A_{k,n} and a_{k,n}).

Used by 11

Used byWeighted Schreier counts on and above the diagonal · Weighted Schreier counts equal twice a Fibonacci number for small offsets · Diagonal weighted Schreier counts · Weighted Schreier counts for \(n < k\) · Weighted Schreier counts for \(0 < m < k\) · Weighted Schreier counts for \(k = 1\) · Weighted Schreier count \(a_{1,4}\) · Weighted Schreier count \(a_{1,1}\) · Recurrence for weighted Schreier counts · Weighted Schreier count \(a_{3,3}\) · Weighted Schreier count \(a_{2,1}\)

TheoremWeighted Schreier count \(a_{1,1}\)#✓fully proved

The weighted Schreier count \(a_{1,1}\) equals \(2\).

public theorem weightedSchreierCount_one_one : weightedSchreierCount 1 1 = 2

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 1, Table 1.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremWeighted Schreier count \(a_{2,1}\)#✓fully proved

The weighted Schreier count \(a_{2,1}\) equals \(1\).

public theorem weightedSchreierCount_two_one : weightedSchreierCount 2 1 = 1

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 1, Table 1.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremWeighted Schreier count \(a_{3,3}\)#✓fully proved

The weighted Schreier count \(a_{3,3}\) equals \(4\).

public theorem weightedSchreierCount_three_three : weightedSchreierCount 3 3 = 4

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 1, Table 1.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremWeighted Schreier count \(a_{1,4}\)#✓fully proved

The weighted Schreier count \(a_{1,4}\) equals \(6\).

public theorem weightedSchreierCount_one_four : weightedSchreierCount 1 4 = 6

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 1, Table 1.

Uses 1

Statement usesWeighted Schreier-type sets

DefinitionSeeded partial sums#✓fully proved

Let \(M\) be an additive commutative monoid, and let \(s = (s_n)_{n \ge 0}\) (the seed sequence) and \(a = (a_n)_{n \ge 0}\) be sequences in \(M\). The seeded partial sums \(t^s_{k,n}\), for \(k, n \ge 0\), are defined by recursion on \(k\): \(t^s_{0,n} = a_n\) and \(t^s_{k+1,n} = s_k + \sum_{i\lt n} t^s_{k,i}\).

public def seededPartialSums {M : Type*} [AddCommMonoid M] (s a : ℕ → M) : ℕ → ℕ → M
  | 0, n => a n
  | k + 1, n => s k + ∑ i ∈ Finset.range n, seededPartialSums s a k i

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 3 (partial sum operator P_b and the sequences t^s_{k,n}).

Used by 4

Used byIterated partial sums · Recurrence for iterated partial sums · Effect of the seed on seeded partial sums · Seeded partial sums start at the seed

DefinitionIterated partial sums#✓fully proved

Let \(M\) be an additive commutative monoid and let \(a = (a_n)_{n \ge 0}\) be a sequence in \(M\). For \(k, m \ge 0\), the \(k\)-fold iterated partial sum \(P^{(k)}(a)(m)\) is the seeded partial sum \(t^s_{k,m}\) of \(a\) for the zero seed sequence \(s = 0\). Thus \(P^{(0)}(a)(m) = a_m\) and \(P^{(k+1)}(a)(m) = \sum_{i\lt m} P^{(k)}(a)(i)\).

public def iteratedPartialSum {M : Type*} [AddCommMonoid M] (k : ℕ) (a : ℕ → M) (m : ℕ) : M :=
  seededPartialSums 0 a k m

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 3 (definition of P^{(k)}).

Uses 1 · Used by 4

Statement usesSeeded partial sums

Used byAdding one to a sequence shifts its iterated partial sums by a binomial coefficient · Iterated partial sums of shifted Fibonacci numbers · The first iterated partial sum · Recurrence for iterated partial sums

TheoremSeeded partial sums start at the seed#✓fully proved

Let \(M\) be an additive commutative monoid, let \(s = (s_n)_{n \ge 0}\) and \(a = (a_n)_{n \ge 0}\) be sequences in \(M\), and write \(t^s_{k,n}\) for the seeded partial sums of \(a\) with seed sequence \(s\). Then \(t^s_{k+1,0} = s_k\) for every \(k \ge 0\).

public theorem seededPartialSums_succ_zero {M : Type*} [AddCommMonoid M] (s a : ℕ → M)
    (k : ℕ) : seededPartialSums s a (k + 1) 0 = s k

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 3 (partial sum operator P_b).

Uses 1

Statement usesSeeded partial sums

TheoremThe first iterated partial sum#✓fully proved

Let \(M\) be an additive commutative monoid and let \((a_n)_{n \ge 0}\) be a sequence in \(M\). For every \(m \ge 0\), the \(1\)-fold iterated partial sum of \((a_n)\) at \(m\) is the ordinary partial sum: \(P^{(1)}((a_n)_{n \ge 0})(m) = \sum_{i\lt m} a_i\).

public theorem iteratedPartialSum_one {M : Type*} [AddCommMonoid M] (a : ℕ → M) (m : ℕ) :
    iteratedPartialSum 1 a m = ∑ i ∈ Finset.range m, a i

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 3 (definition of P^{(k)}).

Uses 1

Statement usesIterated partial sums

TheoremRecurrence for iterated partial sums#✓fully proved

Let \(M\) be an additive commutative monoid, let \(a = (a_n)_{n \ge 0}\) be a sequence in \(M\), and write \(P^{(k)}(a)(m)\) for its \(k\)-fold iterated partial sum at \(m\). Then for all \(k, m \ge 0\), \(P^{(k+1)}(a)(m+1) = P^{(k+1)}(a)(m) + P^{(k)}(a)(m)\).

public theorem iteratedPartialSum_succ_succ {M : Type*} [AddCommMonoid M] (a : ℕ → M)
    (k m : ℕ) :
    iteratedPartialSum (k + 1) a (m + 1) =
      iteratedPartialSum (k + 1) a m + iteratedPartialSum k a m

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Section 3 (definition of P^{(k)}; recurrence used in the proofs of Lemmas 3.3 and 3.4).

Uses 2

Statement usesIterated partial sums

Proof usesSeeded partial sums

TheoremDiagonal weighted Schreier counts#●ready to prove

For every natural number \(n \ge 1\), the weighted Schreier count satisfies \(a_{n,n} = 2F_n\), where \(F_n\) is the \(n\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)).

public theorem_wanted weightedSchreierCount_diag {n : ℕ} (hn : 1 ≤ n) :
    weightedSchreierCount n n = 2 * Nat.fib n

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Theorem 1.1.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremWeighted Schreier counts for \(k = 1\)#●ready to prove

For every natural number \(\ell\), the weighted Schreier count satisfies \(a_{1,1+\ell} = F_{\ell+2} + 1\), where \(F_j\) is the \(j\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)).

public theorem_wanted weightedSchreierCount_one (l : ℕ) :
    weightedSchreierCount 1 (1 + l) = Nat.fib (l + 2) + 1

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Theorem 1.2, case k = 1.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremWeighted Schreier counts on and above the diagonal#●ready to prove

Let \(a_{k,n}\) be the weighted Schreier count and let \(F_n\) denote the Fibonacci numbers, with \(F_0 = 0\) and \(F_1 = 1\). For all \(k \ge 2\) and \(\ell \ge 0\), \(a_{k,k+\ell} = 2\sum_{i=0}^{k-2} \binom{\ell}{i} F_{k-i} + 2\binom{\ell}{k-1} + \sum_{j=1}^{\ell} \binom{j}{\ell-j+k}\).

public theorem_wanted weightedSchreierCount_add {k : ℕ} (hk : 2 ≤ k) (l : ℕ) :
    weightedSchreierCount k (k + l) =
      2 * ∑ i ∈ Finset.range (k - 1), l.choose i * Nat.fib (k - i) + 2 * l.choose (k - 1) +
        ∑ j ∈ Finset.Icc 1 l, j.choose (l - j + k)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Theorem 1.2, case k ≥ 2, ℓ ≥ 0.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremWeighted Schreier counts for \(0 < m < k\)#●ready to prove

For natural numbers \(k \ge 2\) and \(m\) with \(0 < m < k\), the weighted Schreier count satisfies \(a_{k,m} = F_{m+1}\), where \(F_j\) is the \(j\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)).

public theorem_wanted weightedSchreierCount_of_pos_of_lt {k m : ℕ} (hk : 2 ≤ k) (hm : 0 < m)
    (hmk : m < k) : weightedSchreierCount k m = Nat.fib (m + 1)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Theorem 1.2, case k ≥ 2, -k < ℓ < 0.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremWeighted Schreier counts equal twice a Fibonacci number for small offsets#●ready to prove

Let \(a_{k,n}\) be the weighted Schreier count and let \(F_n\) denote the Fibonacci numbers, with \(F_0 = 0\) and \(F_1 = 1\). For all \(k, \ell \ge 0\) with \(k \ge \ell + 2\), we have \(a_{k,k+\ell} = 2F_{k+\ell}\).

public theorem_wanted weightedSchreierCount_add_of_le {k l : ℕ} (hkl : l + 2 ≤ k) :
    weightedSchreierCount k (k + l) = 2 * Nat.fib (k + l)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Theorem 1.4.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremRecurrence for weighted Schreier counts#●ready to prove

For natural numbers \(k\) and \(n\) with \(k \ge 1\), \(n > k\) and \(n > 2\), the weighted Schreier counts satisfy \(a_{k,n} = a_{k,n-1} + a_{k-1,n-2}\). At \(k = 1\) the term \(a_{0,n-2}\) is the same count with \(\omega_0(E)\), the number of elements of \(E\) different from \(0\), equal to the number \(|E|\) of all elements of \(E\), since no element of a set \(E \subseteq \{1, \dots, n-2\}\) equals \(0\).

public theorem_wanted weightedSchreierCount_recurrence {k n : ℕ} (hk : 1 ≤ k) (hkn : k < n)
    (h2n : 2 < n) :
    weightedSchreierCount k n =
      weightedSchreierCount k (n - 1) + weightedSchreierCount (k - 1) (n - 2)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Proposition 3.1.

Uses 1

Statement usesWeighted Schreier-type sets

TheoremEffect of the seed on seeded partial sums#●ready to prove

Let \(R\) be a commutative ring, let \(a = (a_n)_{n \ge 0}\) and \(b = (b_n)_{n \ge 0}\) be sequences in \(R\), and write \(t^b_{k,n}\) for the seeded partial sums of \(a\) with seed sequence \(b\) and \(t^0_{k,n}\) for those with the zero seed sequence. Then for all \(k, n \ge 0\), \(t^b_{k,n} - t^0_{k,n} = \sum_{i\lt k} \binom{n}{i} b_{k-1-i}\), where the binomial coefficients are read as elements of \(R\).

public theorem_wanted seededPartialSums_sub_zero {R : Type*} [CommRing R] (b a : ℕ → R)
    (k n : ℕ) :
    seededPartialSums b a k n - seededPartialSums 0 a k n =
      ∑ i ∈ Finset.range k, (n.choose i : R) * b (k - 1 - i)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Lemma 3.2.

Uses 1

Statement usesSeeded partial sums

TheoremAdding one to a sequence shifts its iterated partial sums by a binomial coefficient#●ready to prove

Let \(R\) be a commutative ring, let \((a_n)_{n \ge 0}\) be a sequence in \(R\), and let \(k, m \ge 0\). Writing \(P^{(k)}(x)(m)\) for the \(k\)-fold iterated partial sum of a sequence \(x\) at \(m\), we have \(P^{(k)}((a_n + 1)_{n \ge 0})(m) - P^{(k)}((a_n)_{n \ge 0})(m) = \binom{m}{k}\), where \(\binom{m}{k}\) is read as an element of \(R\).

public theorem_wanted iteratedPartialSum_add_one_sub {R : Type*} [CommRing R] (a : ℕ → R)
    (k m : ℕ) :
    iteratedPartialSum k (fun n => a n + 1) m - iteratedPartialSum k a m = (m.choose k : R)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Lemma 3.3.

Uses 1

Statement usesIterated partial sums

TheoremIterated partial sums of shifted Fibonacci numbers#●ready to prove

Let \(F_n\) denote the Fibonacci numbers, with \(F_0 = 0\) and \(F_1 = 1\), and write \(P^{(k)}(x)(m)\) for the \(k\)-fold iterated partial sum of a sequence \(x\) of natural numbers at \(m\). Then for all \(k, \ell \ge 0\), \(P^{(k)}((F_{n+2})_{n \ge 0})(\ell) = P^{(k)}((F_n)_{n \ge 0})(\ell) + P^{(k)}((F_n)_{n \ge 0})(\ell + 1)\).

public theorem_wanted iteratedPartialSum_fib_add_two (k l : ℕ) :
    iteratedPartialSum k (fun n => Nat.fib (n + 2)) l =
      iteratedPartialSum k Nat.fib l + iteratedPartialSum k Nat.fib (l + 1)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Lemma 3.4.

Uses 1

Statement usesIterated partial sums

TheoremWeighted Schreier counts for \(n < k\)#●ready to prove

For all natural numbers \(n < k\), the weighted Schreier count satisfies \(a_{k,n} = F_{n+1}\), where \(F_j\) is the \(j\)-th Fibonacci number (\(F_0 = 0\), \(F_1 = 1\)).

This includes \(n = 0\), where \(a_{k,0} = 1 = F_1\); the source takes \(n\) positive.

public theorem_wanted weightedSchreierCount_of_lt {k n : ℕ} (hnk : n < k) :
    weightedSchreierCount k n = Nat.fib (n + 1)

Sources

• Hùng Việt Chu and Zachary Louis Vasseur, Weighted Schreier-type Sets and the Fibonacci Sequence, The Fibonacci Quarterly 62 (2024), no. 4, Proposition 3.5.

Uses 1

Statement usesWeighted Schreier-type sets

61 fully proved35 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.