Erdős Problem 402

Reference: erdosproblems.com/402

theorem erdos_402 (A : Finset ℕ) (h₁ : 0 ∉ A) (h₂ : A.Nonempty) : ∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) ≤ ↑a / ↑A.card

Prove that, for any finite set $A\subset\mathbb{N}$, there exist $a, b\in A$ such that $$ \gcd(a, b)\leq a/|A|. $$

theorem erdos_402.variants.equality (A : Finset ℕ) (h₁ : 0 ∉ A) (h₂ : A.Nonempty) (hA : ∀ (n : ℕ), A ≠ Finset.Icc 1 n ∧ A ≠ Finset.image (fun (i : ℕ) => (Finset.Icc 1 n).lcm id / i) (Finset.Icc 1 n) ∧ A ≠ {2, 3, 4, 6}) : ∃ a ∈ A, ∃ b ∈ A, ↑(a.gcd b) < ↑a / ↑A.card

A conjecture of Graham [Gr70], who also conjectured that (assuming $A$ itself has no common divisor) the only cases where equality is achieved are when $A = \{1, ..., n\}$ or $\{L/1, ..., L/n\}$ (where $L = \operatorname{lcm}(1, ..., n)$) or $\{2, 3, 4, 6\}$. Note: The source [BaSo96] mentioned on the Erdős page makes it clear what quantfiers to use for "where equality is achieved". See Theorem 1.1 there.

TODO(firsching): Consider if we should have the other direction here as well or an iff statement.

theorem erdos_402.variants.szegedy_zaharescu_weak : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (A : Finset ℕ), A.card = n → 0 ∉ A → (n ≤ (A ×ˢ A).sup fun (x : ℕ × ℕ) => x.1 / x.1.gcd x.2) ∧ ((n = (A ×ˢ A).sup fun (x : ℕ × ℕ) => x.1 / x.1.gcd x.2) ↔ ∃ k > 0, A = Finset.image (fun (x : ℕ) => k * x) (Finset.Icc 1 n) ∨ A = Finset.image (fun (x : ℕ) => k * (Finset.Icc 1 n).lcm id / x) (Finset.Icc 1 n))

Proved for all sufficiently large sets (including the sharper version which characterises the case of equality) independently by Szegedy [Sz86] and Zaharescu [Za87]. The following is taken from [Sz86].

There exists an effectively computable $n_0$ with the following properties: (i) if $n\geq n_0$ and $a_1, a_2, ..., a_n$ are distinct natural numbers then $\max_{i, j} \frac{a_i}{(a_i, a_j)} \geq n$. (ii) If equality holds then the system $\{a_1, a_2, ..., a_n\}$ is either of the type $\{k, 2k, ..., nk\}$ or of the type $\left\{\frac{k}{1}, \frac{k}{2}, ..., \frac{k}{n}\right\}$