Subgraphs of large cochromatic number

DefinitionErdős Problem 760: subgraphs of large cochromatic number#✓fully proved

The proposition asserts two statements. First, there is a real number \(c > 0\) such that for every simple graph \(G\) on a finite vertex set with chromatic number \(m\) there are a subgraph \(H\) of \(G\) and a natural number \(k\) with \(k \ge c\,m / \log m\) such that the cochromatic number of \(H\) is at least \(k\). Second, there is a real number \(c > 0\) with the same property for the bound \(k \ge c\sqrt{m / \log m}\).

Here \(\log\) is the natural logarithm, with the conventions \(\log 0 = 0\) and \(x / 0 = 0\), so both bounds are \(0\) when \(m \le 1\). The second statement is the Erdős–Gimbel form.

def conjecture : Prop :=
  (∃ c > (0 : ℝ), ∀ (V : Type*) [Finite V] (G : SimpleGraph V) (m : ℕ),
    G.chromaticNumber = (m : ℕ∞) →
      ∃ H : G.Subgraph, ∃ k : ℕ, ((k : ℕ∞) ≤ H.coe.cochromaticNumber) ∧
        (c * (m : ℝ) / Real.log (m : ℝ) ≤ (k : ℝ))) ∧
  (∃ c > (0 : ℝ), ∀ (V : Type*) [Finite V] (G : SimpleGraph V) (m : ℕ),
    G.chromaticNumber = (m : ℕ∞) →
      ∃ H : G.Subgraph, ∃ k : ℕ, ((k : ℕ∞) ≤ H.coe.cochromaticNumber) ∧
        (c * Real.sqrt ((m : ℝ) / Real.log (m : ℝ)) ≤ (k : ℝ)))

Uses 1 · Used by 1

Statement usesCochromatic number

Used byAlon–Krivelevich–Sudakov theorem on subgraphs of large cochromatic number

TheoremAlon–Krivelevich–Sudakov theorem on subgraphs of large cochromatic number#●ready to prove

There is a real number \(c > 0\) such that for every simple graph \(G\) on a finite vertex set with chromatic number \(m\) there are a subgraph \(H\) of \(G\) and a natural number \(k\) with \(k \ge c\,m / \log m\) such that the cochromatic number of \(H\) is at least \(k\). Moreover, there is a real number \(c > 0\) with the same property for the bound \(k \ge c\sqrt{m / \log m}\).

Here \(\log\) is the natural logarithm, with the conventions \(\log 0 = 0\) and \(x / 0 = 0\), so both bounds are \(0\) when \(m \le 1\). This answers Erdős Problem 760 affirmatively.

public theorem_wanted conjecture_holds : conjecture

Sources

• plby/lean-proofs (following Alon, Krivelevich and Sudakov, Subgraphs with a large cochromatic number, 1997), https://github.com/plby/lean-proofs/blob/8822f7ddef30fadbd92e1c6ab4ed897af356af5e/src/v4.29.1/ErdosProblems/Erdos760.lean#L1306.

Uses 1

Statement usesErdős Problem 760: subgraphs of large cochromatic number

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.