Difference bases

A difference basis for a finite set $S$ is a finite set $A$ such that every element of $S$ can be written as a difference $a - b$ of two elements $a, b \in A$; equivalently $S \subseteq A - A$. The multiplicative version is a ratio basis ($S \subseteq A / A$).

The classical case $S = \{0, 1, \ldots, N\}$ over $\mathbb{Z}$ (or $\mathbb{N}$) recovers the notion of a restricted difference basis, dual to the recreational notion of a sparse ruler: a difference basis for $\{0, \ldots, N\}$ of minimal size is an optimal ruler of length $N$.

Main definitions

• Finset.IsRatioBasis A S (additive: Finset.IsDifferenceBasis A S): $S \subseteq A / A$.

Main results

• Finset.isRatioBasis_iff: the elementwise characterization.
• Finset.IsRatioBasis.mono_left / Finset.IsRatioBasis.mono_right: monotonicity.
• Finset.IsRatioBasis.card_le_sq: a ratio basis for $S$ has at least $\sqrt{|S|}$ elements, i.e. $|S| \le |A|^2$.

References

• [Wi63] Wichmann, B. "A note on restricted difference bases." Journal of the London Mathematical Society 38 (1963): 465-466.

def Finset.IsRatioBasis {G : Type u_1} [DecidableEq G] [Div G] (A S : Finset G) : Prop

A finset $A$ is a ratio basis for $S$ if every element of $S$ is a ratio $a / b$ of two elements $a, b \in A$, i.e. $S \subseteq A / A$.

Equations

• A.IsRatioBasis S = (S ⊆ A / A)

def Finset.IsDifferenceBasis {G : Type u_1} [DecidableEq G] [Sub G] (A S : Finset G) : Prop

A finset $A$ is a difference basis for $S$ if every element of $S$ is a difference $a - b$ of two elements $a, b \in A$, i.e. $S \subseteq A - A$.

Equations

• A.IsDifferenceBasis S = (S ⊆ A - A)

theorem Finset.isRatioBasis_iff {G : Type u_1} [DecidableEq G] [Div G] {A S : Finset G} : A.IsRatioBasis S ↔ ∀ x ∈ S, ∃ a ∈ A, ∃ b ∈ A, a / b = x

A finset $A$ is a ratio basis for $S$ iff every $x \in S$ is a ratio of two elements of $A$.

theorem Finset.isDifferenceBasis_iff {G : Type u_1} [DecidableEq G] [Sub G] {A S : Finset G} : A.IsDifferenceBasis S ↔ ∀ x ∈ S, ∃ a ∈ A, ∃ b ∈ A, a - b = x

A finset $A$ is a difference basis for $S$ iff every $x \in S$ is a difference of two elements of $A$.

theorem Finset.IsRatioBasis.mono_left {G : Type u_1} [DecidableEq G] [Div G] {A S T : Finset G} (h : A.IsRatioBasis S) (hTS : T ⊆ S) : A.IsRatioBasis T

Shrinking the target set preserves being a ratio basis.

theorem Finset.IsDifferenceBasis.mono_left {G : Type u_1} [DecidableEq G] [Sub G] {A S T : Finset G} (h : A.IsDifferenceBasis S) (hTS : T ⊆ S) : A.IsDifferenceBasis T

Shrinking the target set preserves being a difference basis.

theorem Finset.IsRatioBasis.mono_right {G : Type u_1} [DecidableEq G] [Div G] {A B S : Finset G} (h : A.IsRatioBasis S) (hAB : A ⊆ B) : B.IsRatioBasis S

Enlarging the basis preserves being a ratio basis.

theorem Finset.IsDifferenceBasis.mono_right {G : Type u_1} [DecidableEq G] [Sub G] {A B S : Finset G} (h : A.IsDifferenceBasis S) (hAB : A ⊆ B) : B.IsDifferenceBasis S

Enlarging the basis preserves being a difference basis.

theorem Finset.IsRatioBasis.card_le_sq {G : Type u_1} [DecidableEq G] [Div G] {A S : Finset G} (h : A.IsRatioBasis S) : S.card ≤ A.card ^ 2

A ratio basis for $S$ has at least $\sqrt{|S|}$ elements: $|S| \le |A|^2$.

theorem Finset.IsDifferenceBasis.card_le_sq {G : Type u_1} [DecidableEq G] [Sub G] {A S : Finset G} (h : A.IsDifferenceBasis S) : S.card ≤ A.card ^ 2

A difference basis for $S$ has at least $\sqrt{|S|}$ elements: $|S| \le |A|^2$.