/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module
public import FormalConjecturesForMathlib.Combinatorics.AP.Basic
public import Mathlib.Analysis.Normed.Field.Lemmas
public import Mathlib.Order.CompletePartialOrder@[expose] public sectionopen Function Setopen scoped Pointwisevariable {α : Type*} [AddCommMonoid α]A set $S$ is said to be product-free if the product set $S \cdot S$ is disjoint from $S$, i.e. if the equation $x \cdot y = z$ has no solution with $x, y, z \in S$.
@[to_additive IsSumFree 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$.
]
def IsProductFree {M : Type*} [Mul M] (S : Set M) : Prop := Disjoint (S * S) S@[to_additive isSumFree_iff]
theorem isProductFree_iff {M : Type*} [Mul M] {S : Set M} :
IsProductFree S ↔ ∀ x ∈ S, ∀ y ∈ S, x * y ∉ S := M:Type u_2inst✝:Mul MS:Set M⊢ IsProductFree S ↔ ∀ x ∈ S, ∀ y ∈ S, x * y ∉ S
M:Type u_2inst✝:Mul MS:Set M⊢ (∀ ⦃a : M⦄, ∀ x ∈ S, ∀ x_1 ∈ S, x * x_1 = a → a ∉ S) ↔ ∀ x ∈ S, ∀ y ∈ S, x * y ∉ S
All goals completed! 🐙
allUniqueSums A is the set of elements in α that can be written as the sum of exactly one
unordered pair of elements from A.
def allUniqueSums (A : Set α) : Set α :=
{ 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) }
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₂}.
def HasNoUniqueRepresentation {α : Type*} [AddCommMonoid α] (A : Finset α) : Prop :=
allUniqueSums (A : Set α) = ∅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$.
def IsSyndetic (A : Set ℕ) : Prop := ∃ p, ∀ n, (A ∩ .Icc n (n + p)).NonemptyA 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.
def IsSidon (A : Set α) : Prop := ∀ᵉ (i₁ ∈ A) (j₁ ∈ A) (i₂ ∈ A) (j₂ ∈ A),
i₁ + i₂ = j₁ + j₂ → (i₁ = j₁ ∧ i₂ = j₂) ∨ (i₁ = j₂ ∧ i₂ = j₁)namespace SetA:Set ℕhA:IsSidon AY:Set ℕhc:Y.encard = 3a:ℕd:ℕhY:Y = {x | ∃ n < 3, a + n * d = x}hY_card:Y.ncard = 3h:2 < (A ∩ Y).ncardhss:Y ⊆ A ∩ Yha:a ∈ Aha₁:a + d ∈ Aha₂:a + 2 • d ∈ Athis:a = a + d ∧ a + 2 • d = a + d ∨ a = a + d ∧ a + 2 • d = a + d⊢ False
A:Set ℕhA:IsSidon AY:Set ℕhc:Y.encard = 3a:ℕd:ℕhY:Y = {x | ∃ n < 3, a + n * d = x}hY_card:Y.ncard = 3h:2 < (A ∩ Y).ncardhss:Y ⊆ A ∩ Yha:a ∈ Aha₁:a + d ∈ Aha₂:a + 2 • d ∈ Athis:d = 0 ∧ 2 * d = d⊢ False
A:Set ℕhA:IsSidon AY:Set ℕhc:Y.encard = 3a:ℕd:ℕhY:Y = {x | ∃ n < 3, a + n * d = x}h:2 < (A ∩ Y).ncardhss:Y ⊆ A ∩ Yha:a ∈ Aha₁:a + d ∈ Aha₂:a + 2 • d ∈ Athis:d = 0 ∧ 2 * d = dhY_card:({a | ∃ x, x < 3} ∩ {a}).ncard = 3⊢ False
All goals completed! 🐙theorem IsSidon.subset {A B : Set α} (hB : IsSidon B) (hAB : A ⊆ B) : IsSidon A :=
fun _ _ _ _ _ _ _ _ _ ↦ hB _ (hAB ‹_›) _ (hAB ‹_›) _ (hAB ‹_›) _ (hAB ‹_›) ‹_›theorem IsSidon.insert {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) := α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon A⊢ IsSidon (A ∪ {m}) ↔ m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∈ A⊢ IsSidon (A ∪ {m}) ↔ m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + cα:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ A⊢ IsSidon (A ∪ {m}) ↔ m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∈ A⊢ IsSidon (A ∪ {m}) ↔ m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c exact ⟨fun _ ↦ .inl h_mem, fun _ ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∈ Ax✝:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c⊢ IsSidon (A ∪ {m}) rwa [α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∈ Ax✝:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c⊢ IsSidon (Insert.insert m A) α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∈ Ax✝:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c⊢ IsSidon Aα:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∈ Ax✝:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c⊢ IsSidon A⟩
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + b⊢ Falseα:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + c⊢ Falseα:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c⊢ IsSidon (A ∪ {m})
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + b⊢ False exact h m (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + b⊢ m ∈ A ∪ {m} All goals completed! 🐙) a (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + b⊢ a ∈ A ∪ {m} All goals completed! 🐙) m (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + b⊢ m ∈ A ∪ {m} All goals completed! 🐙) b (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + b⊢ b ∈ A ∪ {m} All goals completed! 🐙) hc
|>.elim (fun _ ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + bx✝:m = a ∧ m = b⊢ False All goals completed! 🐙) (fun _ ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ahc:m + m = a + bx✝:m = b ∧ m = a⊢ False All goals completed! 🐙)
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + c⊢ False exact h m (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + c⊢ m ∈ A ∪ {m} All goals completed! 🐙) b (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + c⊢ b ∈ A ∪ {m} All goals completed! 🐙) a (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + c⊢ a ∈ A ∪ {m} All goals completed! 🐙) c (α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + c⊢ c ∈ A ∪ {m} All goals completed! 🐙) h_contr
|>.elim (fun _ ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + cx✝:m = b ∧ a = c⊢ False All goals completed! 🐙) (fun _ ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ah:IsSidon (A ∪ {m})a:αha:a ∈ Ab:αhb:b ∈ Ac:αhc:c ∈ Ah_contr:m + a = b + cx✝:m = c ∧ a = b⊢ False All goals completed! 🐙)
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + c⊢ IsSidon (A ∪ {m}) α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ A ∪ {m}⊢ ∀ j₁ ∈ A ∪ {m}, ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ A⊢ ∀ j₁ ∈ A ∪ {m}, ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ {m}⊢ ∀ j₁ ∈ A ∪ {m}, ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ A⊢ ∀ j₁ ∈ A ∪ {m}, ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ A ∪ {m}⊢ ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ A⊢ ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ {m}⊢ ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ A⊢ ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ A ∪ {m}⊢ ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ A⊢ ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ {m}⊢ ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ A⊢ ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ Aj₂:αhj₂:j₂ ∈ A ∪ {m}⊢ i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ Aj₂:αhj₂:j₂ ∈ A⊢ i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ Aj₂:αhj₂:j₂ ∈ {m}⊢ i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ Aj₂:αhj₂:j₂ ∈ A⊢ i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ All goals completed! 🐙
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ Aj₂:αhj₂:j₂ ∈ {m}⊢ i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αi₂:αj₂:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ ∈ Ahi₂:i₂ ∈ Ahj₂:j₂ = m⊢ i₁ + i₂ = j₁ + m → i₁ = j₁ ∧ i₂ = m ∨ i₁ = m ∧ i₂ = j₁
exact fun h ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αi₂:αj₂:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ ∈ Ahi₂:i₂ ∈ Ahj₂:j₂ = mh:i₁ + i₂ = j₁ + m⊢ i₁ = j₁ ∧ i₂ = m ∨ i₁ = m ∧ i₂ = j₁ All goals completed! 🐙
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ Ai₂:αhi₂:i₂ ∈ {m}⊢ ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αi₂:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ ∈ Ahi₂:i₂ = m⊢ ∀ a ∈ A, i₁ + m = j₁ + a → i₁ = j₁ ∧ m = a ∨ i₁ = a ∧ m = j₁
exact fun a ha h ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αi₂:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ ∈ Ahi₂:i₂ = ma:αha:a ∈ Ah:i₁ + m = j₁ + a⊢ i₁ = j₁ ∧ m = a ∨ i₁ = a ∧ m = j₁ All goals completed! 🐙
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ Aj₁:αhj₁:j₁ ∈ {m}⊢ ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ = m⊢ (∀ a ∈ A, i₁ + m = m + a → i₁ = m ∧ m = a ∨ i₁ = a) ∧
∀ a ∈ A, (i₁ + a = m + m → i₁ = m ∧ a = m) ∧ ∀ a_2 ∈ A, i₁ + a = m + a_2 → i₁ = m ∧ a = a_2 ∨ i₁ = a_2 ∧ a = m
refine ⟨fun b hb h ↦ .inr <| α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ = mb:αhb:b ∈ Ah:i₁ + m = m + b⊢ i₁ = b All goals completed! 🐙, fun b hb ↦ ⟨fun h ↦ ?_, ?_⟩⟩
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ = mb:αhb:b ∈ Ah:i₁ + b = m + m⊢ i₁ = m ∧ b = m All goals completed! 🐙
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ = mb:αhb:b ∈ A⊢ ∀ a ∈ A, i₁ + b = m + a → i₁ = m ∧ b = a ∨ i₁ = a ∧ b = m exact fun c hc h ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αj₁:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ ∈ Ahj₁:j₁ = mb:αhb:b ∈ Ac:αhc:c ∈ Ah:i₁ + b = m + c⊢ i₁ = m ∧ b = c ∨ i₁ = c ∧ b = m All goals completed! 🐙
α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ahm:m ∈ A ∨ ∀ a ∈ A, ∀ b ∈ A, m + m ≠ a + b ∧ ∀ c ∈ A, m + a ≠ b + ci₁:αhi₁:i₁ ∈ {m}⊢ ∀ j₁ ∈ A ∪ {m}, ∀ i₂ ∈ A ∪ {m}, ∀ j₂ ∈ A ∪ {m}, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ = m⊢ ∀ a ∈ A, ∀ a_2 ∈ A, m + a_2 = a + m → m = a ∧ a_2 = m ∨ a_2 = a
exact fun _ _ _ _ _ ↦ α:Type u_1inst✝²:AddCommMonoid αA:Set αm:αinst✝¹:IsRightCancelAdd αinst✝:IsLeftCancelAdd αhA:IsSidon Ah_mem:m ∉ Ai₁:αhm:∀ a ∈ A, ∀ b ∈ A, ¬m + m = a + b ∧ ∀ c ∈ A, ¬m + a = b + chi₁:i₁ = mx✝⁴:αx✝³:x✝⁴ ∈ Ax✝²:αx✝¹:x✝² ∈ Ax✝:m + x✝² = x✝⁴ + m⊢ m = x✝⁴ ∧ x✝² = m ∨ x✝² = x✝⁴ All goals completed! 🐙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.
IsMaximalSidonSetIn A N means A ⊆ {1, …, N} is Sidon and cannot be extended within
{1, …, N} while remaining Sidon.
def IsMaximalSidonSetIn (A : Set ℕ) (N : ℕ) : Prop :=
A ⊆ Set.Icc 1 N ∧ IsSidon A ∧
∀ ⦃x : ℕ⦄, x ∈ Set.Icc 1 N → x ∉ A → ¬ IsSidon (A ∪ {x})namespace IsMaximalSidonSetIn
If A is a maximal Sidon set in {1, …, N}, then A ⊆ {1, …, N}.
theorem subset {A : Set ℕ} {N : ℕ} (hA : IsMaximalSidonSetIn A N) :
A ⊆ Set.Icc 1 N := hA.1
If A is a maximal Sidon set in {1, …, N}, then A is Sidon.
theorem isSidon {A : Set ℕ} {N : ℕ} (hA : IsMaximalSidonSetIn A N) : IsSidon A := hA.2.1Maximality condition unpacked.
theorem maximal {A : Set ℕ} {N : ℕ} (hA : IsMaximalSidonSetIn A N) {x : ℕ}
(hx : x ∈ Set.Icc 1 N) (hxA : x ∉ A) : ¬ IsSidon (A ∪ {x}) := hA.2.2 hx hxAend IsMaximalSidonSetInend Setnamespace Finsetinstance (A : Finset α) [DecidableEq α] : Decidable (IsSidon (A : Set α)) := α:Type u_1inst✝¹:AddCommMonoid αA:Finset αinst✝:DecidableEq α⊢ Decidable (IsSidon ↑A)
α:Type u_1inst✝¹:AddCommMonoid αA:Finset αinst✝:DecidableEq α⊢ (∀ i₁ ∈ A, ∀ j₁ ∈ A, ∀ i₂ ∈ A, ∀ j₂ ∈ A, i₁ + i₂ = j₁ + j₂ → i₁ = j₁ ∧ i₂ = j₂ ∨ i₁ = j₂ ∧ i₂ = j₁) ↔ IsSidon ↑A
All goals completed! 🐙
The maximum size of a Sidon set in the supplied Finset.
def maxSidonSubsetCard (A : Finset α) [DecidableEq α] : ℕ :=
(A.powerset.filter fun B : Finset α ↦ IsSidon (B : Set α)).sup Finset.card
If A is finite Sidon, then A ∪ {s} is also Sidon provided s ≥ A.max + 1.
A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:2 * A.max' h + 1 ≤ sh₁:∀ {a b c : ℕ}, a ∈ A → b ∈ A → c ∈ A → a + b < 2 * A.max' h + 1 + cthis:s ∉ A⊢ IsSidon (↑A ∪ {s})
exact (IsSidon.insert hA).2 <| A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:2 * A.max' h + 1 ≤ sh₁:∀ {a b c : ℕ}, a ∈ A → b ∈ A → c ∈ A → a + b < 2 * A.max' h + 1 + cthis:s ∉ A⊢ s ∈ ↑A ∨ ∀ a ∈ ↑A, ∀ b ∈ ↑A, s + s ≠ a + b ∧ ∀ c ∈ ↑A, s + a ≠ b + c simpa [this] using fun a ha b hb ↦
⟨A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:2 * A.max' h + 1 ≤ sh₁:∀ {a b c : ℕ}, a ∈ A → b ∈ A → c ∈ A → a + b < 2 * A.max' h + 1 + cthis:s ∉ Aa:ℕha:a ∈ Ab:ℕhb:b ∈ A⊢ ¬s + s = a + b All goals completed! 🐙, fun c hc ↦ A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:2 * A.max' h + 1 ≤ sh₁:∀ {a b c : ℕ}, a ∈ A → b ∈ A → c ∈ A → a + b < 2 * A.max' h + 1 + cthis:s ∉ Aa:ℕha:a ∈ Ab:ℕhb:b ∈ Ac:ℕhc:c ∈ A⊢ ¬s + a = b + c All goals completed! 🐙⟩theorem IsSidon.exists_insert {A : Finset ℕ} (h : A.Nonempty) (hA : IsSidon (A : Set ℕ)) :
∃ m ∉ A, IsSidon (A ∪ {m}) := A:Finset ℕh:A.NonemptyhA:IsSidon ↑A⊢ ∃ m ∉ A, IsSidon (↑A ∪ {m})
A:Finset ℕh:A.NonemptyhA:IsSidon ↑A⊢ 2 * A.max' h + 1 ∉ A
exact mt (A.le_max' _) <| not_le.2 <| Finset.max'_lt_iff _ ‹_› |>.2 fun a ha ↦ A:Finset ℕh:A.NonemptyhA:IsSidon ↑Aa:ℕha:a ∈ A⊢ a < 2 * A.max' h + 1
All goals completed! 🐙theorem IsSidon.exists_insert_ge {A : Finset ℕ} (h : A.Nonempty) (hA : IsSidon (A : Set ℕ)) (s : ℕ) :
∃ m ≥ s, m ∉ A ∧ IsSidon (A ∪ {m}) := A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕ⊢ ∃ m ≥ s, m ∉ A ∧ IsSidon (↑A ∪ {m})
A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕ⊢ (if s ≥ 2 * A.max' h + 1 then s else 2 * A.max' h + 1) ≥ sA:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕ⊢ (if s ≥ 2 * A.max' h + 1 then s else 2 * A.max' h + 1) ∉ AA:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕ⊢ IsSidon (↑A ∪ {if s ≥ 2 * A.max' h + 1 then s else 2 * A.max' h + 1})
A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕ⊢ (if s ≥ 2 * A.max' h + 1 then s else 2 * A.max' h + 1) ≥ s A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:s ≥ 2 * A.max' h + 1⊢ s ≥ sA:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:¬s ≥ 2 * A.max' h + 1⊢ 2 * A.max' h + 1 ≥ s A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:s ≥ 2 * A.max' h + 1⊢ s ≥ sA:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:¬s ≥ 2 * A.max' h + 1⊢ 2 * A.max' h + 1 ≥ s All goals completed! 🐙
A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕ⊢ (if s ≥ 2 * A.max' h + 1 then s else 2 * A.max' h + 1) ∉ A A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:s ≥ 2 * A.max' h + 1⊢ s ∉ AA:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:¬s ≥ 2 * A.max' h + 1⊢ 2 * A.max' h + 1 ∉ A A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:s ≥ 2 * A.max' h + 1⊢ s ∉ AA:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:¬s ≥ 2 * A.max' h + 1⊢ 2 * A.max' h + 1 ∉ A
exact mt (A.le_max' _) <| not_le.2 <| Finset.max'_lt_iff _ ‹_› |>.2 fun a ha ↦ A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕh✝:¬s ≥ 2 * A.max' h + 1a:ℕha:a ∈ A⊢ a < 2 * A.max' h + 1
All goals completed! 🐙
A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕ⊢ IsSidon (↑A ∪ {if s ≥ 2 * A.max' h + 1 then s else 2 * A.max' h + 1}) A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:s ≥ 2 * A.max' h + 1⊢ IsSidon (↑A ∪ {s})A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:¬s ≥ 2 * A.max' h + 1⊢ IsSidon (↑A ∪ {2 * A.max' h + 1})
A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:s ≥ 2 * A.max' h + 1⊢ IsSidon (↑A ∪ {s}) All goals completed! 🐙
A:Finset ℕh:A.NonemptyhA:IsSidon ↑As:ℕhs:¬s ≥ 2 * A.max' h + 1⊢ IsSidon (↑A ∪ {2 * A.max' h + 1}) All goals completed! 🐙
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.
def greedySidon.go (A : Finset ℕ) (hA : IsSidon (A : Set ℕ)) (m : ℕ) :
{m' : ℕ // m' ≥ m ∧ m' ∉ A ∧ IsSidon (↑(A ∪ {m'}) : Set ℕ)} :=
if h : A.Nonempty then
have : ∃ m', m' ≥ m ∧ m' ∉ A ∧ IsSidon (↑(A ∪ {m'}) : Set ℕ) := α:Type u_1inst✝:AddCommMonoid αA:Finset ℕhA:IsSidon ↑Am:ℕh:A.Nonempty⊢ ∃ m' ≥ m, m' ∉ A ∧ IsSidon ↑(A ∪ {m'})
All goals completed! 🐙
⟨Nat.find this, Nat.find_spec this⟩
else ⟨m, α:Type u_1inst✝:AddCommMonoid αA:Finset ℕhA:IsSidon ↑Am:ℕh:¬A.Nonempty⊢ m ≥ m ∧ m ∉ A ∧ IsSidon ↑(A ∪ {m}) All goals completed! 🐙⟩
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.
def greedySidon.aux (n : ℕ) : ({A : Finset ℕ // IsSidon (A : Set ℕ)} × ℕ) :=
match n with
| 0 => (⟨{1}, α:Type u_1inst✝:AddCommMonoid αn:ℕ⊢ IsSidon ↑{1} All goals completed! 🐙⟩, 1)
| k + 1 =>
let (A, s) := greedySidon.aux k
let s := if h : A.1.Nonempty then A.1.max' h + 1 else s
let s' := greedySidon.go A.1 A.2 s
(⟨A.1 ∪ {s'.1}, s'.2.2.2⟩, s'.1)
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, ....
def greedySidon (n : ℕ) : ℕ := greedySidon.aux n |>.2
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.
def greedySidonBelow (N : ℕ) : Finset ℕ :=
(greedySidon.aux N).1.1.filter (· ≤ N)end Finset