FormalConjectures/ErdosProblems/537.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

1. theorem Erdos537.erdos_537 Let $\epsilon>0$ and $N$ be sufficiently large sorry line 52 source

   Source documentation

   Let $\epsilon>0$ and $N$ be sufficiently large. If $A\subseteq \{1,\ldots,N\}$ has $\lvert A\rvert \geq \epsilon N$ then must there exist $a_1,a_2,a_3\in A$ and distinct primes $p_1,p_2,p_3$ such that $$a_1p_1=a_2p_2=a_3p_3?$$

   A positive answer would imply [536].

   Erdős describes a construction of Ruzsa which disproves this: consider the set of all squarefree numbers of the shape $p_1\cdots p_r$ where $p_{i+1}>2p_i$ for $1\leq i<r$. This set has positive density, and hence if $A$ is its intersection with $(N/2,N)$ then $\lvert A\rvert \gg N$ for all large $N$. Suppose now that $p_1a_1=p_2a_2=p_3a_3$ where $a_i\in A$ and $p_1,p_2,p_3$ are distinct primes. Without loss of generality we may assume that $a_2>a_3$ and hence $p_2<p_3$, and so since $p_2p_3\mid a_1\in A$ we must have $2<p_3/p_2$. On the other hand $p_3/p_2=a_2/a_3\in (1,2)$, a contradiction.

   L4DEL explanation

   Let $\epsilon>0$ and $N$ be sufficiently large. If $A\subseteq \{1,\ldots,N\}$ has $\lvert A\rvert \geq \epsilon N$ then must there exist $a_1,a_2,a_3\in A$ and distinct primes $p_1,p_2,p_3$ such that $$a_1p_1=a_2p_2=a_3p_3?$$ A positive answer would imply [536]. Erdős describes a construction of Ruzsa which disproves this: consider the set of all squarefree numbers of the shape $p_1\cdots p_r$ where $p_{i+1}>2p_i$ for $1\leq ia_3$ and hence $p_2<p_3$, and so since $p_2p_3\mid a_1\in A$ we must have $2<p_3/p_2$. On the other hand $p_3/p_2=a_2/a_3\in (1,2)$, a contradiction.

   Sources and attribution: Pinned Lean source (1646ca16afd6)

   depends on sorry what this means

   Statement uses: Iff, False, Real, LT.lt, OfNat.ofNat, Filter.Eventually, Nat, Finset, LE.le, Finset.Icc, GE.ge, Finset.card, HMul.hMul, Exists, And, Membership.mem, Nat.Prime, Ne, Eq, Filter.atTop

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

   34 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_537 : answer(False) ↔
       ∀ ε : ℝ, 0 < ε → ∀ᶠ N : ℕ in atTop,
         ∀ A ⊆ Finset.Icc 1 N, (A.card : ℝ) ≥ ε * N →
           ∃ a₁ ∈ A, ∃ a₂ ∈ A, ∃ a₃ ∈ A, ∃ p₁ p₂ p₃ : ℕ,
             p₁.Prime ∧ p₂.Prime ∧ p₃.Prime ∧
             p₁ ≠ p₂ ∧ p₁ ≠ p₃ ∧ p₂ ≠ p₃ ∧
             a₁ * p₁ = a₂ * p₂ ∧ a₂ * p₂ = a₃ * p₃ := by
   …