Eq. (10) — the Laplacian of a weighted star satisfies ‖L(G)‖ ≤ Σ_e w_e + max_e w_e
ProvedQMaxCutBeyond.TwoQubit.eq_10graph-laplacianp2o-batch-pfp2ap2o-gran-per-chapterp2o-plan-paperp2o-v1quantum-max-cutstar-graph
Let be a star graph (every edge contains a fixed centre ) with nonnegative weights, and let be its weighted Laplacian. Then for every real vector
that is, .
In the proof of Lemma 1 the star Hamiltonian restricted to the Hamming-weight-one subspace is the Laplacian, so this bound is the spectral input of Lemma 1.
Formalization Note is real symmetric and positive semidefinite, so its norm is its largest eigenvalue, the maximum of the Rayleigh quotient; the statement is that quotient bound. The graph may have isolated vertices besides the star; if .
Preamble
import Mathlib import Definitions.Def_QMaxCutBeyond_TwoQubit_Setting
Formal statement
namespace QMaxCutBeyond.TwoQubit
open Matrix
/-- Eq. (10), p. 7: for a star graph with nonnegative weights, the Laplacian satisfies
`‖L(G)‖ ≤ Σ_{e∈E} w_e + max_{e∈E} w_e`, stated as the Rayleigh-quotient bound for the
(positive semidefinite, real symmetric) Laplacian. -/
theorem eq_10 {n : ℕ} (G : SimpleGraph (Fin n)) [DecidableRel G.Adj]
(w : Sym2 (Fin n) → ℝ) (hw : ∀ e, 0 ≤ w e) (c : Fin n) (hstar : IsStar G c)
(x : Fin n → ℝ) :
x ⬝ᵥ (laplacian G w *ᵥ x) ≤ (totalWeight G w + maxEdgeWeight G w) * (x ⬝ᵥ x) := by sorry
end QMaxCutBeyond.TwoQubit
Source
Anshu, Gosset & Morenz, Beyond product state approximations for a quantum analogue of Max Cut, arXiv:2003.14394v1, p. 7, eq. (10), proof of Lemma 1
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.