Tran–Vu Lemma 2.4 (double counting of large minimals G_W).

noncomputable def KahnKalai.coveringWidth (p : ℝ) (N : ℕ) : ℕ

w = ⌊0.1 L p N⌋.

Equations

• KahnKalai.coveringWidth p N = ⌊1 / 10 * KahnKalai.coveringConstant * p * ↑N⌋₊

theorem KahnKalai.coveringWidth_eq (p : ℝ) (N : ℕ) : coveringWidth p N = ⌊100 * p * ↑N⌋₊

theorem KahnKalai.choose_add_le (N w k : ℕ) : ↑(N.choose (w + k)) ≤ ↑(N.choose w) * (↑N / (↑w + 1)) ^ k

theorem KahnKalai.np_div_width_succ_le (p : ℝ) (N : ℕ) : ↑N * p / (↑(coveringWidth p N) + 1) ≤ 1 / 100

theorem KahnKalai.largeMinimals_disjoint {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W T : Finset α} {ℓ : ℕ} (h : T ∈ largeMinimals H W ℓ) : Disjoint T W

theorem KahnKalai.exists_mem_subset_union {α : Type u_1} [DecidableEq α] {H : Finset (Finset α)} {W' S₀ : Finset α} (h : S₀ ∈ restrictFamily H (W' \ S₀)) (hsub : S₀ ⊆ W') : ∃ S ∈ H, S ⊆ W' ∧ S₀ ⊆ S

theorem KahnKalai.subset_of_minimal_fiber {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W' S S' : Finset α} (hS' : S' ∈ minimals (restrictFamily H (W' \ S'))) (hS : S ∈ H) (hSW' : S ⊆ W') : S' ⊆ S

theorem KahnKalai.card_fiber_le {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ : ℕ} (hb : IsBounded H ℓ) (W' : Finset α) (k : ℕ) : {S' : Finset α | S'.card = k ∧ S' ⊆ W' ∧ S' ∈ largeMinimals H (W' \ S') ℓ}.card ≤ ℓ.choose k

noncomputable def KahnKalai.largePairs {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (ℓ w k : ℕ) : Finset (Finset α × Finset α)

Pairs of a width-w set and a size-k large minimal restricted member.

Equations

• KahnKalai.largePairs H ℓ w k = {W : Finset α | W.card = w}.biUnion fun (W : Finset α) => Finset.image (fun (S' : Finset α) => (W, S')) ({S' ∈ KahnKalai.largeMinimals H W ℓ | S'.card = k})

theorem KahnKalai.mem_largePairs {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ w k : ℕ} {p : Finset α × Finset α} : p ∈ largePairs H ℓ w k ↔ p.1.card = w ∧ p.2.card = k ∧ p.2 ∈ largeMinimals H p.1 ℓ

theorem KahnKalai.card_pairs_le {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ w k : ℕ} (hb : IsBounded H ℓ) : (largePairs H ℓ w k).card ≤ (Fintype.card α).choose (w + k) * ℓ.choose k

theorem KahnKalai.card_pairs_fst {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ w k : ℕ} {W : Finset α} (hW : W.card = w) : {p ∈ largePairs H ℓ w k | p.1 = W}.card = {S' ∈ largeMinimals H W ℓ | S'.card = k}.card

theorem KahnKalai.sum_card_large_eq_pairs {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (ℓ w k : ℕ) : ∑ W : Finset α with W.card = w, {S' ∈ largeMinimals H W ℓ | S'.card = k}.card = (largePairs H ℓ w k).card

theorem KahnKalai.expectation_eq_sum_level {α : Type u_1} {p : ℝ} (G : Finset (Finset α)) (ℓ : ℕ) (hb : IsBounded G ℓ) : expectation p G = ∑ k ∈ Finset.Icc 0 ℓ, p ^ k * ↑{S ∈ G | S.card = k}.card

theorem KahnKalai.sum_expectation_large {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (H : Finset (Finset α)) (ℓ : ℕ) (hb : IsBounded H ℓ) (w : ℕ) : ∑ W : Finset α with W.card = w, expectation p (largeMinimals H W ℓ) = ∑ k ∈ Finset.Icc 0 ℓ, p ^ k * ↑(largePairs H ℓ w k).card

theorem KahnKalai.largePairs_eq_empty_of_lt_kmin {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ w k : ℕ} (hk : k < kmin ℓ) : largePairs H ℓ w k = ∅

theorem KahnKalai.sum_expectation_large_tail {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (H : Finset (Finset α)) (ℓ : ℕ) (hb : IsBounded H ℓ) (w : ℕ) : ∑ W : Finset α with W.card = w, expectation p (largeMinimals H W ℓ) = ∑ k ∈ Finset.Icc (kmin ℓ) ℓ, p ^ k * ↑(largePairs H ℓ w k).card

theorem KahnKalai.double_counting_tail {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp0 : 0 ≤ p) (H : Finset (Finset α)) (ℓ : ℕ) (hb : IsBounded H ℓ) : ∑ W : Finset α with W.card = coveringWidth p (Fintype.card α), coverCost p (largeMinimals H W ℓ) ≤ ↑((Fintype.card α).choose (coveringWidth p (Fintype.card α))) * ∑ k ∈ Finset.Icc (kmin ℓ) ℓ, (1 / 100) ^ k * ↑(ℓ.choose k)

theorem KahnKalai.double_counting {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp0 : 0 ≤ p) (H : Finset (Finset α)) (ℓ : ℕ) (hb : IsBounded H ℓ) : ∑ W : Finset α with W.card = coveringWidth p (Fintype.card α), coverCost p (largeMinimals H W ℓ) ≤ ↑((Fintype.card α).choose (coveringWidth p (Fintype.card α))) * (1 / 100) ^ kmin ℓ * 2 ^ ℓ