Erdos 43

FormalConjectures/ErdosProblems/43.lean

@@ -0,0 +1,57 @@
+/-
+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.
+-/
+
+import FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 43
+
+*Reference:* [erdosproblems.com/43](https://www.erdosproblems.com/43)
+-/
+
+open scoped Pointwise
+
+
+/--
+If `A` and `B` are Sidon sets in `{1, ..., N}` with disjoint difference sets,
+is the sum of unordered pair counts bounded by that of an optimal Sidon set up to `O(1)`?
+-/
+@[category research open, AMS 11 05]
+theorem erdos_43 :
+    ∃ C : ℝ, ∀ (N : ℕ) (A B : Finset ℕ),
+      A ⊆ Finset.Icc 1 N →
+      B ⊆ Finset.Icc 1 N →
+      IsSidon A.toSet →
+      IsSidon B.toSet →
+      (A - A) ∩ (B - B) = ∅ →
+      A.card.choose 2 + B.card.choose 2 ≤ (maxSidonSetSize N).choose 2 + C := by
+  sorry
+
+/--
+If `A` and `B` are equal-sized Sidon sets with disjoint difference sets,
+can the sum of pair counts be bounded by a strict fraction of the optimum?
+-/
+@[category research open, AMS 11 05]
+theorem erdos_43_equal_size :
+    ∃ᵉ (c > 0), ∀ (N : ℕ) (A B : Finset ℕ),
+      A ⊆ Finset.Icc 1 N →
+      B ⊆ Finset.Icc 1 N →
+      IsSidon A.toSet →
+      IsSidon B.toSet →
+      A.card = B.card →
+      (A - A) ∩ (B - B) = ∅ →
+      A.card.choose 2 + B.card.choose 2 ≤ (1 - c) *(maxSidonSetSize N).choose 2 := by
+  sorry

FormalConjectures/ForMathlib/Combinatorics/Basic.lean

@@ -15,6 +15,8 @@ limitations under the License.
 -/
 
 import FormalConjectures.ForMathlib.Combinatorics.AP.Basic
+import Mathlib.Combinatorics.Enumerative.Bell
+import Mathlib.Combinatorics.SimpleGraph.Finite
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Nat.Lattice
 import Mathlib.Tactic.Linarith
@@ -23,17 +25,39 @@ open Function Set
 
 variable {α : Type*} [AddCommMonoid α]
 
-/-- 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. -/
+/-- A Sidon set is a set such that all pairwise sums of elements are distinct,
+apart from coincidences forced by commutativity. -/
 def IsSidon {S : Type*} [Membership α S] (A : S) : Prop := ∀ᵉ (i₁ ∈ A) (j₁ ∈ A) (i₂ ∈ A) (j₂ ∈ A),
   i₁ + i₂ = j₁ + j₂ → (i₁ = j₁ ∧ i₂ = j₂) ∨ (i₁ = j₂ ∧ i₂ = j₁)
 
 @[simp, push_cast]
 theorem coe {S : Type*} [SetLike S α] {A : S} : IsSidon (A : Set α) ↔ IsSidon A := by
   simp [IsSidon]
 
+open Classical
+
+/-- The subsets of `{0, ..., n - 1}` which are Sidon sets. -/
+noncomputable def SidonSubsets (n : ℕ) : Finset (Finset ℕ) :=
+  (Finset.range n).powerset.filter fun s => IsSidon (s : Set ℕ)
+
+/-- The sizes of Sidon subsets of `{0, ..., n - 1}`. -/
+noncomputable def SidonSubsetsSizes (n : ℕ) : Finset ℕ :=
+  (SidonSubsets n).image Finset.card
+
+lemma SidonSubsetsSizesNonempty (n : ℕ) : (SidonSubsetsSizes n).Nonempty := by
+  use 0
+  simp only [SidonSubsetsSizes, Finset.mem_image]
+  use ∅
+  simp [SidonSubsets, IsSidon, Set.Pairwise, Finset.mem_filter, Finset.mem_powerset, Finset.card_empty]
+
+/-- The maximum size of a Sidon set in `{1, ..., N}`. -/
+noncomputable def maxSidonSetSize (N : ℕ) : ℕ :=
+  sSup {(A.card) | (A : Finset ℕ) (_ : A ⊆ Finset.Icc 1 N) (_ : IsSidon A.toSet)}
+
+
 namespace Set
 
+
 lemma IsSidon.avoids_isAPOfLength_three {A : Set ℕ} (hA : IsSidon A)
     {Y : Set ℕ} (hY : Y.IsAPOfLength 3) :
     (A ∩ Y).ncard ≤ 2 := by