Prove2Me

Quantum Lovász Local Lemma (asymmetric form): R(⋂iXi)≥∏i(1−yi)\mathrm{R}(\bigcap_i X_i) \ge \prod_i (1-y_i)

Proved
QLLL.quantum_lll

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).

Let y1,…,yny_1, \dots, y_n be real numbers with 0≤yi<10 \le y_i < 1 such that R(Xi)≥1−yi∏j∈Γ(i)(1−yj)\mathrm{R}(X_i) \ge 1 - y_i \prod_{j \in \Gamma(i)} (1 - y_j) for every ii. Then

R(⋂i=1nXi) ≥ ∏i=1n(1−yi).\mathrm{R}\Big(\bigcap_{i=1}^{n} X_i\Big) \ \ge\ \prod_{i=1}^{n} (1 - y_i).

This is the main theorem of Ambainis, Kempe and Sattath (Theorem 14): the Lovász Local Lemma with events replaced by subspaces and probability replaced by relative dimension, with exactly the classical parameters. It is the instance of the abstract lemma QLLL.Valuation.lll at relative dimension.

Formalization Note The paper works with subspaces of a complex Hilbert space; the statement here holds over any field, since neither orthogonality nor an inner product is involved. 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 {m : ℕ} {X : Fin m → Submodule 𝕜 V}
    {Γ : Fin m → Finset (Fin m)} {y : Fin m → ℝ}
    (hΓ : (relDimValuation (𝕜 := 𝕜) (V := V)).IsDependencyGraph X Γ)
    (hy₀ : ∀ i, 0 ≤ y i) (hy₁ : ∀ i, y i < 1)
    (hX : ∀ i, 1 - y i * ∏ j ∈ Γ i, (1 - y j) ≤ relDim (X i)) :
    ∏ i, (1 - y i) ≤ 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 14 (Quantum Lovász Local Lemma)

View graph