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 $\max_{i, j} \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 $\max_{i, j} \frac{a_i}{\gcd(a_i, a_j)} \ge n$.

Equations

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

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

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