Sidon sets

This file defines the multiplicative predicate IsMulSidon for sets in commutative monoids, and the additive predicate IsAddSidon generated from it. A set is multiplicatively Sidon if whenever a * b = c * d for elements a, b, c, d of the set, then either a = c and b = d, or a = d and b = c. Additively, products are replaced by sums. The two elements in each pair are not required to be distinct.

Main declarations

• IsMulSidon/IsAddSidon: Predicates for a set to be Sidon.

Tags

Sidon set, additive combinatorics

def IsMulSidon {G : Type u_1} [CommMonoid G] (A : Set G) : Prop

A set A is multiplicatively Sidon if whenever a * b = c * d for elements a, b, c, d of A, then either a = c and b = d, or a = d and b = c. The two elements in each pair are not required to be distinct.

Equations

• IsMulSidon A = ∀ ⦃a : G⦄, a ∈ A → ∀ ⦃b : G⦄, b ∈ A → ∀ ⦃c : G⦄, c ∈ A → ∀ ⦃d : G⦄, d ∈ A → a * b = c * d → a = c ∧ b = d ∨ a = d ∧ b = c

def IsAddSidon {G : Type u_1} [AddCommMonoid G] (A : Set G) : Prop

A set A is additively Sidon if whenever a + b = c + d for elements a, b, c, d of A, then either a = c and b = d, or a = d and b = c. The two elements in each pair are not required to be distinct.

Equations

• IsAddSidon A = ∀ ⦃a : G⦄, a ∈ A → ∀ ⦃b : G⦄, b ∈ A → ∀ ⦃c : G⦄, c ∈ A → ∀ ⦃d : G⦄, d ∈ A → a + b = c + d → a = c ∧ b = d ∨ a = d ∧ b = c

theorem IsMulSidon.mono {G : Type u_1} [CommMonoid G] {A B : Set G} (hAB : A ⊆ B) (hB : IsMulSidon B) : IsMulSidon A

A subset of a Sidon set is Sidon.

theorem IsAddSidon.mono {G : Type u_1} [AddCommMonoid G] {A B : Set G} (hAB : A ⊆ B) (hB : IsAddSidon B) : IsAddSidon A

A subset of an additively Sidon set is additively Sidon.

@[simp]

theorem IsMulSidon.empty {G : Type u_1} [CommMonoid G] : IsMulSidon ∅

The empty set is Sidon.

@[simp]

theorem IsAddSidon.empty {G : Type u_1} [AddCommMonoid G] : IsAddSidon ∅

The empty set is additively Sidon.

theorem IsMulSidon.of_subsingleton {G : Type u_1} [CommMonoid G] {A : Set G} (hA : A.Subsingleton) : IsMulSidon A

A subsingleton set is Sidon.

theorem IsAddSidon.of_subsingleton {G : Type u_1} [AddCommMonoid G] {A : Set G} (hA : A.Subsingleton) : IsAddSidon A

A subsingleton set is additively Sidon.

@[simp]

theorem IsMulSidon.singleton {G : Type u_1} [CommMonoid G] (a : G) : IsMulSidon {a}

A singleton is Sidon.

@[simp]

theorem IsAddSidon.singleton {G : Type u_1} [AddCommMonoid G] (a : G) : IsAddSidon {a}

A singleton is additively Sidon.

theorem IsMulSidon.iUnion {G : Type u_1} [CommMonoid G] {ι : Sort u_2} {A : ι → Set G} (hA : Directed (fun (x1 x2 : Set G) => x1 ⊆ x2) A) (h : ∀ (i : ι), IsMulSidon (A i)) : IsMulSidon (⋃ (i : ι), A i)

A directed union of Sidon sets is Sidon.

theorem IsAddSidon.iUnion {G : Type u_1} [AddCommMonoid G] {ι : Sort u_2} {A : ι → Set G} (hA : Directed (fun (x1 x2 : Set G) => x1 ⊆ x2) A) (h : ∀ (i : ι), IsAddSidon (A i)) : IsAddSidon (⋃ (i : ι), A i)

A directed union of additively Sidon sets is additively Sidon.

theorem IsMulSidon.sUnion {G : Type u_1} [CommMonoid G] {S : Set (Set G)} (hS : DirectedOn (fun (x1 x2 : Set G) => x1 ⊆ x2) S) (h : ∀ A ∈ S, IsMulSidon A) : IsMulSidon (⋃₀ S)

A directed union of Sidon sets is Sidon.

theorem IsAddSidon.sUnion {G : Type u_1} [AddCommMonoid G] {S : Set (Set G)} (hS : DirectedOn (fun (x1 x2 : Set G) => x1 ⊆ x2) S) (h : ∀ A ∈ S, IsAddSidon A) : IsAddSidon (⋃₀ S)

A directed union of additively Sidon sets is additively Sidon.

theorem IsMulSidon.pair {G : Type u_1} [CommGroup G] [IsMulTorsionFree G] (a b : G) : IsMulSidon {a, b}

A pair in a torsion-free group is Sidon.

theorem IsAddSidon.pair {G : Type u_1} [AddCommGroup G] [IsAddTorsionFree G] (a b : G) : IsAddSidon {a, b}

A pair in a torsion-free group is additively Sidon.