ε-light vertex sets

Definitionε-light vertex sets#✓fully proved

Let \(G\) be a simple graph on a finite vertex set \(V\), let \(\varepsilon\) be a real number and let \(S \subseteq V\). Let \(L\) be the real Laplacian matrix of \(G\) and \(L_S\) the real Laplacian matrix of the graph on \(V\) whose edges are the edges of \(G\) with both endpoints in \(S\). The set \(S\) is \(\varepsilon\)-light in \(G\) if \(\varepsilon L - L_S\) is positive semidefinite.

def IsEpsilonLight (G : SimpleGraph V) (ε : ℝ) (S : Finset V) : Prop :=
  open Classical in
  letI G_S := G.induce S |>.spanningCoe
  letI L := lapMatrix ℝ G
  letI L_S := lapMatrix ℝ (G_S)
  PosSemidef (ε • L - L_S)

Used by 1

Used byThe large ε-light subset property

DefinitionThe large ε-light subset property#✓fully proved

The statement that there is a real constant \(c > 0\) such that for every natural number \(n\), every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) and every real number \(\varepsilon\) with \(0 < \varepsilon < 1\), some set \(S\) of vertices that is \(\varepsilon\)-light in \(G\) has at least \(c \varepsilon n\) elements.

def epsilonLightSubsetExists : Prop :=
  ∃ (c : ℝ), c > 0 ∧ ∀ (n : ℕ) (G : SimpleGraph (Fin n)) (ε : ℝ),
  0 < ε → ε < 1 →
  ∃ (S : Finset (Fin n)), IsEpsilonLight G ε S ∧ (S.card : ℝ) ≥ c * ε * n

Uses 1 · Used by 1

Statement usesε-light vertex sets

Used byEvery graph has a large ε-light vertex set

TheoremEvery graph has a large ε-light vertex set#●ready to prove

There is a real constant \(c > 0\) such that for every natural number \(n\), every simple graph \(G\) on the vertex set \(\{0, \dots, n-1\}\) and every real number \(\varepsilon\) with \(0 < \varepsilon < 1\), there is a set \(S\) of vertices with at least \(c \varepsilon n\) elements that is \(\varepsilon\)-light in \(G\): the matrix \(\varepsilon L - L_S\) is positive semidefinite, where \(L\) is the real Laplacian matrix of \(G\) and \(L_S\) is the real Laplacian matrix of the graph on all \(n\) vertices whose edges are the edges of \(G\) with both endpoints in \(S\).

Appendix B.6 of the source proves this, with \(c = 1/42\), as Lemma B.1 (stated for weighted graphs).

public theorem_wanted epsilonLightSubsetExists_holds : epsilonLightSubsetExists

Sources

• First Proof authors, arXiv:2602.05192v2, Appendix B.6 (Lemma B.1), https://arxiv.org/html/2602.05192v2.

Uses 1

Statement usesThe large ε-light subset property

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.