FormalConjectures/ErdosProblems/806.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
3 declarations, 3 contain sorry, 0 declared as axioms
Erdős Problem 806
References:
- erdosproblems.com/806
- [ErNe77] Erdős, P. and Newman, D. J., Bases for sets of integers. J. Number Theory (1977), 420-425.
- [ABS09] Alon, Noga and Bukh, Boris and Sudakov, Benny, Discrete Kakeya-type problems and small bases. Israel J. Math. (2009), 285-301.
Imports (1)
- theorem
Erdos806.erdos_806sorry line 54 sourcedepends on sorry what this means
Statement uses:
Iff,True,Real,LT.lt,OfNat.ofNat,Filter.Eventually,Nat,Finset,LE.le,Finset.Icc,Finset.card,Real.sqrt,Exists,Int,And,Finset.map,Nat.castEmbedding,HAdd.hAdd,HMul.hMul,Filter.atTopProof 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
Erdos806.erdos_806.variants.alon_bukh_sudakovDocumented declaration: alon_bukh_sudakov sorry line 65 sourceSource documentation
Alon, Bukh, and Sudakov [ABS09] proved that for any $A\subseteq \{1,\ldots,n\}$ with $\lvert A\rvert \leq n^{1/2}$ there exists some $B$ such that $A\subseteq B+B$ and $\lvert B\rvert \ll \frac{\log\log n}{\log n}n^{1/2}$.
depends on sorry what this means
Statement uses:
Exists,Real,Filter.Eventually,Nat,Finset,LE.le,Finset.Icc,OfNat.ofNat,Finset.card,Real.sqrt,Int,And,Finset.map,Nat.castEmbedding,HAdd.hAdd,HMul.hMul,HDiv.hDiv,Real.log,Filter.atTopProof 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_806.variants.alon_bukh_sudakov : ∃ C : ℝ, ∀ᶠ n : ℕ in atTop, ∀ A : Finset ℕ, A ⊆ Finset.Icc 1 n → (A.card : ℝ) ≤ √n → ∃ B : Finset ℤ, A.map Nat.castEmbedding ⊆ B + B ∧ (B.card : ℝ) ≤ C * Real.log (Real.log n) / Real.log n * √n := by … - theorem
Erdos806.erdos_806.variants.erdos_newmanErdős and Newman [ErNe77] proved that there exist sorry line 77 sourceSource documentation
Erdős and Newman [ErNe77] proved that there exist $A\subseteq\{1,\ldots,n\}$ with $\lvert A\rvert\asymp n^{1/2}$ such that if $A\subseteq B+B$ then $\lvert B\rvert \gg \frac{\log\log n}{\log n}n^{1/2}$.
depends on sorry what this means
Statement uses:
Exists,Real,And,LT.lt,OfNat.ofNat,Filter.Eventually,Nat,Finset,LE.le,Finset.Icc,HMul.hMul,Real.sqrt,Finset.card,Int,Finset.map,Nat.castEmbedding,HAdd.hAdd,HDiv.hDiv,Real.log,Filter.atTopProof 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 erdos_806.variants.erdos_newman : ∃ c : ℝ, 0 < c ∧ ∀ᶠ n : ℕ in atTop, ∃ A : Finset ℕ, A ⊆ Finset.Icc 1 n ∧ c * √n ≤ A.card ∧ (A.card : ℝ) ≤ √n ∧ ∀ B : Finset ℤ, A.map Nat.castEmbedding ⊆ B + B → c * Real.log (Real.log n) / Real.log n * √n ≤ B.card := by …Mentions: c