noncomputable def SimpleGraph.fractionalAlpha {α : Type u_1} [Fintype α] (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ

Fractional alpha. This is defined as $$ \max_x \sum_{v \in V} x_v $$ subject to $0 \le x_v \le 1$ for all $v \in V$ and $x_u + x_v \le 1$ whenever $(u, v)$ are connected by an edge.

Equations

• G.fractionalAlpha = sSup {x : ℝ | ∃ (x_1 : α → ℝ) (_ : ∀ (v : α), x_1 v ∈ Set.Icc 0 1) (_ : ∀ (u v : α), G.Adj u v → x_1 u + x_1 v ≤ 1), ∑ i : α, x_1 i = x}