Erdős Problem 535

References:

• erdosproblems.com/535
• [Er64] P. Erdős, On a problem in elementary number theory and a combinatorial problem. Math. Comp. (1964), 644–646.
• [AbHa70] H. L. Abbott and D. Hanson, An extremal problem in number theory. Bull. London Math. Soc. (1970), 324–326.
• [Er73] P. Erdős, Problems and results on combinatorial number theory, in A Survey of Combinatorial Theory, North-Holland, 1973.

def Erdos535.NoConstantPairwiseGcdCoprimeSubsets (r : ℕ) (A : Finset ℕ) : Prop

No r-subset has constant pairwise GCD with coprime quotients.

Equations

• Erdos535.NoConstantPairwiseGcdCoprimeSubsets r A = ∀ S ⊆ A, S.card = r → ¬∃ (d : ℕ), 0 < d ∧ ((↑S).Pairwise fun (a b : ℕ) => a.gcd b = d) ∧ ∀ a ∈ S, ∃ (b : ℕ), a = d * b ∧ b.gcd d = 1

def Erdos535.AllBigOmega (k : ℕ) (A : Finset ℕ) : Prop

All elements of A are positive and have exactly k prime factors, counted with multiplicity.

Erdős [Er73] explains that Abbott pointed out the ordinary sunflower conjecture does not seem to suffice for Problem 535; the corrected stronger auxiliary statement uses $Ω$, not $ω$.

Equations

• Erdos535.AllBigOmega k A = ∀ a ∈ A, 1 ≤ a ∧ ArithmeticFunction.cardFactors a = k

noncomputable def Erdos535.f (r N : ℕ) : ℕ

f r N is the maximum size of a subset A ⊆ {1,…,N} such that no r-element subset of A has constant pairwise GCD.

Equations

• Erdos535.f r N = sSup {k : ℕ | ∃ A ⊆ Finset.Icc 1 N, (∀ S ⊆ A, S.card = r → ¬∃ (d : ℕ), (↑S).Pairwise fun (a b : ℕ) => a.gcd b = d) ∧ A.card = k}

theorem Erdos535.erdos_535 (r : ℕ) : r ≥ 3 → ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(f r N) ≤ ↑N ^ (c / Real.log (Real.log ↑N))

Let $r \geq 3$, and let $f_r(N)$ denote the size of the largest subset of $\{1,\ldots,N\}$ such that no subset of size $r$ has the same pairwise greatest common divisor between all elements. Erdős [Er64] proved that $f_3(N) > N^{c/\log\log N}$ for some constant $c > 0$, and conjectured this should also be an upper bound; here we state the conjectural upper bound for all $r \geq 3$.

See also [536].

theorem Erdos535.erdos_535.variants.first_open_case : ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑(f 3 N) ≤ ↑N ^ (c / Real.log (Real.log ↑N))

The first open case of Erdős Problem 535 is $r = 3$: there should exist $c > 0$ such that $f_3(N) \leq N^{c/\log\log N}$ for all sufficiently large $N$.

theorem Erdos535.erdos_535.variants.erdos_upper_bound {r : ℕ} (hr : 3 ≤ r) (ε : ℝ) : ε > 0 → ∀ᶠ (N : ℕ) in Filter.atTop, ↑(f r N) ≤ ↑N ^ (3 / 4 + ε)

Erdős [Er64] proved that $f_r(N) \leq N^{3/4+o(1)}$ for all $r \geq 3$.

theorem Erdos535.erdos_535.variants.lower_bound : ∃ c > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ↑N ^ (c / Real.log (Real.log ↑N)) ≤ ↑(f 3 N)

Erdős [Er64] proved that $f_3(N) > N^{c/\log\log N}$ for some constant $c > 0$.

theorem Erdos535.erdos_535.variants.abbott_hanson {r : ℕ} (hr : 3 ≤ r) (ε : ℝ) : ε > 0 → ∀ᶠ (N : ℕ) in Filter.atTop, ↑(f r N) ≤ ↑N ^ (1 / 2 + ε)

Abbott and Hanson [AbHa70] improved Erdős's upper bound to $f_r(N) \leq N^{1/2+o(1)}$ for all $r \geq 3$.

theorem Erdos535.erdos_535.variants.sunflower_strong {r : ℕ} (hr : 3 ≤ r) : ∃ c_r > 0, ∀ (k : ℕ) (A : Finset ℕ), AllBigOmega k A → NoConstantPairwiseGcdCoprimeSubsets r A → ↑A.card ≤ c_r ^ k

Erdős [Er73] records that Abbott pointed out the ordinary sunflower conjecture does not seem to suffice here. The stronger auxiliary conjecture uses $Ω(n)=k$, i.e. prime factors counted with multiplicity; this stronger statement would imply the conjectured upper bound for $f_r(N)$.

theorem Erdos535.erdos_535.variants.sunflower_erdos_rado {r : ℕ} (hr : 3 ≤ r) : ∃ c_r > 0, ∀ (k : ℕ) (A : Finset ℕ), AllBigOmega k A → NoConstantPairwiseGcdCoprimeSubsets r A → ↑A.card ≤ c_r ^ k * ↑k.factorial

For the stronger $Ω(n)=k$ variant above, the Erdős–Rado method gives the weaker bound $c_r^k \cdot k!$; see Erdős [Er73].