The Marica-Schönheim special case of Graham's conjecture #
Graham's conjecture states that if
References #
[Applications of the FKG Inequality and Its Relatives, Graham][Graham1983]
Statement of Graham's conjecture (which is now a theorem in the literature).
Graham's conjecture states that if
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.