FormalConjectures/ErdosProblems/154.lean
Explanation legend Lean4 Domain Explanation Language (L4DEL)
L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.
- L4DEL
- Lean4 Domain Explanation Language
Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.
Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1
2 declarations, 2 contain sorry, 0 declared as axioms
Erdős Problem 154
References:
- erdosproblems.com/154
- [Li98] Lindström, Bernt, Well distribution of Sidon sets in residue classes. J. Number Theory (1998), 197-200.
- [Ko99] Kolountzakis, Mihail N., On the uniform distribution in residue classes of dense sets of integers with distinct sums. J. Number Theory (1999), 147-153.
- [ESS94] Erdős, P. and Sárközy, A. and Sós, T., On Sum Sets of Sidon Sets, I. Journal of Number Theory (1994), 329-347.
Imports (1)
- theorem
Erdos154.erdos_154sorry line 57 sourcedepends on sorry what this means
Statement uses:
Iff,True,Nat,LE.le,OfNat.ofNat,Finset,Filter.Tendsto,Real,Filter.atTop,Membership.mem, IsSidon,HDiv.hDiv,Finset.card,Real.sqrt,nhds,LT.lt,Finset.filter,Eq,HMod.hMod,HAdd.hAddProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous50 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
- theorem
Erdos154.erdos_154.variants.lindstromDocumented declaration: lindstrom sorry line 78 sourceSource documentation
Lindström's result for $A$ itself [Li98], later strengthened by Kolountzakis [Ko99]: for any sequence of Sidon sets $A_k\subseteq\{0,\ldots,N_k\}$ with $N_k\to\infty$ and $\lvert A_k\rvert\sim N_k^{1/2}$, and any modulus $m\geq 2$, the number of elements of $A_k$ congruent to $i\pmod m$, divided by $N_k^{1/2}$, tends to $1/m$ for every residue $i<m$.
Well-distribution of $A+A$ (the actual question,
erdos_154) follows from this using the Sidon property.depends on sorry what this means
Statement uses:
Nat,LE.le,OfNat.ofNat,Finset,Filter.Tendsto,Real,Filter.atTop,Membership.mem, IsSidon,HDiv.hDiv,Finset.card,Real.sqrt,nhds,LT.lt,Finset.filter,Eq,HMod.hModProof uses:
sorryAx,Lean.Name,Bool.false,Lean.Name.num,Lean.Name.str,Lean.Name.anonymous44 instances, coercions and auxiliary constants left out.
Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem erdos_154.variants.lindstrom : ∀ (m : ℕ) (hm : 2 ≤ m) (N : ℕ → ℕ) (A : ℕ → Finset ℕ), Tendsto (fun k => (N k : ℝ)) atTop atTop → (∀ k, ∀ x ∈ A k, x ≤ N k) → (∀ k, IsSidon (A k : Set ℕ)) → Tendsto (fun k => ((A k).card : ℝ) / Real.sqrt (N k)) atTop (nhds 1) → ∀ i < m, Tendsto (fun k => (((A k).filter (fun a => a % m = i)).card : ℝ) / Real.sqrt (N k)) atTop (nhds (1 / m)) := by …Mentions: IsSidon