FormalConjectures/ErdosProblems/331.lean

GitHub source file

2 declarations, 2 contain sorry, 0 declared as axioms

1. theorem Erdos331.erdos_331 Documented declaration: erdos_331 sorry line 51 source

   Source documentation

   Let $A,B\subseteq \mathbb{N}$ such that for all large $N$$$\lvert A\cap \{1,\ldots,N\}\rvert \gg N^{1/2}$$and$$\lvert B\cap \{1,\ldots,N\}\rvert \gg N^{1/2}.$$ Is it true that there are infinitely many solutions to $a_1-a_2=b_1-b_2\neq 0$ with $a_1,a_2\in A$ and $b_1,b_2\in B$?

   Ruzsa has observed that there is a simple counterexample: take $A$ to be the set of numbers whose binary representation has only non-zero digits in even places, and $B$ similarly but with non-zero digits only in odd places. It is easy to see $A$ and $B$ both grow like $\gg N^{1/2}$ and yet for any $n\geq 1$ there is exactly one solution to $n=a+b$ with $a\in A$ and $b\in B$.

   This was formalized in Lean by van Doorn using Aristotle.

   depends on sorry what this means

   Statement uses: Iff, False, Set, Nat, Asymptotics.IsBigO, Real, Filter.atTop, HPow.hPow, HDiv.hDiv, OfNat.ofNat, Nat.count, Membership.mem, Classical.propDecidable, Set.Infinite, Prod, Set.ofPred, Erdos331.erdos_331.match_1, And, Ne, Eq and 1 more

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

   36 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_331 :
       answer(False) ↔
         ∀ A B : Set ℕ,
         (fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count (· ∈ A) n : ℝ)) →
         (fun (n : ℕ) ↦ (n : ℝ) ^ (1 / 2 : ℝ)) =O[atTop] (fun (n : ℕ) ↦ (count (· ∈ B) n : ℝ)) →
         { s : ℕ × ℕ × ℕ × ℕ | let ⟨a₁, a₂, b₁, b₂⟩ := s
   …

2. theorem Erdos331.erdos_331.variants.ruzsa Documented declaration: ruzsa sorry line 75 source

   Source documentation

   Ruzsa suggests that a non-trivial variant of this problem arises if one imposes the stronger condition that $|A \cap \{1,\dots,N\}| \sim c_A N^{1/2}$ for some constant $c_A>0$, and similarly for $B$.

   The answer is yes. Write $A(N) = |A \cap \{1,\dots,N\}|$ and $B(N) = |B \cap \{1,\dots,N\}|$. Erdős and Freud [ErFr84, Theorem 4] proved that if $a_1 - a_2 = b_1 - b_2$ has only trivial solutions and $\liminf_N \min(A(N), B(N)) / N^{1/2} > 0$, then neither $A(N) / N^{1/2}$ nor $B(N) / N^{1/2}$ tends to a limit. If there were only finitely many non-trivial solutions, removing the finitely many elements of $A$ that occur in them would give sets with the same asymptotics and no non-trivial solution.

   depends on sorry what this means

   Statement uses: Iff, True, Set, Nat, Exists, Real, And, GT.gt, OfNat.ofNat, Asymptotics.IsEquivalent, Filter.atTop, Nat.count, Membership.mem, Classical.propDecidable, HMul.hMul, HPow.hPow, HDiv.hDiv, Set.Infinite, Prod, Set.ofPred and 4 more

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

   54 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_331.variants.ruzsa :
       answer(True) ↔
         ∀ A B : Set ℕ,
         (∃ c_A > 0, (fun (n : ℕ) ↦ (count (· ∈ A) n : ℝ)) ~[atTop] (fun (n : ℕ) ↦ c_A * (n : ℝ) ^ (1 / 2 : ℝ))) →
         (∃ c_B > 0, (fun (n : ℕ) ↦ (count (· ∈ B) n : ℝ)) ~[atTop] (fun (n : ℕ) ↦ c_B * (n : ℝ) ^ (1 / 2 : ℝ))) →
         { s : ℕ × ℕ × ℕ × ℕ | let ⟨a₁, a₂, b₁, b₂⟩ := s
   …