Simultaneous deficits across a hypergraph cut

For a family of supports of size at most d, a uniformly random set meets each support with probability at most 1 - 2⁻ᵈ. If each coordinate occurs in at most D supports, changing one coordinate changes the number of selected coordinates minus the number of supports met by at most D + 1. The Boolean Poincaré inequality therefore controls the variance of this deficit.

If every cut has a side whose deficit is below k, symmetry between a cut and its complement forces the mean deficit below k + (D + 1) √(|ι| / 2).

Main results

• Cslib.HypergraphCut.card_le_of_deficit: a finite support-sensitive bound from a deficit obstruction on every cut.
• Cslib.HypergraphCut.card_lt_of_deficit_chain: a chain whose cuts cross few supports gives a bound without a concentration error.

References

The cut bound applies the Boolean Poincaré inequality O'Donnell, Section 2.3.

theorem Cslib.HypergraphCut.card_le_of_deficit {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] (S : κ → Finset ι) {d D : ℕ} {k : ℝ} (hd : ∀ (j : κ), (S j).card ≤ d) (hD : ∀ (i : ι), {j : κ | i ∈ S j}.card ≤ D) (hcut : ∀ (U : Finset ι), ↑U.card - ↑{j : κ | ¬Disjoint (S j) U}.card < k ∨ ↑Uᶜ.card - ↑{j : κ | ¬Disjoint (S j) Uᶜ}.card < k) : ↑(Fintype.card ι) / 2 ≤ (1 - (1 / 2) ^ d) * ↑(Fintype.card κ) + k + (↑D + 1) * √(↑(Fintype.card ι) / 2)

If every cut of a finite support family has a side whose number of coordinates exceeds the number of supports it meets by less than k, then the family must be large. Supports have size at most d, and every coordinate belongs to at most D supports.

theorem Cslib.HypergraphCut.card_lt_of_deficit_chain {ι : Type u_1} {κ : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype κ] (S : κ → Finset ι) (U : ℕ → Finset ι) {m W k : ℕ} (hzero : U 0 = ∅) (hlast : U m = Finset.univ) (hstep : ∀ t < m, U t ⊆ U (t + 1)) (hcard : ∀ t < m, (U (t + 1)).card ≤ (U t).card + 1) (hcross : ∀ t ≤ m, {j : κ | ¬Disjoint (S j) (U t) ∧ ¬Disjoint (S j) (U t)ᶜ}.card ≤ W) (hcut : ∀ (V : Finset ι), V.card < {j : κ | ¬Disjoint (S j) V}.card + k ∨ Vᶜ.card < {j : κ | ¬Disjoint (S j) Vᶜ}.card + k) : Fintype.card ι < Fintype.card κ + W + 2 * k

If a chain from the empty set to the whole coordinate set adds at most one coordinate per step and crosses at most W supports at each cut, then a cut-deficit obstruction forces |ι| < |κ| + W + 2 k. The first cut with deficit at least k has deficit exactly k; counting supports on both sides then bounds the complementary deficit.