def IsSumFree {α : Type u_1} [AddCommMonoid α] (A : Set α) : Prop

A set $A$ is said to be sum-free if the sumset $A + A$ is disjoint from $A$, i.e. if the equation $a + b = c$ has no solution with $a, b, c \in A$.

Equations

• IsSumFree A = Disjoint (A + A) A

def IsSyndetic (A : Set ℕ) : Prop

A set $A$ of natural numbers is said to have bounded gaps if there exists an integer $p$ such that $A ∩ [n, n + 1, ..., n + p]$ is nonempty for all $n$.

Equations

• IsSyndetic A = ∃ (p : ℕ), ∀ (n : ℕ), (A ∩ Set.Icc n (n + p)).Nonempty

def IsSidon {α : Type u_1} [AddCommMonoid α] {S : Type u_2} [Membership α S] (A : S) : Prop

A Sidon set is a set, such that such that all pairwise sums of elements are distinct apart from coincidences forced by the commutativity of addition.

Equations

• IsSidon A = ∀ i₁ ∈ A, ∀ j₁ ∈ A, ∀ i₂ ∈ A, ∀ j₂ ∈ A, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁

@[simp]

theorem coe {α : Type u_1} [AddCommMonoid α] {S : Type u_2} [SetLike S α] {A : S} : IsSidon ↑A ↔ IsSidon A

theorem Set.IsSidon.avoids_isAPOfLength_three {A : Set ℕ} (hA : IsSidon A) {Y : Set ℕ} (hY : Y.IsAPOfLength 3) : (A ∩ Y).ncard ≤ 2

theorem Set.IsSidon.subset {α : Type u_1} [AddCommMonoid α] {A B : Set α} (hB : IsSidon B) (hAB : A ⊆ B) : IsSidon A

theorem Set.IsSidon.insert {α : Type u_1} [AddCommMonoid α] {A : Set α} {m : α} [IsRightCancelAdd α] [IsLeftCancelAdd α] (hA : IsSidon A) : IsSidon (A ∪ {m}) ↔ m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c

Maximal Sidon sets in an interval.

We follow the convention that IsMaximalSidonSetIn A N means A ⊆ {1, …, N} is Sidon and is inclusion-maximal among subsets of Set.Icc 1 N with the Sidon property.

def Set.IsMaximalSidonSetIn (A : Set ℕ) (N : ℕ) : Prop

IsMaximalSidonSetIn A N means A ⊆ {1, …, N} is Sidon and cannot be extended within {1, …, N} while remaining Sidon.

Equations

• A.IsMaximalSidonSetIn N = (A ⊆ Set.Icc 1 N ∧ IsSidon A ∧ ∀ ⦃x : ℕ⦄, x ∈ Set.Icc 1 N → x ∉ A → ¬IsSidon (A ∪ {x}))

theorem Set.IsMaximalSidonSetIn.subset {A : Set ℕ} {N : ℕ} (hA : A.IsMaximalSidonSetIn N) : A ⊆ Icc 1 N

If A is a maximal Sidon set in {1, …, N}, then A ⊆ {1, …, N}.

theorem Set.IsMaximalSidonSetIn.isSidon {A : Set ℕ} {N : ℕ} (hA : A.IsMaximalSidonSetIn N) : IsSidon A

If A is a maximal Sidon set in {1, …, N}, then A is Sidon.

theorem Set.IsMaximalSidonSetIn.maximal {A : Set ℕ} {N : ℕ} (hA : A.IsMaximalSidonSetIn N) {x : ℕ} (hx : x ∈ Icc 1 N) (hxA : x ∉ A) : ¬IsSidon (A ∪ {x})

Maximality condition unpacked.

@[simp]

theorem Finset.isSidon_toSet {α : Type u_1} [AddCommMonoid α] {A : Finset α} : IsSidon ↑A ↔ IsSidon A

instance Finset.instDecidableIsSidonOfDecidableEq {α : Type u_1} [AddCommMonoid α] (A : Finset α) [DecidableEq α] : Decidable (IsSidon A)

Equations

• A.instDecidableIsSidonOfDecidableEq = decidable_of_iff (∀ i₁ ∈ A, ∀ j₁ ∈ A, ∀ i₂ ∈ A, ∀ j₂ ∈ A, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁) ⋯

def Finset.maxSidonSubsetCard {α : Type u_1} [AddCommMonoid α] (A : Finset α) [DecidableEq α] : ℕ

The maximum size of a Sidon set in the supplied Finset.

Equations

• A.maxSidonSubsetCard = (Finset.filter IsSidon A.powerset).sup Finset.card

theorem Finset.IsSidon.insert {α : Type u_1} [AddCommMonoid α] {A : Finset α} {m : α} [DecidableEq α] [IsRightCancelAdd α] [IsLeftCancelAdd α] (hA : IsSidon A) : IsSidon (A ∪ {m}) ↔ m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c

theorem Finset.IsSidon.insert_ge_max' {A : Finset ℕ} (h : A.Nonempty) (hA : IsSidon A) {s : ℕ} (hs : 2 * A.max' h + 1 ≤ s) : IsSidon (A ∪ {s})

If A is finite Sidon, then A ∪ {s} is also Sidon provided s ≥ A.max + 1.

theorem Finset.IsSidon.exists_insert {A : Finset ℕ} (h : A.Nonempty) (hA : IsSidon A) : ∃ m ∉ A, IsSidon (A ∪ {m})

theorem Finset.IsSidon.exists_insert_ge {A : Finset ℕ} (h : A.Nonempty) (hA : IsSidon A) (s : ℕ) : ∃ m ≥ s, m ∉ A ∧ IsSidon (A ∪ {m})