Balanced functions and the one-sided count

A function is (K, ν)-balanced when, on every rectangle with both sides of size at least K, under every split, the fraction of accepting inputs lies within ν of one half. A sumset extractor with error ν is balanced with K polynomial, for the same reason it is rectangle-free.

The one-sided count Network.card_accepting_inter_le bounds, for a network with unique satisfying assignments, the number of its accepted inputs on which a balanced f is 1. Fix a vertex set L. The accepted inputs are partitioned by the bits their satisfying assignment places on the cut of L, and each class is a rectangle of past and future assignments. Classes with both sides at least K are balanced. A class with a small past side has at most K - 1 rows; summing its columns over all such classes counts pairs of a future assignment and a cut assignment, and the cut assignment is determined by the future assignment together with the forward-crossing bits (BackwardDetermined). Symmetrically for small future sides with the backward-crossing bits (ForwardDetermined).

noncomputable def Algebraic.Cutwidth.rectangleOnes {n : ℕ} (f : Cslib.BooleanFunction n) (U : Finset (Fin n)) (P : Finset (↥U → Bool)) (Q : Finset (↥Uᶜ → Bool)) : Finset ((↥U → Bool) × (↥Uᶜ → Bool))

The points of the rectangle P × Q, under the split U, accepted by f.

Equations

• Algebraic.Cutwidth.rectangleOnes f U P Q = {pq ∈ P ×ˢ Q | f (Algebraic.Cutwidth.glue U pq.1 pq.2) = true}

def Algebraic.Cutwidth.Balanced {n : ℕ} (f : Cslib.BooleanFunction n) (K : ℕ) (ν : ℝ) : Prop

f is (K, ν)-balanced: on every rectangle with both sides of size at least K, under every split, the accepted fraction is within ν of 1/2.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Network.fwdCut {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] (L : Finset V) : Finset E

The forward-crossing edges of L: produced inside L, consumed outside.

Equations

• N.fwdCut L = {e ∈ N.cut L | N.fst e ∈ L}

noncomputable def Algebraic.Cutwidth.Network.bwdCut {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] (L : Finset V) : Finset E

The backward-crossing edges of L: produced outside L, consumed inside.

Equations

• N.bwdCut L = {e ∈ N.cut L | N.snd e ∈ L}

theorem Algebraic.Cutwidth.Network.mem_fwdCut {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] {L : Finset V} {e : E} : e ∈ N.fwdCut L ↔ e ∈ N.cut L ∧ N.fst e ∈ L

theorem Algebraic.Cutwidth.Network.mem_bwdCut {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] {L : Finset V} {e : E} : e ∈ N.bwdCut L ↔ e ∈ N.cut L ∧ N.snd e ∈ L

theorem Algebraic.Cutwidth.Network.fwdCut_subset {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] (L : Finset V) : N.fwdCut L ⊆ N.cut L

theorem Algebraic.Cutwidth.Network.bwdCut_subset {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] (L : Finset V) : N.bwdCut L ⊆ N.cut L

theorem Algebraic.Cutwidth.Network.card_fwdCut_add_card_bwdCut {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] (L : Finset V) : (N.fwdCut L).card + (N.bwdCut L).card = (N.cut L).card

The cut is the disjoint union of its forward- and backward-crossing edges.

def Algebraic.Cutwidth.Network.Unambiguous {n : ℕ} {V E : Type} (N : Network n V E) : Prop

Every accepted input has exactly one satisfying assignment.

Equations

• N.Unambiguous = ∀ (x : Fin n → Bool) (α α' : E → Bool), N.Satisfies x α → N.Satisfies x α' → α = α'

def Algebraic.Cutwidth.Network.ForwardDetermined {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] : Prop

The inputs read in L and the backward-crossing bits determine the cut.

Equations

• One or more equations did not get rendered due to their size.

def Algebraic.Cutwidth.Network.BackwardDetermined {n : ℕ} {V E : Type} (N : Network n V E) [Fintype E] : Prop

The inputs read outside L and the forward-crossing bits determine the cut.

Equations

• One or more equations did not get rendered due to their size.

theorem Algebraic.Cutwidth.Network.exists_satisfies_glue {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {L : Finset V} {σ : E → Bool} {p : ↥(N.past L) → Bool} (hp : p ∈ N.pastSet L σ) {q : ↥(N.past L)ᶜ → Bool} (hq : q ∈ N.futureSet L σ) : ∃ (γ : E → Bool), N.Satisfies (glue (N.past L) p q) γ ∧ ∀ e ∈ N.cut L, γ e = σ e

Gluing a consistent past and future gives a satisfying assignment that agrees with the cut assignment on the cut.

theorem Algebraic.Cutwidth.Network.glue_injOn {n : ℕ} (U : Finset (Fin n)) (S : Finset ((↥U → Bool) × (↥Uᶜ → Bool))) : Set.InjOn (fun (pq : (↥U → Bool) × (↥Uᶜ → Bool)) => glue U pq.1 pq.2) ↑S

Gluing is injective: a point of the product is recovered by restriction.

theorem Algebraic.Cutwidth.Network.card_accepting_inter_le {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {g : Cslib.BooleanFunction n} (hg : N.Computes g) (unique : N.Unambiguous) (fwd : N.ForwardDetermined) (bwd : N.BackwardDetermined) {f : Cslib.BooleanFunction n} {K : ℕ} {ν : ℝ} (hν : 0 ≤ ν) (hbal : Balanced f K ν) (L : Finset V) : ↑(accepting g ∩ accepting f).card ≤ (1 / 2 + ν) * ↑(accepting g).card + ↑(K - 1) * (2 ^ (n - (N.past L).card + (N.fwdCut L).card) + 2 ^ ((N.past L).card + (N.bwdCut L).card))

The one-sided count. For a network with unique satisfying assignments computing g, and a (K, ν)-balanced f, the accepted inputs of g on which f is 1 number at most (1/2 + ν) times the accepted inputs plus the thin-rectangle mass at the cut of L.