Restrict a Boolean function on α to the subtype of elements lying in a finset C.
Instances For
theorem
Beck.product_space_lll_existence
{α : Type u_1}
{ι : Type u_2}
[Fintype α]
[DecidableEq α]
[Fintype ι]
[DecidableEq ι]
(G : Digraph ι)
[DecidableRel G.Adj]
(A : ι → Set (α → Bool))
(hA_meas : ∀ (i : ι), MeasurableSet (A i))
(coords : ι → Finset α)
(hA_coords : ∀ (i : ι) (f g : α → Bool), (∀ a ∈ coords i, f a = g a) → (f ∈ A i ↔ g ∈ A i))
(hG_dep : ∀ (i j : ι), ¬G.Adj i j → j ≠ i → Disjoint (coords i) (coords j))
(x : ι → ℝ)
(hx01 : ∀ (i : ι), 0 ≤ x i ∧ x i < 1)
(hbound :
∀ (i : ι),
↑{x : α → Bool | x ∈ A i}.card ≤ (ENNReal.ofReal (x i * ∏ j ∈ LovaszLocalLemma.neighbors G i, (1 - x j))).toReal * 2 ^ Fintype.card α)
:
∃ (f : α → Bool), ∀ (i : ι), f ∉ A i
General product-space LLL: in the uniform product probability space on α → Bool, if each
bad event $A_i$ depends only on the coordinates in coords i, and the dependency digraph $G$
together with weights $x_i \in [0,1)$ satisfies the LLL probability bound, then there exists a
Boolean assignment avoiding all bad events.