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 allUniqueSums {α : Type u_1} [AddCommMonoid α] (A : Set α) : Set α

allUniqueSums A is the set of elements in α that can be written as the sum of exactly one unordered pair of elements from A.

Equations

• allUniqueSums A = {n : α | ∃ (p : α × α), p.1 ∈ A ∧ p.2 ∈ A ∧ p.1 + p.2 = n ∧ ∀ a₁ ∈ A, ∀ a₂ ∈ A, a₁ + a₂ = n → a₁ = p.1 ∧ a₂ = p.2 ∨ a₁ = p.2 ∧ a₂ = p.1}

def HasNoUniqueRepresentation {α : Type u_2} [AddCommMonoid α] (A : Finset α) : Prop

A set A has no unique representation in its sumset A + A if for every pair of elements a₁, a₂ ∈ A, there exist another pair of elements b₁, b₂ ∈ A such that a₁ + a₂ = b₁ + b₂ and {a₁, a₂} ≠ {b₁, b₂}.

Equations

• HasNoUniqueRepresentation A = (allUniqueSums ↑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 α] (A : Set α) : 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₁

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.

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

Equations

• A.instDecidableIsSidonCoeOfDecidableEq = 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 = {B ∈ A.powerset | IsSidon ↑B}.sup Finset.card

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

def Finset.greedySidon.go (A : Finset ℕ) (hA : IsSidon ↑A) (m : ℕ) : { m' : ℕ // m' ≥ m ∧ m' ∉ A ∧ IsSidon ↑(A ∪ {m'}) }

Given a finite Sidon set A and a lower bound m, go finds the smallest number m' ≥ m such that A ∪ {m'} is Sidon. If A is empty then this returns the value m. Note that the lower bound is required to avoid 0 being a contender in some cases.

Equations

• Finset.greedySidon.go A hA m = if h : A.Nonempty then have this := ⋯; ⟨Nat.find this, ⋯⟩ else ⟨m, ⋯⟩

def Finset.greedySidon.aux (n : ℕ) : { A : Finset ℕ // IsSidon ↑A } × ℕ

Main search loop for generating the greedy Sidon sequence. The return value for step n is the finite set of numbers generated so far, a proof that it is Sidon, and the greatest element of the finite set at that point. This is initialised at {1}, then greedySidon.go is called iteratively using the lower bound max + 1 to find the next smallest Sidon preserving number.

Equations

• One or more equations did not get rendered due to their size.
• Finset.greedySidon.aux 0 = (⟨{1}, Finset.greedySidon.aux._proof_5⟩, 1)

def Finset.greedySidon (n : ℕ) : ℕ

greedySidon is the sequence obtained by the initial set $\{1\}$ and iteratively obtaining the next smallest integer that preserves the Sidon property of the set. This gives the sequence 1, 2, 4, 8, 13, 21, 31, ....

Equations

• Finset.greedySidon n = (Finset.greedySidon.aux n).2

def Finset.greedySidonBelow (N : ℕ) : Finset ℕ

The greedy Sidon set in {1, …, N}: starting from ∅, iterate through 1, …, N and include x if and only if A ∪ {x} remains Sidon. Alternatively, this is precisely the set of elements in the greedy Sidon sequence that are ≤ N.

Equations

• Finset.greedySidonBelow N = {x ∈ ↑(Finset.greedySidon.aux N).1 | x ≤ N}