Prove2Me

Quantum Lovász Local Lemma (symmetric form): R(⋂iXi)>0\mathrm{R}(\bigcap_i X_i) > 0 when p e (d+1)≤1p\,e\,(d+1) \le 1

Proved
QLLL.quantum_lll_symmetric

by sattath · Oct 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

lovasz-local-lemmaquantum-informationquantum-lll

Let VV be a nonzero finite-dimensional vector space over a field K\mathbb{K}, and for a subspace X⊆VX \subseteq V write

R(X)=dim⁡Xdim⁡V\mathrm{R}(X) = \frac{\dim X}{\dim V}

for its relative dimension (Definition 3 of the paper). Let X1,…,XnX_1, \dots, X_n be subspaces of VV and let Γ(1),…,Γ(n)⊆{1,…,n}\Gamma(1), \dots, \Gamma(n) \subseteq \{1, \dots, n\} form a dependency graph for relative dimension: for every ii and every set SS of indices with i∉Si \notin S and S∩Γ(i)=∅S \cap \Gamma(i) = \emptyset, R(Xi∩⋂j∈SXj)=R(Xi) R(⋂j∈SXj)\mathrm{R}\big(X_i \cap \bigcap_{j \in S} X_j\big) = \mathrm{R}(X_i)\,\mathrm{R}\big(\bigcap_{j \in S} X_j\big).

Suppose every Γ(i)\Gamma(i) has at most dd elements, R(Xi)≥1−p\mathrm{R}(X_i) \ge 1 - p for every ii, and p⋅e⋅(d+1)≤1p \cdot e \cdot (d+1) \le 1. Then

R(⋂i=1nXi) > 0,\mathrm{R}\Big(\bigcap_{i=1}^{n} X_i\Big) \ >\ 0,

that is, the subspaces have a nonzero common vector.

This is Theorem 4 of Ambainis, Kempe and Sattath, the symmetric quantum local lemma, and the instance of QLLL.Valuation.lll_symmetric at relative dimension. It is the form applied to kk-QSAT.

Formalization Note The statement holds over any field. "Mutually R-independent of all but dd of the others" is expressed through a dependency graph with out-degree at most dd. The index set is Fin n. The dependency-graph condition excludes ii itself from the independent family (the paper's Definition 12 read literally includes ii when (i,i)∉E(i,i) \notin E, which would force R(Xi)∈{0,1}R(X_i) \in \{0,1\}), and mutual independence is stated in product form rather than through conditional values as in Definition 9; the two agree whenever the conditional is defined.

Preamble
import Definitions.Def_QLLL_LocalLemma_Basic
import Mathlib

open QLLL
open Finset
open Module
variable {𝕜 : Type*} [Field 𝕜] {V : Type*} [AddCommGroup V] [Module 𝕜 V]
variable [FiniteDimensional 𝕜 V] [Nontrivial V]
Formal statement
theorem QLLL.quantum_lll_symmetric {m : ℕ} {X : Fin m → Submodule 𝕜 V}
    {Γ : Fin m → Finset (Fin m)} {p : ℝ} {d : ℕ}
    (hΓ : (relDimValuation (𝕜 := 𝕜) (V := V)).IsDependencyGraph X Γ)
    (hd : ∀ i, (Γ i).card ≤ d) (hX : ∀ i, 1 - p ≤ relDim (X i))
    (hp : p * Real.exp 1 * (d + 1) ≤ 1) :
    0 < relDim (Finset.univ.inf X) := by sorry
Source
A. Ambainis, J. Kempe, O. Sattath, A Quantum Lovász Local Lemma, J. ACM 59(5):24 (2012), arXiv:0911.1696 (numbering of the arXiv version), Theorem 4 (symmetric Quantum Lovász Local Lemma)

View graph