B_h-sets

DefinitionSum of a nonempty list#✓fully proved

For a nonempty list \((a_1, \dots, a_k)\) of elements of a type with an addition, its sum is obtained by adding the entries from left to right starting from the head: it is \(a_1\) when \(k = 1\), and \((\cdots((a_1 + a_2) + a_3) + \cdots) + a_k\) in general. No zero element is needed, and the proof that the list is nonempty does not affect the value.

public def sumNE {G : Type*} [Add G] : (l : List G) → l ≠ [] → G
  | [], h => absurd rfl h
  | a :: t, _ => t.foldl (· + ·) a

Used by 4

Used by\(B_h\)-set · The sum of a nonempty list does not depend on the nonemptiness proof · \(R_h(1) = 1\) · The shortest interval holding a one-element \(B_h\)-set

TheoremThe sum of a nonempty list does not depend on the nonemptiness proof#✓fully proved

For every list \(l\) of elements of a type with an addition and any two proofs \(e_1\) and \(e_2\) that \(l\) is nonempty, the sum of \(l\) computed with \(e_1\) equals the sum of \(l\) computed with \(e_2\).

public theorem sumNE_proof_irrel {G : Type*} [Add G] (l : List G) (e₁ e₂ : l ≠ []) :
    sumNE l e₁ = sumNE l e₂

Uses 1

Statement usesSum of a nonempty list

Definition\(B_h\)-set#✓fully proved

Let \(G\) be an additive commutative semigroup, \(A \subseteq G\) and \(h\) a natural number. \(A\) is a \(B_h\)-set if \(A\) is nonempty, \(h \ge 1\), and whenever two sequences \((a_1, \dots, a_h)\) and \((b_1, \dots, b_h)\) of elements of \(A\) satisfy \(a_1 + \dots + a_h = b_1 + \dots + b_h\), the sequence \((b_1, \dots, b_h)\) is a rearrangement of \((a_1, \dots, a_h)\).

Repeated summands are allowed: the entries of each sequence need not be distinct. No zero element is assumed.

public def IsBhSet {G : Type*} [AddCommSemigroup G] (A : Set G) (h : ℕ) : Prop :=
  A.Nonempty ∧ 0 < h ∧
    ∀ (l₁ l₂ : List G),
      (∀ x ∈ l₁, x ∈ A) →
      (∀ x ∈ l₂, x ∈ A) →
      l₁.length = h →
      l₂.length = h →
      ∀ (e₁ : l₁ ≠ []) (e₂ : l₂ ≠ []),
        sumNE l₁ e₁ = sumNE l₂ e₂ → l₁.Perm l₂

Uses 1 · Used by 8

Statement usesSum of a nonempty list

Used byMaximum size of a \(B_h\)-set in \(\{1, \dots, n\}\) · \(R_h(n)\) is at most \(n\) · \(R_h(1) = 1\) · Shortest interval containing a \(B_h\)-set of given size · The shortest interval holding a one-element \(B_h\)-set · Bose's construction of \(B_h\)-sets · Singer's construction of \(B_h\)-sets · Next term of a greedy \(B_h\)-set

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.