Restricted additive bases

DefinitionMinimum size of a restricted additive basis#✓fully proved

Let \(s\) be a natural number. A restricted additive basis of \(\{0, 1, \dots, s\}\) is a finite set \(A\) of natural numbers with \(2a \le s\) for every \(a \in A\) such that every natural number \(x \le s\) can be written as \(x = a + b\) with \(a, b \in A\), where \(a = b\) is allowed. The minimum restricted additive basis size \(k^*(s)\) is the smallest cardinality of a restricted additive basis of \(\{0, 1, \dots, s\}\); it is undefined when no restricted additive basis of \(\{0, 1, \dots, s\}\) exists.

The restriction \(2a \le s\) is imposed for odd \(s\) as well as for even \(s\).

MetaMathlibExt.minimumRestrictedAdditiveBasisCard · 36 lines

public noncomputable def minimumRestrictedAdditiveBasisCard (s : Nat) :
    { opt : Option Nat //
      (∀ k : Nat, opt = some k →
        ((∃ A : Finset Nat, (∀ a ∈ A, 2 * a ≤ s) ∧
          (∀ x : Nat, x ≤ s → ∃ a ∈ A, ∃ b ∈ A, a + b = x) ∧ A.card = k) ∧
          (∀ B : Finset Nat, (∀ b ∈ B, 2 * b ≤ s) →
            (∀ x : Nat, x ≤ s → ∃ a ∈ B, ∃ b ∈ B, a + b = x) → k ≤ B.card))) ∧
      (opt = none →
        ¬∃ A : Finset Nat, (∀ a ∈ A, 2 * a ≤ s) ∧
          (∀ x : Nat, x ≤ s → ∃ a ∈ A, ∃ b ∈ A, a + b = x)) } := by
  by_cases h : ∃ A : Finset Nat, (∀ a ∈ A, 2 * a ≤ s) ∧
      ∀ x : Nat, x ≤ s → ∃ a ∈ A, ∃ b ∈ A, a + b = x
  · have hex : ∃ k, ∃ A : Finset Nat, ((∀ a ∈ A, 2 * a ≤ s) ∧
        (∀ x : Nat, x ≤ s → ∃ a ∈ A, ∃ b ∈ A, a + b = x)) ∧ A.card = k := by
      obtain ⟨A₀, hA₀⟩ := h
      exact ⟨A₀.card, A₀, hA₀, rfl⟩
    refine ⟨some (Nat.find hex), ?_, ?_⟩
    · intro k hk
      have hk' : Nat.find hex = k := Option.some_inj.mp hk
      subst hk'
      obtain ⟨A, hA, hcard⟩ := Nat.find_spec hex
      obtain ⟨hbound, hcover⟩ := hA
      refine ⟨⟨A, hbound, hcover, hcard⟩, ?_⟩
      intro B hBbound hBcover
      have hmem : ∃ A : Finset Nat, ((∀ a ∈ A, 2 * a ≤ s) ∧
          (∀ x : Nat, x ≤ s → ∃ a ∈ A, ∃ b ∈ A, a + b = x)) ∧
          A.card = B.card :=
        ⟨B, ⟨hBbound, hBcover⟩, rfl⟩
      exact Nat.find_min' hex hmem
    · intro hnone
      cases hnone
  · refine ⟨none, ?_, ?_⟩
    · intro k hk
      cases hk
    · intro _ hx
      exact h hx

Sources

• Jukka Kohonen, Visa Koivunen, and Robin Rajamäki, Planar Additive Bases for Rectangles, Journal of Integer Sequences 21 (2018), Article 18.9.8: additive-basis notion (A + A ⊇ [0, n]), lines 126–128; one-dimensional restricted basis (A ⊆ [0, n/2]), lines 170–171; minimum restricted-basis notation k^*, lines 200–203, https://cs.uwaterloo.ca/journals/JIS/VOL21/Rajamaki/raj.tex. The one-dimensional k^*(s, 0) notion supports G. Yu's restricted 2-basis bound (s_x / k^*(s_x, 0)^2 ≤ 0.41983, equation eq:yu_restr, lines 897–901), quoting G. Yu, Upper bounds for finite additive 2-bases, Proc. Amer. Math. Soc. 137 (2009), 11–18, Theorem 1.2.

Used by 2

Used byThe minimum restricted additive basis size is undefined exactly in the odd case · The minimum restricted additive basis size is defined exactly in the even case

TheoremThe minimum restricted additive basis size is undefined exactly in the odd case#✓fully proved

For every natural number \(s\), the minimum size \(k^*(s)\) of a restricted additive basis of \(\{0, 1, \dots, s\}\), that is, of a finite set \(A\) of natural numbers with \(2a \le s\) for every \(a \in A\) such that every natural number \(x \le s\) equals \(a + b\) for some \(a, b \in A\), is undefined if and only if \(s\) is odd.

public theorem minimumRestrictedAdditiveBasisCard_eq_none_iff (s : ℕ) :
    (minimumRestrictedAdditiveBasisCard s).val = none ↔ s % 2 = 1

Uses 1

Statement usesMinimum size of a restricted additive basis

TheoremThe minimum restricted additive basis size is defined exactly in the even case#✓fully proved

For every natural number \(s\), the minimum size \(k^*(s)\) of a restricted additive basis of \(\{0, 1, \dots, s\}\), that is, of a finite set \(A\) of natural numbers with \(2a \le s\) for every \(a \in A\) such that every natural number \(x \le s\) equals \(a + b\) for some \(a, b \in A\), is defined if and only if \(s\) is even.

public theorem minimumRestrictedAdditiveBasisCard_isSome_iff (s : ℕ) :
    (minimumRestrictedAdditiveBasisCard s).val.isSome ↔ s % 2 = 0

Uses 1

Statement usesMinimum size of a restricted additive basis

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.