Fractional coloring

DefinitionFractional clique number#✓fully proved

Let \(X\) be a graph with finite vertex set \(V(X)\). A fractional clique of \(X\) is a function \(f \colon V(X) \to \mathbb{R}\) with \(f(v) \ge 0\) for every vertex \(v\), such that \(\sum_{v \in S} f(v) \le 1\) for every independent set \(S\) of \(X\). The weight of \(f\) is \(\sum_{v \in V(X)} f(v)\). The fractional clique number \(\omega^*(X)\) of \(X\) is the supremum of the weights of all fractional cliques of \(X\).

noncomputable def _root_.SimpleGraph.fracCliqueNumber {V : Type*} [Fintype V]
    (G : SimpleGraph V) : ℝ :=
  sSup {q : ℝ | ∃ c : FracClique G, c.weight = q}

DefinitionFractional chromatic number#✓fully proved

Let \(X\) be a graph with finite vertex set \(V(X)\). A fractional colouring of \(X\) assigns to each set \(S\) of vertices of \(X\) a real weight \(f(S) \ge 0\), with \(f(S) = 0\) unless \(S\) is independent, such that \(\sum_{S \ni x} f(S) \ge 1\) for every vertex \(x\) of \(X\), the sum running over all sets of vertices containing \(x\). The weight of \(f\) is the sum of \(f(S)\) over all sets \(S\) of vertices of \(X\). The fractional chromatic number \(\chi^*(X)\) of \(X\) is the infimum of the weights of all fractional colourings of \(X\).

Since \(f\) vanishes off the independent sets, a fractional colouring is the same as a nonnegative function on the independent sets of \(X\), and both sums run over independent sets only.

noncomputable def _root_.SimpleGraph.fracChromaticNumber {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) : ℝ :=
  sInf {q : ℝ | ∃ c : FracColouring G, c.weight = q}

DefinitionRegular fractional colouring#✓fully proved

Let \(X\) be a finite simple graph. A fractional colouring of \(X\) assigns to each set \(S\) of vertices of \(X\) a real weight \(f(S) \ge 0\), with \(f(S) = 0\) unless \(S\) is independent, such that \(\sum_{S \ni x} f(S) \ge 1\) for every vertex \(x\), the sum running over all sets of vertices containing \(x\). The fractional colouring \(f\) is regular if \(\sum_{S \ni x} f(S) = 1\) for every vertex \(x\) of \(X\). Since \(f\) vanishes off the independent sets, this is the sum of \(f\) over the independent sets of \(X\) containing \(x\).

def FracColouring.IsRegular {V : Type*} [Fintype V] [DecidableEq V] {G : SimpleGraph V}
    (c : FracColouring G) : Prop :=
  ∀ u : V,
    (∑ s ∈ Finset.univ.filter (fun s => u ∈ s), c.w s) = 1

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.