Local lemma for an infinite index set: the whole family has a nonzero meet
ProvedQLLL.iInf_ne_botlattice-theorylovasz-local-lemmaquantum-lll
Let be a complete lattice and a valuation (nonnegative, monotone, modular, , ). Let be a family in indexed by an arbitrary set , and let be finite sets forming a dependency graph: for every and every finite with and , . Let with for every , and let be a real number with for every finite . Assume is continuous from above in the following sense: whenever for every finite , also . Suppose moreover that .
Then
This is the qualitative conclusion of QLLL.lll_iInf: under the same hypotheses and a positive lower bound on the finite products, the meet of the whole family is not the bottom element.
Preamble
import Definitions.Def_QLLL_LocalLemma_Basic
import Definitions.Def_QLLL_LocalLemma_Infinite
import Mathlib
open QLLL
open Finset
variable {α : Type*} [CompleteLattice α] (R : Valuation α)
variable {ι : Type*} {X : ι → α} {Γ : ι → Finset ι} {y : ι → ℝ}Formal statement
theorem QLLL.iInf_ne_bot (hΓ : IsDependencyGraphOn R X Γ)
(hy₀ : ∀ i, 0 ≤ y i) (hy₁ : ∀ i, y i < 1)
(hX : ∀ i, 1 - y i * ∏ j ∈ Γ i, (1 - y j) ≤ R (X i))
(c : ℝ) (hc : ∀ S : Finset ι, c ≤ ∏ j ∈ S, (1 - y j)) (hcpos : 0 < c)
(hcont : ∀ b : ℝ, (∀ S : Finset ι, b ≤ R (S.inf X)) → b ≤ R (⨅ i, X i)) :
(⨅ i, X i) ≠ ⊥ := by sorrySource
Not in the paper; an extension of Theorem 14 to infinite index sets. Formalization companion to Ambainis, Kempe and Sattath, A Quantum Lovász Local Lemma, arXiv:0911.1696; see the blueprint https://sattath.github.io/Quantum-Lovasz-Local-Lemma/blueprint/