Erdős problem 402
Prove that, for any finite set , there exist such that
Sources
FormalConjectures/ErdosProblems/
402.lean
Retained formal statement
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 with the following properties: (i) if and are distinct natural numbers then . (ii) If equality holds then the system is either of the type or of the type .
∀ᶠ (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))SolvedStatement only, no proof