Greedy B_h-sets

DefinitionNext term of a greedy \(B_h\)-set#✓fully proved

Let \(h\) and \(a\) be natural numbers and \(A\) a set of natural numbers. Then \(a\) is the next greedy \(B_h\) choice after \(A\) if \(a\) is greater than every element of \(A\), the set \(A \cup \{a\}\) is a \(B_h\)-set, and for every natural number \(b < a\) that is greater than every element of \(A\), the set \(A \cup \{b\}\) is not a \(B_h\)-set.

def IsNextGreedyBh (h : ℕ) (A : Set ℕ) (a : ℕ) : Prop :=
  (∀ x ∈ A, x < a) ∧ AdditiveCombinatorics.IsBhSet (insert a A) h ∧
    ∀ b : ℕ, (∀ x ∈ A, x < b) → b < a →
      ¬AdditiveCombinatorics.IsBhSet (insert b A) h

Uses 1 · Used by 1

Statement uses\(B_h\)-set

Used byFourth positive term of the greedy \(B_h\)-set

DefinitionFourth positive term of the greedy \(B_h\)-set#✓fully proved

For natural numbers \(h\) and \(a\), we say that \(a\) is the fourth positive element \(a_4(h)\) of the greedy \(B_h\)-set if \(1\) is the next greedy \(B_h\) choice after \(\{0\}\), \(h + 1\) is the next greedy \(B_h\) choice after \(\{0, 1\}\), \(h^2 + h + 1\) is the next greedy \(B_h\) choice after \(\{0, 1, h + 1\}\), and \(a\) is the next greedy \(B_h\) choice after \(\{0, 1, h + 1, h^2 + h + 1\}\).

def IsFourthGreedyBh (h a : ℕ) : Prop :=
  IsNextGreedyBh h {0} 1 ∧
    IsNextGreedyBh h {0, 1} (h + 1) ∧
    IsNextGreedyBh h {0, 1, h + 1} (h ^ 2 + h + 1) ∧
    IsNextGreedyBh h {0, 1, h + 1, h ^ 2 + h + 1} a

Uses 1 · Used by 3

Statement usesNext term of a greedy \(B_h\)-set

Used byLower bound for the fourth greedy \(B_h\) term · Formula for the fourth greedy \(B_h\) term · Upper bound for the fourth greedy \(B_h\) term

DefinitionQuasipolynomial for the fourth greedy \(B_h\) term#✓fully proved

For a natural number \(h\), the value \(v(h)\) is \((h^3 + 3h^2 + 3h + 1)/2\) if \(h\) is odd and \((h^3 + 2h^2 + 3h + 2)/2\) if \(h\) is even.

Both numerators are even, so the divisions are exact.

def fourthValue (h : ℕ) : ℕ :=
  if Odd h then (h ^ 3 + 3 * h ^ 2 + 3 * h + 1) / 2
  else (h ^ 3 + 2 * h ^ 2 + 3 * h + 2) / 2

Used by 3

Used byLower bound for the fourth greedy \(B_h\) term · Formula for the fourth greedy \(B_h\) term · Upper bound for the fourth greedy \(B_h\) term

TheoremFormula for the fourth greedy \(B_h\) term#●ready to prove

For every integer \(h \ge 1\), the fourth positive element \(a_4(h)\) of the greedy \(B_h\)-set is \((h^3 + 3h^2 + 3h + 1)/2\) if \(h\) is odd and \((h^3 + 2h^2 + 3h + 2)/2\) if \(h\) is even.

theorem_wanted isFourthGreedyBh_fourthValue
    (h : ℕ) (hh : 0 < h) :
    IsFourthGreedyBh h (fourthValue h)

Sources

• Melvyn B. Nathanson and Kevin O'Bryant, "The Fourth Positive Element in the Greedy B_h-Set", Theorem 1.

Uses 2

Statement usesFourth positive term of the greedy \(B_h\)-set · Quasipolynomial for the fourth greedy \(B_h\) term

TheoremLower bound for the fourth greedy \(B_h\) term#●ready to prove

Let \(h\) and \(a\) be natural numbers with \(h \ge 2\). If \(a\) is the fourth positive element \(a_4(h)\) of the greedy \(B_h\)-set, then \(a \ge v(h)\), where \(v(h) = (h^3 + 3h^2 + 3h + 1)/2\) if \(h\) is odd and \(v(h) = (h^3 + 2h^2 + 3h + 2)/2\) if \(h\) is even.

theorem_wanted fourthValue_le_of_isFourthGreedyBh
    (h a : ℕ) (hh : 2 ≤ h) (ha : IsFourthGreedyBh h a) :
    fourthValue h ≤ a

Sources

• Melvyn B. Nathanson and Kevin O'Bryant, "The Fourth Positive Element in the Greedy B_h-Set", Lemma 2.

Uses 2

Statement usesFourth positive term of the greedy \(B_h\)-set · Quasipolynomial for the fourth greedy \(B_h\) term

TheoremUpper bound for the fourth greedy \(B_h\) term#●ready to prove

Let \(h\) and \(a\) be natural numbers with \(h \ge 1\). If \(a\) is the fourth positive element \(a_4(h)\) of the greedy \(B_h\)-set, then \(a \le v(h)\), where \(v(h) = (h^3 + 3h^2 + 3h + 1)/2\) if \(h\) is odd and \(v(h) = (h^3 + 2h^2 + 3h + 2)/2\) if \(h\) is even.

theorem_wanted isFourthGreedyBh_le_fourthValue
    (h a : ℕ) (hh : 0 < h) (ha : IsFourthGreedyBh h a) :
    a ≤ fourthValue h

Sources

• Melvyn B. Nathanson and Kevin O'Bryant, "The Fourth Positive Element in the Greedy B_h-Set", Lemma 3.

Uses 2

Statement usesFourth positive term of the greedy \(B_h\)-set · Quasipolynomial for the fourth greedy \(B_h\) term

3 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.