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

@[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})