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

Lovász Theta Function (ϑ(G)) The Lovász theta function is defined as: ϑ(G) = min λ_max(A) where the minimum is taken over all symmetric matrices A such that:

A_ij = 1 for all i = j (diagonal entries are 1) A_ij = 0 for all {i,j} ∈ E (entries corresponding to edges are 0) A is positive semidefinite

Here λ_max(A) denotes the maximum eigenvalue of A.

Equations

• G.lovaszThetaFunction = sInf {x : ℝ | ∃ (A : Matrix α α ℝ) (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), G.Adj i j → A i j = 0), hA.maxEigenvalue = x}