Documentation

FormalConjectures.ErdosProblems.«835»

Erdős Problem 835 #

References:

source
def Erdos835.Property (k : ℕ) :
Prop

The property that for a given $k$, the $k$-subsets of a $2k$-set can be colored with $k+1$ colors such that any $(k+1)$-subset contains all colors.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Erdos835.erdos_835 :
    (∃ k > 2, Property k) ↔ sorry

    Does there exist a $k>2$ such that the $k$-sized subsets of {1,...,2k} can be coloured with $k+1$ colours such that for every $A\subset \{1,\ldots,2k\}$ with $\lvert A\rvert=k+1$ all $k+1$ colours appear among the $k$-sized subsets of $A$?

    source
    theorem Erdos835.property_iff_chromaticNumber (k : ℕ) (hk : 0 < k) :
    (SimpleGraph.johnson (2 * k) k).chromaticNumber = ↑k + 1 ↔ Property k
    source
    theorem Erdos835.erdos_835.variants.johnson :
    (∃ (l : ℕ), (SimpleGraph.johnson (2 * (l + 3)) (l + 3)).chromaticNumber = ↑(l + 3) + 1) ↔ sorry

    Alternative statement of Erdős Problem 835 using the chromatic number of the Johnson graph. This is equivalent to asking whether there exists $k > 2$ such that the chromatic number of the Johnson graph $J(2k, k)$ is $k+1$.

    source
    theorem Erdos835.johnsonGraph_2k_k_chromaticNumber_known_cases (k : ℕ) (hk : 3 ≤ k) (hk' : k ≤ 8) :
    (SimpleGraph.johnson (2 * k) k).chromaticNumber > ↑k + 1

    It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.

    source
    theorem Erdos835.johnsonGraph_18_9_chromaticNumber :
    (SimpleGraph.johnson 18 9).chromaticNumber > 9 + 1

    The smallest case not on this page is $k=9$: But that one can be solved as well: The chromatic number of $J(18, 9)$ is at least $11$.

    source
    def Erdos835.johnsonBound :
    ℕ → ℕ → ℕ → ℕ

    Johnson's upper bound on the maximum size A(n, d, w) of a n-dimensional binary code of distance d and weight w is as follows:

    • If d > 2 * w, then A(n, d, w) = 1.
    • If d ≤ 2 * w, then A(n, d, w) ≤ ⌊n / w * A(n - 1, d, w - 1)⌋.
    Equations
    Instances For
      source
      theorem Erdos835.indepNum_johnson_le_johnsonBound {n k : ℕ} :
      (SimpleGraph.johnson n k).indepNum ≤ johnsonBound n 4 k

      Johnson's bound for the independence number of the Johnson graph.

      source
      theorem Erdos835.div_johnsonBound_le_chromaticNum_johnson {n k : ℕ} :
      ↑⌈↑(n.choose k) / ↑(johnsonBound n 4 k)⌉₊ ≤ (SimpleGraph.johnson n k).chromaticNumber

      Johnson's bound for the chromatic number of the Johnson graph.

      source
      theorem Erdos835.chromaticNumber_johnson_2k_k_lower_bound {k : ℕ} (hk : 3 ≤ k) (hk' : k ≤ 8) :
      ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

      It is known that for $3 \leq k \leq 8$, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.

      source
      theorem Erdos835.chromaticNumber_johnson_2k_k_lower_bound_odd {k : ℕ} (hk : 3 ≤ k) (hk' : k ≤ 300) (hk_odd : Odd k) :
      ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

      It is also known that for $3 \leq k \leq 203$ odd, the chromatic number of $J(2k, k)$ is greater than $k+1$, see Johnson graphs.

      source
      theorem Erdos835.johnson_chromaticNumber_odd (k : ℕ) (hk : 2 < k) (h : Odd k) :
      ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

      It can be seen that the chromatic number of $J(2k,k)$ is $>k+1$ for all odd $k>2$.

      source
      theorem Erdos835.johnson_chromaticNumber_composite (k : ℕ) (hk : 2 < k) (h : (k + 1).Composite) :
      ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

      Ma and Tang have proved that the chromatic number of $J(2k,k)$ is $>k+1$ for all $k>2$ not of the form $p-1$ for prime $p$.

      source
      theorem Erdos835.johnsonGraph_chromaticNumber_odd_of_johnson_chromaticNumber_composite :
      (∀ (k : ℕ), 2 < k → (k + 1).Composite → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber) → ∀ (k : ℕ) (hk : 2 < k) (h : Odd k), ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

      Ma and Tang's result implies the cases for odd $k$.

      source
      theorem Erdos835.johnson_chromaticNumber :
      sorry ↔ ∀ k ≥ 3, ↑k + 2 ≤ (SimpleGraph.johnson (2 * k) k).chromaticNumber

      Is the chromatic number of J(2 * k, k) always at least k + 2?