Elementary clique-number facts

These lemmas make the paper's assumptions n ≥ 1 and ω ≥ 1 explicit and isolate the edgeless ω = 1 case. The Turán factor is the coefficient 1 - 1 / ω(G) in Turán-type bounds.

This module is copied, up to the namespace, from SqOmega/Graph.lean in https://github.com/ShengtongZhang-alt/SqOmega (Liu, Tang, Zhang).

noncomputable def BollobasNikiforov.turanFactor {V : Type u_1} (G : SimpleGraph V) : ℝ

The coefficient 1 - 1 / ω(G) appearing in Turán-type bounds.

Equations

• BollobasNikiforov.turanFactor G = 1 - 1 / ↑G.cliqueNum

theorem BollobasNikiforov.SimpleGraph.one_le_cliqueNum {V : Type u_1} [Finite V] (G : SimpleGraph V) [Nonempty V] : 1 ≤ G.cliqueNum

A graph on a nonempty finite vertex type has clique number at least one.

theorem BollobasNikiforov.SimpleGraph.two_le_cliqueNum_of_adj {V : Type u_1} [Finite V] (G : SimpleGraph V) {u v : V} (huv : G.Adj u v) : 2 ≤ G.cliqueNum

The endpoints of an edge give a two-vertex clique.

theorem BollobasNikiforov.SimpleGraph.eq_bot_of_cliqueNum_eq_one {V : Type u_1} [Finite V] (G : SimpleGraph V) (hω : G.cliqueNum = 1) : G = ⊥

On a nonempty graph, clique number one forces the graph to be edgeless.

theorem BollobasNikiforov.SimpleGraph.cliqueNum_eq_one_iff_eq_bot {V : Type u_1} [Finite V] (G : SimpleGraph V) [Nonempty V] : G.cliqueNum = 1 ↔ G = ⊥

On a nonempty graph, clique number is one exactly in the edgeless case.

theorem BollobasNikiforov.turanFactor_nonneg {V : Type u_1} (G : SimpleGraph V) [Finite V] [Nonempty V] : 0 ≤ turanFactor G

The Turán coefficient is nonnegative for a graph with at least one vertex.

theorem BollobasNikiforov.turanFactor_pos {V : Type u_1} (G : SimpleGraph V) (hω : 2 ≤ G.cliqueNum) : 0 < turanFactor G

The Turán coefficient is positive when the clique number is at least two.