Documentation

Mathlib.NumberTheory.FrobeniusNumber

Frobenius Number #

In this file we first define a predicate for Frobenius numbers, then solve the 2-variable variant of this problem. We also show the Frobenius number exists for any set of coprime natural numbers that doesn't contain 1. This is closely related to the fact that all ideals of ℕ are finitely generated, which we also prove in this file.

Theorem Statement #

Given a finite set of relatively prime integers all greater than 1, their Frobenius number is the largest positive integer that cannot be expressed as a sum of nonnegative multiples of these integers. Here we show the Frobenius number of two relatively prime integers m and n greater than 1 is m * n - m - n. This result is also known as the Chicken McNugget Theorem.

Implementation Notes #

First we define Frobenius numbers in general using IsGreatest and AddSubmonoid.closure. Then we proceed to compute the Frobenius number of m and n.

For the upper bound, we begin with an auxiliary lemma showing m * n is not attainable, then show m * n - m - n is not attainable. Then for the construction, we create a k_1 which is k mod n and 0 mod m, then show it is at most k. Then k_1 is a multiple of m, so (k-k_1) is a multiple of n, and we're done.

Tags #

frobenius number, chicken mcnugget, chinese remainder theorem, AddSubmonoid.closure

source
def FrobeniusNumber (n : ℕ) (s : Set ℕ) :
Prop

A natural number n is the Frobenius number of a set of natural numbers s if it is an upper bound on the complement of the additive submonoid generated by s. In other words, it is the largest number that cannot be expressed as a sum of numbers in s.

Equations
Instances For
    source
    theorem frobeniusNumber_iff {n : ℕ} {s : Set ℕ} :
    FrobeniusNumber n s ↔ n ∉ AddSubmonoid.closure s ∧ ∀ k > n, k ∈ AddSubmonoid.closure s
    source
    theorem frobeniusNumber_pair {m n : ℕ} (cop : m.Coprime n) (hm : 1 < m) (hn : 1 < n) :
    FrobeniusNumber (m * n - m - n) {m, n}

    The Chicken McNugget theorem stating that the Frobenius number of positive numbers m and n is m * n - m - n.

    source
    noncomputable def Nat.setGcd (s : Set ℕ) :
    ℕ

    The gcd of a set of natural numbers is defined to be the nonnegative generator of the ideal of ℤ generated by them.

    Equations
    Instances For
      source
      theorem Nat.setGcd_dvd_of_mem {s : Set ℕ} {n : ℕ} (h : n ∈ s) :
      setGcd s ∣ n
      source
      theorem Nat.setGcd_dvd_of_mem_closure {s : Set ℕ} {n : ℕ} (h : n ∈ AddSubmonoid.closure s) :
      setGcd s ∣ n
      source
      theorem Nat.dvd_setGcd_iff {s : Set ℕ} {n : ℕ} :
      n ∣ setGcd s ↔ ∀ m ∈ s, n ∣ m

      The characterizing property of Nat.setGcd.

      source
      theorem Nat.setGcd_mono {s t : Set ℕ} (h : s ⊆ t) :
      setGcd t ∣ setGcd s
      source
      theorem Nat.dvdNotUnit_setGcd_insert {s : Set ℕ} {n : ℕ} (h : ¬setGcd s ∣ n) :
      DvdNotUnit (setGcd (insert n s)) (setGcd s)
      source
      theorem Nat.setGcd_insert_of_dvd {s : Set ℕ} {n : ℕ} (h : setGcd s ∣ n) :
      setGcd (insert n s) = setGcd s
      source
      theorem Nat.setGcd_eq_zero_iff {s : Set ℕ} :
      setGcd s = 0 ↔ s ⊆ {0}
      source
      theorem Nat.exists_ne_zero_of_setGcd_ne_zero {s : Set ℕ} (hs : setGcd s ≠ 0) :
      ∃ n ∈ s, n ≠ 0
      source
      theorem Nat.span_singleton_setGcd (s : Set ℕ) :
      Ideal.span {↑(setGcd s)} = Ideal.span (Nat.cast '' s)
      source
      theorem Nat.subset_span_setGcd (s : Set ℕ) :
      s ⊆ ↑(Ideal.span {setGcd s})
      source
      theorem Nat.exists_mem_span_nat_finset_of_ge (s : Set ℕ) :
      ∃ (t : Finset ℕ) (n : ℕ), ↑t ⊆ s ∧ ∀ m ≥ n, setGcd s ∣ m → m ∈ Ideal.span ↑t
      source
      theorem Nat.exists_mem_closure_of_ge (s : Set ℕ) :
      ∃ (n : ℕ), ∀ m ≥ n, setGcd s ∣ m → m ∈ AddSubmonoid.closure s
      source
      theorem Nat.finite_setOf_setGcd_dvd_and_mem_span (s : Set ℕ) :
      {n : ℕ | setGcd s ∣ n ∧ n ∉ Ideal.span s}.Finite
      source
      instance Nat.instIsNoetherian :
      IsNoetherian ℕ ℕ

      ℕ is a Noetherian ℕ-module, i.e., ℕ is a Noetherian semiring.

      source
      theorem Nat.addSubmonoid_fg (s : AddSubmonoid ℕ) :
      s.FG
      source
      theorem exists_frobeniusNumber_iff {s : Set ℕ} :
      (∃ (n : ℕ), FrobeniusNumber n s) ↔ Nat.setGcd s = 1 ∧ 1 ∉ s

      A set of natural numbers has a Frobenius number iff their gcd is 1; if 1 is in the set, the Frobenius number is -1, so the Frobenius number doesn't exist as a natural number. Wikipedia seems to attribute this to Issai Schur, but Schur's theorem is a more precise statement about asymptotics of the number of ℕ-linear combinations, and the existence of the Frobenius number for a set with gcd 1 is probably well known before that.