Tran–Vu Theorem 2.3: the covering theorem.

theorem KahnKalai.frac_le_one (ℓ : ℕ) : 2 / 3 + 1 / 2 ^ (ℓ + 2) ≤ 1

theorem KahnKalai.covering_of_empty_mem {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ : ℕ} {p : ℝ} (h : ∅ ∈ H) : (2 / 3 + 1 / 2 ^ (ℓ + 2)) * ↑((Fintype.card α).choose (coveringLevel p (Fintype.card α) ℓ)) ≤ ↑{S ∈ generate H | S.card = coveringLevel p (Fintype.card α) ℓ}.card

theorem KahnKalai.covering_of_level_ge_card {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hf : 1 / 2 - 1 / 2 ^ (ℓ + 2) ≤ coverCost p H) (hm : Fintype.card α ≤ coveringLevel p (Fintype.card α) ℓ) : (2 / 3 + 1 / 2 ^ (ℓ + 2)) * ↑((Fintype.card α).choose (coveringLevel p (Fintype.card α) ℓ)) ≤ ↑{S ∈ generate H | S.card = coveringLevel p (Fintype.card α) ℓ}.card

theorem KahnKalai.ell1_lt {ℓ : ℕ} (hℓ : 1 ≤ ℓ) : ⌊9 / 10 * ↑ℓ⌋₊ < ℓ

theorem KahnKalai.coveringLevel_nonneg (p : ℝ) (N ℓ : ℕ) (hp0 : 0 ≤ p) : 0 ≤ coveringConstant * p * ↑N * Real.logb 2 (↑ℓ + 1)

theorem KahnKalai.floor_add_floor_le {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : ⌊a⌋₊ + ⌊b⌋₊ ≤ ⌊a + b⌋₊

theorem KahnKalai.log_ell1_add_le (ℓ : ℕ) (hℓ : 1 ≤ ℓ) : Real.logb 2 (↑⌊9 / 10 * ↑ℓ⌋₊ + 1) + 1 / 10 ≤ Real.logb 2 (↑ℓ + 1)

theorem KahnKalai.coveringLevel_lift {p : ℝ} {N w ℓ : ℕ} (hp0 : 0 ≤ p) (hℓ : 1 ≤ ℓ) (hw : w = coveringWidth p N) : coveringLevel p (N - w) ⌊9 / 10 * ↑ℓ⌋₊ + w ≤ coveringLevel p N ℓ

theorem KahnKalai.card_subtype_not_mem {α : Type u_1} [DecidableEq α] [Fintype α] (W : Finset α) : Fintype.card { x : α // x ∉ W } = Fintype.card α - W.card

def KahnKalai.toSub {α : Type u_1} [DecidableEq α] (W S : Finset α) : Finset { x : α // x ∉ W }

Regard the part of S outside W as a finset in the complementary subtype.

Equations

• KahnKalai.toSub W S = Finset.subtype (fun (x : α) => x ∉ W) S

def KahnKalai.ofSub {α : Type u_1} (W : Finset α) (T : Finset { x : α // x ∉ W }) : Finset α

Map a finset in the complement of W back to the ambient type.

Equations

• KahnKalai.ofSub W T = Finset.map { toFun := Subtype.val, inj' := ⋯ } T

theorem KahnKalai.ofSub_card {α : Type u_1} (W : Finset α) (T : Finset { x : α // x ∉ W }) : (ofSub W T).card = T.card

theorem KahnKalai.ofSub_toSub {α : Type u_1} [DecidableEq α] {W S : Finset α} (h : Disjoint S W) : ofSub W (toSub W S) = S

theorem KahnKalai.toSub_subset {α : Type u_1} [DecidableEq α] {W S T : Finset α} (h : S ⊆ T) : toSub W S ⊆ toSub W T

theorem KahnKalai.ofSub_subset {α : Type u_1} {W : Finset α} {T₁ T₂ : Finset { x : α // x ∉ W }} (h : T₁ ⊆ T₂) : ofSub W T₁ ⊆ ofSub W T₂

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

theorem KahnKalai.toSub_card {α : Type u_1} [DecidableEq α] {W S : Finset α} (h : Disjoint S W) : (toSub W S).card = S.card

theorem KahnKalai.coverCost_toSub {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp0 : 0 ≤ p) (F : Finset (Finset α)) (W : Finset α) (hF : ∀ S ∈ F, Disjoint S W) : coverCost p (Finset.image (toSub W) F) = coverCost p F

theorem KahnKalai.generate_union_mem {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W : Finset α} {ℓ : ℕ} {T : Finset { x : α // x ∉ W }} (hT : T ∈ generate (Finset.image (toSub W) (smallMinimals H W ℓ))) : ofSub W T ∪ W ∈ generate H

theorem KahnKalai.ofSub_union_card {α : Type u_1} [DecidableEq α] {W : Finset α} (T : Finset { x : α // x ∉ W }) : (ofSub W T ∪ W).card = T.card + W.card

theorem KahnKalai.coveringWidth_le_card {p : ℝ} {N ℓ : ℕ} (hp0 : 0 ≤ p) (hℓ : 1 ≤ ℓ) (hlev : ¬N ≤ coveringLevel p N ℓ) : coveringWidth p N ≤ N

theorem KahnKalai.floor_nine_tenths_le_card_sub_width {p : ℝ} {N ℓ : ℕ} (hp0 : 0 ≤ p) (hℓ : 1 ≤ ℓ) (hℓN : ℓ ≤ N) (hN : 1 ≤ N) (hlev : ¬N ≤ coveringLevel p N ℓ) : ⌊9 / 10 * ↑ℓ⌋₊ ≤ N - coveringWidth p N

theorem KahnKalai.geometric_tail_bound (ℓ : ℕ) (hℓ : 1 ≤ ℓ) : (∑ k ∈ Finset.Icc (kmin ℓ) ℓ, (1 / 100) ^ k * ↑(ℓ.choose k)) * 2 ^ (ℓ + 2) ≤ 12 / 11 * (1 / 2 ^ (ℓ + 2))

theorem KahnKalai.restricted_level_card_le {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W : Finset α} {ℓ k w : ℕ} (hWcard : W.card = w) : ↑{T ∈ generate (Finset.image (toSub W) (smallMinimals H W ℓ)) | T.card = k}.card ≤ ↑{S ∈ generate H | S.card = k + w ∧ W ⊆ S}.card

theorem KahnKalai.good_width_card_lower_bound {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {p : ℝ} {N w ℓ : ℕ} (hp0 : 0 ≤ p) (hb : IsBounded H ℓ) (hNcard : Fintype.card α = N) (hw : w = coveringWidth p N) : have Good := {W ∈ {W : Finset α | W.card = w} | coverCost p (largeMinimals H W ℓ) ≤ 1 / 2 ^ (ℓ + 2)}; ↑(N.choose w) * (1 - (∑ k ∈ Finset.Icc (kmin ℓ) ℓ, (1 / 100) ^ k * ↑(ℓ.choose k)) * 2 ^ (ℓ + 2)) ≤ ↑Good.card

theorem KahnKalai.good_level_of_induction {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W : Finset α} {p : ℝ} {N w ℓ ℓ₁ : ℕ} (hind : ∀ (H' : Finset (Finset { x : α // x ∉ W })) (p' : ℝ), ℓ₁ ≤ Fintype.card { x : α // x ∉ W } → 0 ≤ p' → p' ≤ 1 → IsBounded H' ℓ₁ → 1 / 2 - 1 / 2 ^ (ℓ₁ + 2) ≤ coverCost p' H' → (2 / 3 + 1 / 2 ^ (ℓ₁ + 2)) * ↑((Fintype.card { x : α // x ∉ W }).choose (coveringLevel p' (Fintype.card { x : α // x ∉ W }) ℓ₁)) ≤ ↑{S ∈ generate H' | S.card = coveringLevel p' (Fintype.card { x : α // x ∉ W }) ℓ₁}.card) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hℓ₁N : ℓ₁ ≤ N - w) (hℓ₁lt : ℓ₁ < ℓ) (hℓ₁ : ℓ₁ = ⌊9 / 10 * ↑ℓ⌋₊) (hf : 1 / 2 - 1 / 2 ^ (ℓ + 2) ≤ coverCost p H) (hNcard : Fintype.card α = N) (hWcard : W.card = w) (hgood : coverCost p (largeMinimals H W ℓ) ≤ 1 / 2 ^ (ℓ + 2)) : (2 / 3 + 1 / 2 ^ (ℓ₁ + 2)) * ↑((N - w).choose (coveringLevel p (N - w) ℓ₁)) ≤ ↑{T ∈ generate (Finset.image (toSub W) (smallMinimals H W ℓ)) | T.card = coveringLevel p (N - w) ℓ₁}.card

theorem KahnKalai.covering_aux (ℓ : ℕ) {α : Type u_2} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (p : ℝ) : ℓ ≤ Fintype.card α → 0 ≤ p → p ≤ 1 → IsBounded H ℓ → 1 / 2 - 1 / 2 ^ (ℓ + 2) ≤ coverCost p H → (2 / 3 + 1 / 2 ^ (ℓ + 2)) * ↑((Fintype.card α).choose (coveringLevel p (Fintype.card α) ℓ)) ≤ ↑{S ∈ generate H | S.card = coveringLevel p (Fintype.card α) ℓ}.card

Strong inductive form of Tran–Vu Theorem 2.3.