The Marica-Schönheim special case of Graham's conjecture

Graham's conjecture states that if $0<a_1<\dots a_n$ are integers, then $\underset{i,j}{max}\frac{a_i}{gcd(a_i,a_j)}\ge n$. This file proves the conjecture when the $a_i$ are squarefree as a corollary of the Marica-Schönheim inequality.

References

[Applications of the FKG Inequality and Its Relatives, Graham][Graham1983]

def Nat.GrahamConjecture (n : ℕ) (f : ℕ → ℕ) : Prop

Statement of Graham's conjecture (which is now a theorem in the literature).

Graham's conjecture states that if $0<a_1<\dots a_n$ are integers, then $\underset{i,j}{max}\frac{a_i}{gcd(a_i,a_j)}\ge n$.

Equations

• n.GrahamConjecture f = (n ≠ 0 → StrictMonoOn f (Set.Iio n) → ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i)

theorem Nat.grahamConjecture_of_squarefree {n : ℕ} (f : ℕ → ℕ) (hf' : ∀ k < n, Squarefree (f k)) : n.GrahamConjecture f

The special case of Graham's conjecture where all numbers are squarefree.