Dense rectangle-free sets and sets of small bias exist

The frontier lower bounds are stated for families of sets S_n ⊆ U^n that are rectangle-free, or of small bias on large rectangles, with thresholds K_n such that log K_n = o(n). This file shows, by counting, that such families exist over the binary alphabet, so that the hypotheses of the bundled claims CircuitLowerBound and AverageCaseBound are satisfiable.

Dense rectangle-free sets (exists_rectangleFree_two_pow_le_ncard). For n coordinates, some set of at least 2 ^ (n - 1) bit strings, half of the cube, is (n + 2)-rectangle-free. A set containing a rectangle with both sides of size at least K contains one with sides of size exactly K, and such a rectangle is spanned by K inputs z i: its sides are the parts of the z i on the cut and off it. So there are at most 2 ^ n · (2 ^ n) ^ K of them, each with K ^ 2 points, and at most 2 ^ (n + n K - K ^ 2) of the 2 ^ (2 ^ n) sets of bit strings contain one. For K = n + 2 this is a 2 ^ (-n - 4) fraction, while at least half of all sets have at least 2 ^ (n - 1) elements.

Sets of small bias (exists_rectangleBias). If n + 1 ≤ b ^ 2 K, some set of bit strings has density within b of 1/2 on every rectangle with both sides of size at least K. A rectangle with sides of sizes k₁ and k₂ is spanned by k₁ + k₂ inputs, and by Hoeffding's inequality (Cslib.BitString.card_filter_le_abs_card_filter_sub_half_le) at most a 2 exp (-2 b ^ 2 k₁ k₂) fraction of all sets has bias more than b on it. The union bound over all sizes and all spanning inputs is less than one.

For families over Fin n, the first gives the hypotheses of the worst-case claims with K_n = n + 2 (exists_rectangleFree_family), and the second those of the average-case claims with K_n = (n + 1) ^ 3 and bias b_n = 1 / (n + 1) → 0 (exists_rectangleBias_family).

Main results

• Cslib.Circuits.Frontier.exists_rectangleFree_two_pow_le_ncard: dense rectangle-free sets.
• Cslib.Circuits.Frontier.exists_rectangleFree_family: a family meeting the hypotheses of the worst-case frontier lower bounds.
• Cslib.Circuits.Frontier.exists_rectangleBias: sets of small bias on large rectangles.
• Cslib.Circuits.Frontier.exists_rectangleBias_family: a family meeting the hypotheses of the average-case frontier lower bounds, with bias tending to zero.

References

• N. Alon, J. H. Spencer, The Probabilistic Method
• E. Kushilevitz, N. Nisan, Communication Complexity, Ch. 1

Rectangles spanned by inputs

Dense rectangle-free sets

theorem Cslib.Circuits.Frontier.exists_rectangleFree_two_pow_le_ncard {ι : Type u_1} [Fintype ι] : ∃ (S : Set (ι → Bool)), RectangleFree S (Fintype.card ι + 2) ∧ 2 ^ (Fintype.card ι - 1) ≤ S.ncard

Dense rectangle-free sets exist. For n coordinates, some set of at least 2 ^ (n - 1) bit strings, half of the cube, is (n + 2)-rectangle-free.

At most 2 ^ (n + n K) rectangles with sides of size exactly K are spanned by K inputs, each with K ^ 2 points; for K = n + 2 at most a 2 ^ (-n - 4) fraction of all sets of bit strings contains one, while at least half of them have at least 2 ^ (n - 1) elements.

Sets of small bias

theorem Cslib.Circuits.Frontier.exists_rectangleBias {ι : Type u_1} [Fintype ι] {K : ℕ} {b : ℝ} (hb : 0 < b) (hK : ↑(Fintype.card ι) + 1 ≤ b ^ 2 * ↑K) : ∃ (S : Set (ι → Bool)), RectangleBias S K b

Sets of small bias exist. If n + 1 ≤ b ^ 2 K for n = |ι| and b > 0, some set of bit strings has density within b of 1/2 on every rectangle with both sides of size at least K.

A rectangle with sides of sizes k₁, k₂ ≥ K is spanned by k₁ + k₂ inputs, so there are at most 2 ^ (n + n k₁ + n k₂) of them, and by Hoeffding's inequality at most a 2 exp (-2 b ^ 2 k₁ k₂) ≤ 2 exp (-(n + 1) (k₁ + k₂)) fraction of all sets of bit strings has bias more than b on each. Summed over all sizes, this is less than one.

Families meeting the hypotheses of the frontier lower bounds

theorem Cslib.Circuits.Frontier.exists_rectangleFree_family : ∃ (S : (n : ℕ) → Set (Fin n → Bool)), (∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (S n) (n + 2)) ∧ ((fun (n : ℕ) => Real.log ↑(n + 2)) =o[Filter.atTop] fun (n : ℕ) => ↑n) ∧ ((fun (n : ℕ) => ↑n * Real.log ↑(Nat.card Bool) - Real.log ↑(S n).ncard) =o[Filter.atTop] fun (n : ℕ) => ↑n) ∧ ∀ (n : ℕ), 2 ^ (n - 1) ≤ (S n).ncard

The hypotheses of the worst-case frontier lower bounds can be met. There is a family of sets S_n ⊆ Bool^n that are (n + 2)-rectangle-free, with log (n + 2) = o(n) and n log 2 - log |S_n| = o(n): the hypotheses hfree, hK and hdense of CircuitLowerBound for the alphabet Bool and K_n = n + 2. Moreover |S_n| ≥ 2 ^ (n - 1).

theorem Cslib.Circuits.Frontier.exists_rectangleBias_family : ∃ (S : (n : ℕ) → Set (Fin n → Bool)), (∀ᶠ (n : ℕ) in Filter.atTop, RectangleBias (S n) ((n + 1) ^ 3) (1 / (↑n + 1))) ∧ ((fun (n : ℕ) => Real.log ↑((n + 1) ^ 3)) =o[Filter.atTop] fun (n : ℕ) => ↑n) ∧ Filter.Tendsto (fun (n : ℕ) => 1 / (↑n + 1)) Filter.atTop (nhds 0)

The hypotheses of the average-case frontier lower bounds can be met with bias tending to zero. There is a family of sets S_n ⊆ Bool^n with bias at most b_n = 1 / (n + 1) on every rectangle with both sides of size at least K_n = (n + 1) ^ 3, where log K_n = o(n) and b_n → 0: the hypotheses of AverageCaseBound for the alphabet Bool, with a conclusion that tends to 1/2.