Documentation

LeanPool.Erdos865.Sharpness

Sharpness of the 5/8 bound (Erdős 865, §5) #

The construction A = [M,2M] ∪ [4M,8M] is triple-free of size 5M + 2, so for N = 8M one has 8·|A| = 5·N + 16, showing the constant 5/8 is optimal.

source
def Erdos865.sharpSet (M : ℕ) :
Finset ℕ

The sharpness construction A = [M, 2M] ∪ [4M, 8M].

Equations
Instances For
    source
    theorem Erdos865.sharpSet_subset {M : ℕ} (hM : 1 ≤ M) :
    sharpSet M ⊆ Finset.Icc 1 (8 * M)

    The construction sits inside [1, 8M] (for M ≥ 1).

    source
    theorem Erdos865.sharpSet_card {M : ℕ} (hM : 1 ≤ M) :
    (sharpSet M).card = 5 * M + 2

    The construction has 5M + 2 elements.

    source
    theorem Erdos865.sharpSet_tripleFree (M : ℕ) :
    IsTripleFree (sharpSet M)

    The construction is triple-free.

    source
    theorem Erdos865.sharpness {M : ℕ} (hM : 1 ≤ M) :
    ∃ A ⊆ Finset.Icc 1 (8 * M), IsTripleFree A ∧ 8 * A.card = 5 * (8 * M) + 16

    Sharpness: for N = 8M with M ≥ 1 there is a triple-free subset of [1,N] of size 5M + 2, i.e. with 8 * card = 5 * N + 16.