Frobenius numbers of compound sequences

DefinitionCompound sequence#✓fully proved

Let \(n\) be a natural number and let \(a = (a_i)\) and \(b = (b_i)\) be sequences of natural numbers. For a natural number \(j\), the \(j\)-th term of the compound sequence of \(a\) and \(b\) is

\[c_j = \Big(\prod_{i=1}^{j} b_i\Big) \Big(\prod_{i=j+1}^{n} a_i\Big),\]

so that \(c_j = b_1 b_2 \cdots b_j \, a_{j+1} \cdots a_n\) for \(0 \le j \le n\), the range of interest; for \(j > n\) the second product is empty and \(c_j = b_1 \cdots b_j\).

public def compoundSequence (n : ℕ) (a b : ℕ → ℕ) (j : ℕ) : ℕ :=
  (∏ i ∈ Finset.Icc 1 j, b i) * ∏ i ∈ Finset.Ioc j n, a i

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Section 2, eq. (1) (after Kiers, O'Neill, and Ponomarenko).

Used by 7

Used byApéry set and Frobenius number of a compound sequence · Embedding dimension of the semigroup of a compound sequence · When deleting a term of a compound sequence leaves a numerical semigroup · Deletions from a compound sequence that keep the Frobenius number · The minimal generating set as the least Frobenius-preserving subset · Last term of a compound sequence · First term of a compound sequence

TheoremFirst term of a compound sequence#✓fully proved

For every natural number \(n\) and all sequences \(a\), \(b\) of natural numbers, the compound sequence \(c\) of \(a\) and \(b\) satisfies \(c_0 = a_1 a_2 \cdots a_n\).

public theorem compoundSequence_zero (n : ℕ) (a b : ℕ → ℕ) :
    compoundSequence n a b 0 = ∏ i ∈ Finset.Ioc 0 n, a i

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Section 2, eq. (1).

Uses 1

Statement usesCompound sequence

TheoremLast term of a compound sequence#✓fully proved

For every natural number \(n\) and all sequences \(a\), \(b\) of natural numbers, the compound sequence \(c\) of \(a\) and \(b\) satisfies \(c_n = b_1 b_2 \cdots b_n\).

public theorem compoundSequence_self (n : ℕ) (a b : ℕ → ℕ) :
    compoundSequence n a b n = ∏ i ∈ Finset.Icc 1 n, b i

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Section 2, eq. (1).

Uses 1

Statement usesCompound sequence

TheoremBrauer–Shockley formula for the Frobenius number#●ready to prove

Let \(A_1, \dots, A_k\) be positive integers with \(\gcd(A_1, \dots, A_k) = 1\), let \(S\) be the additive submonoid of \(\mathbb{N}\) they generate, and let \(a = A_i\) be one of them with \(a \ge 2\). For \(1 \le x \le a - 1\) let \(m_x\) be the least element of \(S\) congruent to \(x\) modulo \(a\). If \(M\) is the largest of the numbers \(m_x\), then \(M - a\) is the largest integer not in \(S\), that is, the Frobenius number of \(S\).

The case \(a = 1\), where the maximum would be over an empty set, is excluded.

public theorem_wanted frobenius_eq_max_apery_sub {k : ℕ} (A : Fin k → ℕ) (hA : ∀ i, 0 < A i)
    (hgcd : Finset.univ.gcd A = 1) (i : Fin k) (ha : 2 ≤ A i) (M : ℕ)
    (hM : IsGreatest {m | ∃ x ∈ Finset.Icc 1 (A i - 1),
      IsLeast {s | s ∈ AddSubmonoid.closure (Set.range A) ∧ s ≡ x [MOD A i]} m} M) :
    IsGreatest {m : ℤ | ∀ s ∈ AddSubmonoid.closure (Set.range A), (s : ℤ) ≠ m}
      ((M : ℤ) - A i)

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Lemma 1, quoting Brauer and Shockley.

TheoremApéry set and Frobenius number of a compound sequence#●ready to prove

Let \(n\) be a natural number and let \(a_1, \dots, a_n\) and \(b_1, \dots, b_n\) be natural numbers with \(0 < a_i < b_i\) for \(1 \le i \le n\) and \(\gcd(a_i, b_j) = 1\) whenever \(1 \le j \le i \le n\). Let \(c_0, \dots, c_n\) be their compound sequence and \(S\) the additive submonoid of \(\mathbb{N}\) generated by \(c_0, \dots, c_n\). Then (Kiers, O'Neill and Ponomarenko) the Apéry set of \(S\) with respect to \(c_0\), the set of least elements of \(S\) in the residue classes modulo \(c_0\), is

\[\Big\{\sum_{i=1}^{n} c_i x_i : x_1, \dots, x_n \in \mathbb{N},\ x_i < a_i\Big\},\]

and the largest integer not in \(S\), the Frobenius number of \(S\), is

\[F(S) = \sum_{i=1}^{n} (a_i - 1) c_i - c_0.\]

public theorem_wanted compoundSequence_apery_and_frobenius (n : ℕ) (a b : ℕ → ℕ)
    (hab : ∀ i ∈ Finset.Icc 1 n, 0 < a i ∧ a i < b i)
    (hcop : ∀ i ∈ Finset.Icc 1 n, ∀ j ∈ Finset.Icc 1 n, j ≤ i → Nat.Coprime (a i) (b j)) :
    let c := compoundSequence n a b
    let S := AddSubmonoid.closure (((Finset.range (n + 1)).image c : Finset ℕ) : Set ℕ)
    {m | ∃ x < c 0, IsLeast {s | s ∈ S ∧ s ≡ x [MOD c 0]} m} =
        {m | ∃ x : ℕ → ℕ, (∀ i ∈ Finset.Icc 1 n, x i < a i) ∧
          m = ∑ i ∈ Finset.Icc 1 n, c i * x i} ∧
      IsGreatest {m : ℤ | ∀ s ∈ S, (s : ℤ) ≠ m}
        (∑ i ∈ Finset.Icc 1 n, ((a i : ℤ) - 1) * c i - c 0)

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Theorem 2, eq. (2), quoting Kiers, O'Neill, and Ponomarenko.

Uses 1

Statement usesCompound sequence

TheoremWhen deleting a term of a compound sequence leaves a numerical semigroup#●ready to prove

Let \(n \ge 1\) and let \(a_1, \dots, a_n\) and \(b_1, \dots, b_n\) be natural numbers with \(0 < a_i < b_i\) for \(1 \le i \le n\) and \(\gcd(a_i, b_j) = 1\) whenever \(1 \le j \le i \le n\); let \(c_0, \dots, c_n\) be their compound sequence. For \(0 \le j \le n\), the additive submonoid of \(\mathbb{N}\) generated by the terms \(c_i\) with \(0 \le i \le n\) and \(i \ne j\) has finite complement in \(\mathbb{N}\) (so it is a numerical semigroup) if and only if either \(0 < j < n\) and \(\gcd(a_j, b_{j+1}) = 1\), or \(j = n\) and \(a_n = 1\).

public theorem_wanted compoundSequence_erase_cofinite_iff (n : ℕ) (hn : 1 ≤ n) (a b : ℕ → ℕ)
    (hab : ∀ i ∈ Finset.Icc 1 n, 0 < a i ∧ a i < b i)
    (hcop : ∀ i ∈ Finset.Icc 1 n, ∀ j ∈ Finset.Icc 1 n, j ≤ i → Nat.Coprime (a i) (b j))
    (j : ℕ) (hj : j ≤ n) :
    (AddSubmonoid.closure ((((Finset.range (n + 1)).erase j).image (compoundSequence n a b) :
        Finset ℕ) : Set ℕ) : Set ℕ)ᶜ.Finite ↔
      (0 < j ∧ j < n ∧ Nat.Coprime (a j) (b (j + 1))) ∨ (j = n ∧ a j = 1)

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Proposition 3.

Uses 1

Statement usesCompound sequence

TheoremDeletions from a compound sequence that keep the Frobenius number#●ready to prove

Let \(n\) be a natural number and let \((a_i)_{i \ge 0}\) and \((b_i)_{i \ge 0}\) be sequences of natural numbers with \(0 < a_i < b_i\) for \(1 \le i \le n\) and \(\gcd(a_i, b_j) = 1\) whenever \(1 \le j \le i \le n\); let \(c_0, \dots, c_n\) be their compound sequence. Let \(0 \le j \le n\) and suppose that the terms \(c_i\) with \(0 \le i \le n\) and \(i \ne j\) have greatest common divisor \(1\). Let \(S\) be the additive submonoid of \(\mathbb{N}\) generated by \(c_0, \dots, c_n\) and \(S^\star\) the one generated by the \(c_i\) with \(0 \le i \le n\) and \(i \ne j\). Then some integer is both the largest integer not in \(S^\star\) and the largest integer not in \(S\), that is, \(S^\star\) and \(S\) have the same Frobenius number, if and only if \(a_j = 1\).

public theorem_wanted compoundSequence_erase_frobenius_eq_iff (n : ℕ) (a b : ℕ → ℕ)
    (hab : ∀ i ∈ Finset.Icc 1 n, 0 < a i ∧ a i < b i)
    (hcop : ∀ i ∈ Finset.Icc 1 n, ∀ j ∈ Finset.Icc 1 n, j ≤ i → Nat.Coprime (a i) (b j))
    (j : ℕ) (hj : j ≤ n)
    (hgcd : ((Finset.range (n + 1)).erase j).gcd (compoundSequence n a b) = 1) :
    (∃ F : ℤ,
      IsGreatest {m : ℤ | ∀ s ∈ AddSubmonoid.closure ((((Finset.range (n + 1)).erase j).image
        (compoundSequence n a b) : Finset ℕ) : Set ℕ), (s : ℤ) ≠ m} F ∧
      IsGreatest {m : ℤ | ∀ s ∈ AddSubmonoid.closure (((Finset.range (n + 1)).image
        (compoundSequence n a b) : Finset ℕ) : Set ℕ), (s : ℤ) ≠ m} F) ↔ a j = 1

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Theorem 4.

Uses 1

Statement usesCompound sequence

TheoremEmbedding dimension of the semigroup of a compound sequence#●ready to prove

Let \(n\) be a natural number and let \(a_1, \dots, a_n\) and \(b_1, \dots, b_n\) be natural numbers with \(0 < a_i < b_i\) for \(1 \le i \le n\) and \(\gcd(a_i, b_j) = 1\) whenever \(1 \le j \le i \le n\); let \(c_0, \dots, c_n\) be their compound sequence and \(S\) the additive submonoid of \(\mathbb{N}\) generated by \(c_0, \dots, c_n\). Let \(k\) be the number of indices \(1 \le i \le n\) with \(a_i = 1\). Then the minimal generating set of \(S\), the set of nonzero elements of \(S\) that are not a sum of two nonzero elements of \(S\), has exactly \(n - k + 1\) elements; that is, the embedding dimension of \(S\) is \(n - k + 1\).

public theorem_wanted compoundSequence_embeddingDimension (n : ℕ) (a b : ℕ → ℕ)
    (hab : ∀ i ∈ Finset.Icc 1 n, 0 < a i ∧ a i < b i)
    (hcop : ∀ i ∈ Finset.Icc 1 n, ∀ j ∈ Finset.Icc 1 n, j ≤ i → Nat.Coprime (a i) (b j)) :
    let S := AddSubmonoid.closure (((Finset.range (n + 1)).image (compoundSequence n a b) :
      Finset ℕ) : Set ℕ)
    {s | s ∈ S ∧ s ≠ 0 ∧ ∀ x ∈ S, ∀ y ∈ S, x + y = s → x = 0 ∨ y = 0}.ncard =
      n - ((Finset.Icc 1 n).filter fun i => a i = 1).card + 1

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Theorem 5.

Uses 1

Statement usesCompound sequence

TheoremThe minimal generating set as the least Frobenius-preserving subset#●ready to prove

Let \(n\) be a natural number and let \(a_1, \dots, a_n\) and \(b_1, \dots, b_n\) be natural numbers with \(0 < a_i < b_i\) for \(1 \le i \le n\) and \(\gcd(a_i, b_j) = 1\) whenever \(1 \le j \le i \le n\); let \(C = \{c_0, \dots, c_n\}\) be the set of terms of their compound sequence and \(S\) the additive submonoid of \(\mathbb{N}\) generated by \(C\). Say that a set \(G\) of natural numbers has the same Frobenius number as \(S\) if some integer is both the largest integer not in the submonoid generated by \(G\) and the largest integer not in \(S\). Let \(M\) be the minimal generating set of \(S\), the set of nonzero elements of \(S\) that are not a sum of two nonzero elements of \(S\). Then \(M \subseteq C\) and \(M\) has the same Frobenius number as \(S\), and every subset \(C' \subseteq C\) with the same Frobenius number as \(S\) has at least as many elements as \(M\), with the same number of elements only if \(C' = M\).

public theorem_wanted compoundSequence_minimal_generating_set_least (n : ℕ) (a b : ℕ → ℕ)
    (hab : ∀ i ∈ Finset.Icc 1 n, 0 < a i ∧ a i < b i)
    (hcop : ∀ i ∈ Finset.Icc 1 n, ∀ j ∈ Finset.Icc 1 n, j ≤ i → Nat.Coprime (a i) (b j)) :
    let C : Finset ℕ := (Finset.range (n + 1)).image (compoundSequence n a b)
    let S := AddSubmonoid.closure (C : Set ℕ)
    let M : Set ℕ := {s | s ∈ S ∧ s ≠ 0 ∧ ∀ x ∈ S, ∀ y ∈ S, x + y = s → x = 0 ∨ y = 0}
    let SameF : Set ℕ → Prop := fun G => ∃ F : ℤ,
      IsGreatest {m : ℤ | ∀ s ∈ AddSubmonoid.closure G, (s : ℤ) ≠ m} F ∧
        IsGreatest {m : ℤ | ∀ s ∈ S, (s : ℤ) ≠ m} F
    (M ⊆ C ∧ SameF M) ∧
      ∀ C' ⊆ C, SameF C' → M.ncard ≤ C'.card ∧ (C'.card = M.ncard → (C' : Set ℕ) = M)

Sources

• Edgar Federico Elizeche and Amitabha Tripathi, A Note on Deletions from Compound Sequences That Leave the Frobenius Number Invariant, INTEGERS 25 (2025), Article A6, Theorem 6.

Uses 1

Statement usesCompound sequence

3 fully proved6 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.