FormalConjectures/ErdosProblems/772.lean

GitHub source file

5 declarations, 4 contain sorry, 0 declared as axioms

1. def Erdos772.H $H_k(n)$ is the maximal $r$ such that if $A\subset\mathbb{N}$ has $\lvert A\rvert=n$ and $\| 1_A\ast 1_A\|_\infty \leq k$ then $A$ contains a Sidon set of size at least $r$ line 44 source

   Source documentation

   $H_k(n)$ is the maximal $r$ such that if $A\subset\mathbb{N}$ has $\lvert A\rvert=n$ and $\| 1_A\ast 1_A\|_\infty \leq k$ then $A$ contains a Sidon set of size at least $r$.

   Here $1_A\ast 1_A(m)$ counts the ordered pairs $(a,b)\in A^2$ with $a+b=m$. (The value is truncated at $n$, which only matters when no such $A$ exists.)

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Nat

   Proof uses: SupSet.sSup, Set.ofPred, And, LE.le, Finset, Eq, Finset.card, AdditiveCombinatorics.sumRep, Exists, IsSidon

   8 instances, coercions and auxiliary constants left out.

   noncomputable def H (k n : ℕ) : ℕ :=
   …

2. theorem Erdos772.erdos_772.parts.i sorry line 59 source

   depends on sorry what this means

   Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Filter.Tendsto, Real, HDiv.hDiv, Erdos772.H, Real.sqrt, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   18 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

3. theorem Erdos772.erdos_772.parts.ii sorry line 70 source

   depends on sorry what this means

   Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Exists, Real, And, GT.gt, Filter.Eventually, LT.lt, HPow.hPow, HAdd.hAdd, HDiv.hDiv, Erdos772.H, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   40 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

4. theorem Erdos772.erdos_772.variants.alon_erdos Alon and Erdős [AlEr85] proved that $H_k(n) \gg_k n^{2/3}$ sorry line 76 source

   Source documentation

   Alon and Erdős [AlEr85] proved that $H_k(n) \gg_k n^{2/3}$.

   depends on sorry what this means

   Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Real, And, GT.gt, Filter.Eventually, HMul.hMul, HPow.hPow, HDiv.hDiv, Erdos772.H, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   38 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_772.variants.alon_erdos (k : ℕ) (hk : 1 ≤ k) :
       ∃ c > 0, ∀ᶠ n : ℕ in atTop, c * (n : ℝ) ^ (2 / 3 : ℝ) ≤ H k n := by
   …

   Mentions: c, Erdos772.H

5. theorem Erdos772.erdos_772.variants.upper_bound Erdős [Er84d] proved that $H_k(n) \ll n^{2/3}$, where the implied constant is absolute sorry line 88 source

   Source documentation

   Erdős [Er84d] proved that $H_k(n) \ll n^{2/3}$, where the implied constant is absolute.

   Since $1_A\ast 1_A$ counts ordered pairs, the bound needs $k\geq 4$: the construction of Erdős has at most two unordered representations of each sum, hence at most four ordered ones, while $k\leq 2$ forces $A$ itself to be Sidon and so $H_k(n)=n$. For $k=3$ the only collisions are $a+b=2c$, so the Sidon subsets of $A$ are its $3$-term-progression-free subsets, which have size $n^{1-o(1)}$, and the bound fails there too.

   depends on sorry what this means

   Statement uses: Exists, Real, Nat, GE.ge, OfNat.ofNat, Filter.Eventually, LE.le, Erdos772.H, HMul.hMul, HPow.hPow, HDiv.hDiv, Filter.atTop

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   32 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_772.variants.upper_bound :
       ∃ C : ℝ, ∀ k ≥ 4, ∀ᶠ n : ℕ in atTop,
         (H k n : ℝ) ≤ C * (n : ℝ) ^ (2 / 3 : ℝ) := by
   …

   Mentions: Erdos772.H