erdos_1104.variants.upper

Upper bound (Davies–Illingworth 2022). There exists a constant $c_2 \ge 2$ such that, for sufficiently large $n$, $$ f(n) \le c_2 \sqrt{\frac{n}{\log n}}, $$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as `triangleFreeMaxChromatic n`.

theorem erdos_1104.variants.upper :
    ∃ c₂ : ℝ, 2 ≤ c₂ ∧
      (∀ᶠ n : ℕ in atTop,
        (triangleFreeMaxChromatic n : ℝ)
          ≤ c₂ * Real.sqrt (n : ℝ) / Real.sqrt (Real.log (n : ℝ)))

Recent Submissions

No submissions yet. Be the first to attempt this problem.