Generalized Frobenius numbers

DefinitionNumber of representations by a vector of generators#✓fully proved

For natural numbers \(a_1, \dots, a_k\) and an integer \(m\), the representation count \(d(m; a_1, \dots, a_k)\) is the number of tuples \((x_1, \dots, x_k)\) of natural numbers with \(x_1 a_1 + \dots + x_k a_k = m\), counted as an extended natural number, so that it is \(\infty\) when there are infinitely many such tuples.

It is \(0\) for \(m < 0\), and finite when every \(a_i\) is positive.

noncomputable def frobeniusRepCount {k : ℕ} (a : Fin k → ℕ) (m : ℤ) : ℕ∞ :=
  {x : Fin k → ℕ | ∑ i, (x i : ℤ) * a i = m}.encard
Sources
  • Kittipong Subwattanachai, Formulas for the Generalized Frobenius Number of Triangular Numbers, INTEGERS 26 (2026), Article A63, Introduction (definition of d(n; a₁, …, a_k)).
Used by 8
Used byRepresentation counts between consecutive two-generator Frobenius numbers · Representation counts above a shifted two-generator Frobenius number · Representation count of the reduced triangular triple at a shifted Frobenius number · Splitting off the first generator of the reduced triangular triple · Negative integers have no representations · Finitely many representations for positive generators · Generalized Frobenius number · Uniqueness of the generalized Frobenius number

TheoremNegative integers have no representations#✓fully proved

For all natural numbers \(a_1, \dots, a_k\) and every integer \(m < 0\), the representation count \(d(m; a_1, \dots, a_k)\) is \(0\).

theorem frobeniusRepCount_eq_zero_of_neg {k : ℕ} (a : Fin k → ℕ) {m : ℤ} (hm : m < 0) :
    frobeniusRepCount a m = 0
Sources
  • Kittipong Subwattanachai, Formulas for the Generalized Frobenius Number of Triangular Numbers, INTEGERS 26 (2026), Article A63, Introduction (definition of d(n; a₁, …, a_k)).
Uses 1
Statement usesNumber of representations by a vector of generators

TheoremFinitely many representations for positive generators#✓fully proved

If \(a_1, \dots, a_k\) are positive natural numbers, then for every integer \(m\) the representation count \(d(m; a_1, \dots, a_k)\) is finite.

theorem frobeniusRepCount_ne_top {k : ℕ} {a : Fin k → ℕ} (ha : ∀ i, 0 < a i) (m : ℤ) :
    frobeniusRepCount a m ≠ ⊤
Sources
  • Kittipong Subwattanachai, Formulas for the Generalized Frobenius Number of Triangular Numbers, INTEGERS 26 (2026), Article A63, Introduction (definition of d(n; a₁, …, a_k)).
Uses 1
Statement usesNumber of representations by a vector of generators

DefinitionGeneralized Frobenius number#✓fully proved

For natural numbers \(a_1, \dots, a_k\) and \(s\), write \(d(m; a)\) for the number of representations of an integer \(m\) by \(a = (a_1, \dots, a_k)\). An integer \(g\) is the generalized Frobenius number \(g(a; s) = \max \{m \in \mathbb{Z} \mid d(m; a) \le s\}\) when \(d(g; a) \le s\) and \(d(m; a) > s\) for every integer \(m > g\).

def IsGenFrobeniusNumber {k : ℕ} (a : Fin k → ℕ) (s : ℕ) (g : ℤ) : Prop :=
  frobeniusRepCount a g ≤ s ∧ ∀ m : ℤ, g < m → (s : ℕ∞) < frobeniusRepCount a m
Sources
  • Kittipong Subwattanachai, Formulas for the Generalized Frobenius Number of Triangular Numbers, INTEGERS 26 (2026), Article A63, Introduction (definition of g(A; s)).
Uses 1 · Used by 10
Statement usesNumber of representations by a vector of generators
Used byRepresentation counts between consecutive two-generator Frobenius numbers · Representation counts above a shifted two-generator Frobenius number · Representation count of the reduced triangular triple at a shifted Frobenius number · Beck–Kifer reduction by a common factor of all generators but the first · Generalized Frobenius numbers of the reduced triangular triple · Generalized Frobenius numbers of three consecutive triangular numbers · Komatsu's conjecture on generalized Frobenius numbers of triangular triples · Generalized Frobenius numbers of triangular triples in parametrized form · Explicit generalized Frobenius numbers of triangular triples at levels 11 to 20 · Uniqueness of the generalized Frobenius number

TheoremUniqueness of the generalized Frobenius number#✓fully proved

For natural numbers \(a_1, \dots, a_k\) and \(s\), if the integers \(g\) and \(g'\) are both the generalized Frobenius number \(g(a_1, \dots, a_k; s)\), then \(g = g'\).

theorem IsGenFrobeniusNumber.unique {k : ℕ} {a : Fin k → ℕ} {s : ℕ} {g g' : ℤ}
    (h : IsGenFrobeniusNumber a s g) (h' : IsGenFrobeniusNumber a s g') : g = g'
Sources
  • Kittipong Subwattanachai, Formulas for the Generalized Frobenius Number of Triangular Numbers, INTEGERS 26 (2026), Article A63, Introduction (definition of g(A; s) as a maximum).
Uses 2
Statement usesGeneralized Frobenius number
Proof usesNumber of representations by a vector of generators
5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.