1. FormalConjecturesForMathlib
  2. Combinatorics
  3. SimpleGraph
  4. LovaszTheta
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ module public import Mathlib.Analysis.Matrix.Spectrum public import Mathlib.Combinatorics.SimpleGraph.Basic public import FormalConjecturesForMathlib.Analysis.Matrix.Spectrum@[expose] public sectionnamespace SimpleGraphvariable {α : Type*} [Fintype α] [DecidableEq α]

Lovász Theta Function ($\vartheta(G)$). The Lovász theta function is defined as: $$\vartheta(G) = \min \lambda_{\max}(A)$$ where the minimum is taken over all real symmetric (Hermitian) matrices $A$ such that:

    $A_{ii} = 1$ for all $i$ (diagonal entries are $1$), and

    $A_{ij} = 1$ for all ${i,j} \notin E(G)$ (entries corresponding to non-edges are $1$).

Here $\lambda_{\max}(A)$ denotes the maximum eigenvalue of $A$.

noncomputable def lovaszThetaFunction (G : SimpleGraph α) [DecidableRel G.Adj] : ℝ := sInf {(Matrix.IsHermitian.maxEigenvalue hA) | (A : Matrix α α ℝ) (hA : A.IsHermitian) (_ : ∀ i, A i i = 1) (_ : ∀ i j, ¬G.Adj i j → A i j = 1)}

The Lovász theta function of a graph on an empty vertex type is $0$.

All goals completed! 🐙α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nonempty αA:Matrix α α ℝhA:A.IsHermitianhdiag:∀ (i : α), A i i = 1htrace:↑(Fintype.card α) = ∑ i, hA.eigenvalues ihle:↑(Fintype.card α) ≤ ↑(Fintype.card α) * hA.maxEigenvalue⊢ 1 ≤ hA.maxEigenvalue α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nonempty αA:Matrix α α ℝhA:A.IsHermitianhdiag:∀ (i : α), A i i = 1htrace:↑(Fintype.card α) = ∑ i, hA.eigenvalues ihle:↑(Fintype.card α) ≤ ↑(Fintype.card α) * hA.maxEigenvaluehpos:0 < ↑(Fintype.card α)⊢ 1 ≤ hA.maxEigenvalue All goals completed! 🐙α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhα:IsEmpty α⊢ BddBelow {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬G.Adj i j → A i j = 1), hA.maxEigenvalue = x} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhα:IsEmpty α⊢ 0 ∈ lowerBounds {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬G.Adj i j → A i j = 1), hA.maxEigenvalue = x} α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.Adjhα:IsEmpty αA:Matrix α α ℝhA:A.IsHermitianw✝¹:∀ (i : α), A i i = 1w✝:∀ (i j : α), ¬G.Adj i j → A i j = 1⊢ 0 ≤ hA.maxEigenvalue All goals completed! 🐙α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αG:SimpleGraph αinst✝:DecidableRel G.AdjJ:Matrix α α ℝ := Matrix.of fun x x_1 ↦ 1hJ:J.IsHermitian⊢ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬G.Adj i j → A i j = 1), hA.maxEigenvalue = x}.Nonempty All goals completed! 🐙

The Lovász theta function of any nonempty graph is at least $1$.

theorem one_le_lovaszThetaFunction [Nonempty α] (G : SimpleGraph α) [DecidableRel G.Adj] : 1 ≤ lovaszThetaFunction G := α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αinst✝¹:Nonempty αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ 1 ≤ G.lovaszThetaFunction α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αinst✝¹:Nonempty αG:SimpleGraph αinst✝:DecidableRel G.Adj⊢ ∀ b ∈ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬G.Adj i j → A i j = 1), hA.maxEigenvalue = x}, 1 ≤ b α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αinst✝¹:Nonempty αG:SimpleGraph αinst✝:DecidableRel G.AdjA:Matrix α α ℝhA:A.IsHermitianhdiag:∀ (i : α), A i i = 1w✝:∀ (i j : α), ¬G.Adj i j → A i j = 1⊢ 1 ≤ hA.maxEigenvalue All goals completed! 🐙

Adding edges to a graph can only decrease or preserve its Lovász theta function.

theorem lovaszThetaFunction_anti {G H : SimpleGraph α} [DecidableRel G.Adj] [DecidableRel H.Adj] (h : G ≤ H) : lovaszThetaFunction H ≤ lovaszThetaFunction G := α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αG:SimpleGraph αH:SimpleGraph αinst✝¹:DecidableRel G.Adjinst✝:DecidableRel H.Adjh:G ≤ H⊢ H.lovaszThetaFunction ≤ G.lovaszThetaFunction α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αG:SimpleGraph αH:SimpleGraph αinst✝¹:DecidableRel G.Adjinst✝:DecidableRel H.Adjh:G ≤ H⊢ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬G.Adj i j → A i j = 1), hA.maxEigenvalue = x} ⊆ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬H.Adj i j → A i j = 1), hA.maxEigenvalue = x} α:Type u_1inst✝³:Fintype αinst✝²:DecidableEq αG:SimpleGraph αH:SimpleGraph αinst✝¹:DecidableRel G.Adjinst✝:DecidableRel H.Adjh:G ≤ HA:Matrix α α ℝhA:A.IsHermitianhdiag:∀ (i : α), A i i = 1hnonadj:∀ (i j : α), ¬G.Adj i j → A i j = 1⊢ hA.maxEigenvalue ∈ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬H.Adj i j → A i j = 1), hA.maxEigenvalue = x} All goals completed! 🐙

The Lovász theta function of the complete graph $K_n$ ($n \ge 1$) is $1$.

α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nonempty αh1:Matrix.IsHermitian 1hmem:h1.maxEigenvalue ∈ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬⊤.Adj i j → A i j = 1), hA.maxEigenvalue = x}i:αhmv:(h1.eigenvectorBasis i).ofLp = h1.eigenvalues i • (h1.eigenvectorBasis i).ofLphgt:1 < h1.eigenvalues ihzero:(h1.eigenvectorBasis i).ofLp = 0⊢ False exact h1.eigenvectorBasis.orthonormal.ne_zero i (α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nonempty αh1:Matrix.IsHermitian 1hmem:h1.maxEigenvalue ∈ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬⊤.Adj i j → A i j = 1), hA.maxEigenvalue = x}i:αhmv:(h1.eigenvectorBasis i).ofLp = h1.eigenvalues i • (h1.eigenvectorBasis i).ofLphgt:1 < h1.eigenvalues ihzero:(h1.eigenvectorBasis i).ofLp = 0⊢ h1.eigenvectorBasis i = 0 α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nonempty αh1:Matrix.IsHermitian 1hmem:h1.maxEigenvalue ∈ {x | ∃ A, ∃ (hA : A.IsHermitian) (_ : ∀ (i : α), A i i = 1) (_ : ∀ (i j : α), ¬⊤.Adj i j → A i j = 1), hA.maxEigenvalue = x}i:αhmv:(h1.eigenvectorBasis i).ofLp = h1.eigenvalues i • (h1.eigenvectorBasis i).ofLphgt:1 < h1.eigenvalues ihzero:(h1.eigenvectorBasis i).ofLp = 0k:α⊢ (h1.eigenvectorBasis i).ofLp k = WithLp.ofLp 0 k; All goals completed! 🐙) α:Type u_1inst✝²:Fintype αinst✝¹:DecidableEq αinst✝:Nonempty α⊢ 1 ≤ ⊤.lovaszThetaFunction All goals completed! 🐙

The Lovász theta function of the edgeless graph $\overline{K_n}$ is $n$.

α:Type u_1inst✝¹:Fintype αinst✝:DecidableEq αhα:IsEmpty α⊢ ⊥.lovaszThetaFunction = ↑(Fintype.card α) All goals completed! 🐙

The Lovász theta function of any graph is at most its number of vertices.

theorem lovaszThetaFunction_le_card (G : SimpleGraph α) [DecidableRel G.Adj] : lovaszThetaFunction G ≤ Fintype.card α := (lovaszThetaFunction_anti bot_le).trans_eq lovaszThetaFunction_botend SimpleGraph