The rank-two conic parameter χ''_{vec,3}

chiVec3 G is the supremum of the Frobenius mass inner X X over PSD matrices of rank at most two, nonnegative on the edges of G, and normalized so that the mass of X ⊙ X off those edges equals 1. The feasible set is nonempty and compact, so the supremum is attained.

def BollobasNikiforov.onesMatrix {V : Type u_1} : Matrix V V ℝ

The all-ones matrix J.

Equations

• BollobasNikiforov.onesMatrix = Matrix.of fun (x x_1 : V) => 1

def BollobasNikiforov.offEdgeMatrix {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Matrix V V ℝ

Off-edge indicator I + A_{Gᶜ} = J - A_G. Equals 1 on the diagonal and on non-edges of G, and 0 on edges.

Equations

• BollobasNikiforov.offEdgeMatrix G = 1 + SimpleGraph.adjMatrix ℝ Gᶜ

theorem BollobasNikiforov.onesMatrix_apply {V : Type u_1} (i j : V) : onesMatrix i j = 1

theorem BollobasNikiforov.offEdgeMatrix_apply {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (i j : V) : offEdgeMatrix G i j = if G.Adj i j then 0 else 1

theorem BollobasNikiforov.inner_onesMatrix_hadamard_self {V : Type u_1} [Fintype V] (X : Matrix V V ℝ) : inner onesMatrix (X.hadamard X) = inner X X

theorem BollobasNikiforov.inner_offEdgeMatrix_hadamard_self {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (X : Matrix V V ℝ) : inner (offEdgeMatrix G) (X.hadamard X) = ∑ i : V, ∑ j : V, if G.Adj i j then 0 else X i j ^ 2

theorem BollobasNikiforov.sum_diag_sq_le_inner_offEdgeMatrix {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] (X : Matrix V V ℝ) : ∑ i : V, X i i ^ 2 ≤ inner (offEdgeMatrix G) (X.hadamard X)

The mass on the diagonal is at most the off-edge normalization.

CG06 — feasible set and the parameter

def BollobasNikiforov.ChiVec3Feasible {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (X : Matrix V V ℝ) : Prop

Feasible matrices for χ''_{vec,3}.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BollobasNikiforov.chiVec3 {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ℝ

CG06. The parameter χ''_{vec,3}(G).

Equations

• BollobasNikiforov.chiVec3 G = sSup ((fun (X : Matrix V V ℝ) => BollobasNikiforov.inner X X) '' {X : Matrix V V ℝ | BollobasNikiforov.ChiVec3Feasible G X})

Rank-two writing

theorem BollobasNikiforov.posSemidef_add_vecMulVec {V : Type u_1} [Finite V] (u v : V → ℝ) : (Matrix.vecMulVec u u + Matrix.vecMulVec v v).PosSemidef

theorem BollobasNikiforov.rank_add_vecMulVec_le {V : Type u_1} [Fintype V] (u v : V → ℝ) : (Matrix.vecMulVec u u + Matrix.vecMulVec v v).rank ≤ 2

theorem BollobasNikiforov.exists_add_vecMulVec_of_posSemidef_rank_le_two {V : Type u_1} [Fintype V] {X : Matrix V V ℝ} (hX : X.PosSemidef) (hr : X.rank ≤ 2) : ∃ (u : V → ℝ) (v : V → ℝ), X = Matrix.vecMulVec u u + Matrix.vecMulVec v v

A real PSD matrix of rank at most two is a sum of two real outer products.

CG07 — nonempty compact feasible set

def BollobasNikiforov.chiVec3Param {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Set ((V → ℝ) × (V → ℝ))

Parameter domain for the rank-two writing: bounded outer-product data satisfying the normalization and edge-nonnegativity constraints.

Equations

• One or more equations did not get rendered due to their size.

theorem BollobasNikiforov.continuous_add_vecMulVec {V : Type u_1} : Continuous fun (p : (V → ℝ) × (V → ℝ)) => Matrix.vecMulVec p.1 p.1 + Matrix.vecMulVec p.2 p.2

theorem BollobasNikiforov.continuous_inner_self {V : Type u_1} [Fintype V] : Continuous fun (X : Matrix V V ℝ) => inner X X

theorem BollobasNikiforov.continuous_inner_offEdge_hadamard {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] : Continuous fun (X : Matrix V V ℝ) => inner (offEdgeMatrix G) (X.hadamard X)

theorem BollobasNikiforov.mem_pi_Icc_iff {V : Type u_1} {u : V → ℝ} : (u ∈ Set.univ.pi fun (x : V) => Set.Icc (-1) 1) ↔ ∀ (i : V), u i ∈ Set.Icc (-1) 1

theorem BollobasNikiforov.isClosed_chiVec3Param {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] : IsClosed (chiVec3Param G)

theorem BollobasNikiforov.isCompact_chiVec3Param {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] : IsCompact (chiVec3Param G)

theorem BollobasNikiforov.mem_chiVec3Param_of_add_vecMulVec {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} {u v : V → ℝ} (hX : X = Matrix.vecMulVec u u + Matrix.vecMulVec v v) (hnorm : inner (offEdgeMatrix G) (X.hadamard X) = 1) (hnn : ∀ (i j : V), G.Adj i j → 0 ≤ X i j) : (u, v) ∈ chiVec3Param G

theorem BollobasNikiforov.ChiVec3Feasible.mem_image_param {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} (hX : ChiVec3Feasible G X) : X ∈ (fun (p : (V → ℝ) × (V → ℝ)) => Matrix.vecMulVec p.1 p.1 + Matrix.vecMulVec p.2 p.2) '' chiVec3Param G

theorem BollobasNikiforov.ChiVec3Feasible.of_mem_image_param {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} (hX : X ∈ (fun (p : (V → ℝ) × (V → ℝ)) => Matrix.vecMulVec p.1 p.1 + Matrix.vecMulVec p.2 p.2) '' chiVec3Param G) : ChiVec3Feasible G X

theorem BollobasNikiforov.chiVec3FeasibleSet_eq_image {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] : {X : Matrix V V ℝ | ChiVec3Feasible G X} = (fun (p : (V → ℝ) × (V → ℝ)) => Matrix.vecMulVec p.1 p.1 + Matrix.vecMulVec p.2 p.2) '' chiVec3Param G

theorem BollobasNikiforov.chiVec3Feasible_single {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : ChiVec3Feasible G (Matrix.vecMulVec (Pi.single (Classical.arbitrary V) 1) (Pi.single (Classical.arbitrary V) 1))

CG07. A standard-basis rank-one matrix is feasible after the normalization (already equal to 1).

theorem BollobasNikiforov.chiVec3FeasibleSet_nonempty {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : {X : Matrix V V ℝ | ChiVec3Feasible G X}.Nonempty

theorem BollobasNikiforov.isCompact_chiVec3FeasibleSet {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] : IsCompact {X : Matrix V V ℝ | ChiVec3Feasible G X}

CG07. The feasible set is compact.

theorem BollobasNikiforov.bddAbove_image_inner_chiVec3 {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] : BddAbove ((fun (X : Matrix V V ℝ) => inner X X) '' {X : Matrix V V ℝ | ChiVec3Feasible G X})

theorem BollobasNikiforov.exists_isMaxOn_inner_chiVec3 {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : ∃ (X : Matrix V V ℝ), ChiVec3Feasible G X ∧ IsMaxOn (fun (X : Matrix V V ℝ) => inner X X) {X : Matrix V V ℝ | ChiVec3Feasible G X} X

CG07. The Frobenius objective attains its maximum on the feasible set.

CG09 — clique Gram matrix

def BollobasNikiforov.cliqueIndicator {V : Type u_1} [DecidableEq V] (s : Finset V) : V → ℝ

Indicator of a vertex set.

Equations

• BollobasNikiforov.cliqueIndicator s i = if i ∈ s then 1 else 0

noncomputable def BollobasNikiforov.cliqueGram {V : Type u_1} [DecidableEq V] (s : Finset V) : Matrix V V ℝ

Normalized rank-one Gram matrix of a clique: qqᵀ / √r.

Equations

• BollobasNikiforov.cliqueGram s = (1 / √↑s.card) • Matrix.vecMulVec (BollobasNikiforov.cliqueIndicator s) (BollobasNikiforov.cliqueIndicator s)

theorem BollobasNikiforov.cliqueIndicator_apply {V : Type u_1} [DecidableEq V] (s : Finset V) (i : V) : cliqueIndicator s i = if i ∈ s then 1 else 0

theorem BollobasNikiforov.cliqueGram_apply {V : Type u_1} [DecidableEq V] (s : Finset V) (i j : V) : cliqueGram s i j = if i ∈ s ∧ j ∈ s then 1 / √↑s.card else 0

theorem BollobasNikiforov.cliqueGram_sq_apply {V : Type u_1} [DecidableEq V] {s : Finset V} (hs : s.Nonempty) (i j : V) : cliqueGram s i j ^ 2 = if i ∈ s ∧ j ∈ s then 1 / ↑s.card else 0

theorem BollobasNikiforov.rank_smul_le {V : Type u_1} [Fintype V] (c : ℝ) (A : Matrix V V ℝ) : (c • A).rank ≤ A.rank

theorem BollobasNikiforov.inner_offEdge_cliqueGram {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {s : Finset V} (hs : G.IsClique ↑s) (hne : s.Nonempty) : inner (offEdgeMatrix G) ((cliqueGram s).hadamard (cliqueGram s)) = 1

CG09. Off-edge mass of the clique Gram matrix is 1.

theorem BollobasNikiforov.chiVec3Feasible_cliqueGram {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {s : Finset V} (hs : G.IsClique ↑s) (hne : s.Nonempty) : ChiVec3Feasible G (cliqueGram s)

CG09. The clique Gram matrix is feasible.

theorem BollobasNikiforov.inner_cliqueGram {V : Type u_1} [Fintype V] [DecidableEq V] {s : Finset V} (hne : s.Nonempty) : inner (cliqueGram s) (cliqueGram s) = ↑s.card

CG09. The clique Gram matrix has Frobenius mass s.card.

theorem BollobasNikiforov.cliqueNum_le_chiVec3 {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : ↑G.cliqueNum ≤ chiVec3 G

A maximum clique witnesses ω(G) ≤ χ''_{vec,3}(G).

CG08 — upper bound chiVec3 ≤ cliqueNum

theorem BollobasNikiforov.onesMatrix_eq_adjMatrix_add_offEdgeMatrix {V : Type u_1} [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] : onesMatrix = SimpleGraph.adjMatrix ℝ G + offEdgeMatrix G

theorem BollobasNikiforov.inner_adjMatrix_hadamard_self_eq_sum_posPart_sq {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} (hnn : ∀ (i j : V), G.Adj i j → 0 ≤ X i j) : inner (SimpleGraph.adjMatrix ℝ G) (X.hadamard X) = ∑ i : V, ∑ j : V, SimpleGraph.adjMatrix ℝ G i j * posPart X i j ^ 2

theorem BollobasNikiforov.inner_adjMatrix_hadamard_self_nonneg {V : Type u_1} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (X : Matrix V V ℝ) : 0 ≤ inner (SimpleGraph.adjMatrix ℝ G) (X.hadamard X)

theorem BollobasNikiforov.inner_adjMatrix_hadamard_le_turanFactor {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} (hX : ChiVec3Feasible G X) : inner (SimpleGraph.adjMatrix ℝ G) (X.hadamard X) ≤ turanFactor G * inner X X

theorem BollobasNikiforov.inner_self_eq_inner_adjMatrix_hadamard_add_one {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] {X : Matrix V V ℝ} (hX : ChiVec3Feasible G X) : inner X X = inner (SimpleGraph.adjMatrix ℝ G) (X.hadamard X) + 1

theorem BollobasNikiforov.one_sub_turanFactor {V : Type u_1} {G : SimpleGraph V} : 1 - turanFactor G = 1 / ↑G.cliqueNum

theorem BollobasNikiforov.inner_le_cliqueNum_of_chiVec3Feasible {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] {X : Matrix V V ℝ} (hX : ChiVec3Feasible G X) : inner X X ≤ ↑G.cliqueNum

A feasible matrix has Frobenius mass at most ω(G).

theorem BollobasNikiforov.chiVec3_le_cliqueNum {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : chiVec3 G ≤ ↑G.cliqueNum

CG08. Every feasible objective is ≤ ω(G), so the supremum is too.

CG10 — cor:parameter

theorem BollobasNikiforov.chiVec3_eq_cliqueNum {V : Type u_1} [Fintype V] [DecidableEq V] {G : SimpleGraph V} [DecidableRel G.Adj] [Nonempty V] : chiVec3 G = ↑G.cliqueNum

CG10. Corollary cor:parameter.