Documentation

Mathlib.NumberTheory.MaricaSchoenheim

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 : ) :

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
Instances For
    theorem Nat.grahamConjecture_of_squarefree {n : } (f : ) (hf' : k < n, Squarefree (f k)) :

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