Cover-cost calculus for Tran–Vu: the infimum is a minimum, subadditivity, empty-family / empty-set evaluation, and ⊆-minimals.

theorem KahnKalai.generate_empty {α : Type u_1} [DecidableEq α] [Fintype α] : generate ∅ = ∅

theorem KahnKalai.generate_eq_univ_of_empty_mem {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} (h : ∅ ∈ F) : generate F = Finset.univ

theorem KahnKalai.expectation_empty {α : Type u_1} (p : ℝ) : expectation p ∅ = 0

theorem KahnKalai.expectation_singleton_empty {α : Type u_1} (p : ℝ) : expectation p {∅} = 1

theorem KahnKalai.expectation_mono {α : Type u_1} {p : ℝ} (hp : 0 ≤ p) {G₁ G₂ : Finset (Finset α)} (h : G₁ ⊆ G₂) : expectation p G₁ ≤ expectation p G₂

theorem KahnKalai.expectation_union_le {α : Type u_1} [DecidableEq α] {p : ℝ} (hp : 0 ≤ p) (G₁ G₂ : Finset (Finset α)) : expectation p (G₁ ∪ G₂) ≤ expectation p G₁ + expectation p G₂

theorem KahnKalai.covers_empty {α : Type u_1} [DecidableEq α] [Fintype α] (G : Finset (Finset α)) : Covers G ∅

theorem KahnKalai.covers_union {α : Type u_1} [DecidableEq α] [Fintype α] {G H₁ H₂ : Finset (Finset α)} (h₁ : Covers G H₁) (h₂ : Covers G H₂) : Covers G (H₁ ∪ H₂)

theorem KahnKalai.covers_union_covers {α : Type u_1} [DecidableEq α] [Fintype α] {G₁ G₂ H₁ H₂ : Finset (Finset α)} (h₁ : Covers G₁ H₁) (h₂ : Covers G₂ H₂) : Covers (G₁ ∪ G₂) (H₁ ∪ H₂)

theorem KahnKalai.covers_of_subset {α : Type u_1} [DecidableEq α] [Fintype α] {G H₁ H₂ : Finset (Finset α)} (hH : H₁ ⊆ H₂) (h : Covers G H₂) : Covers G H₁

theorem KahnKalai.covers_singleton_empty {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) : Covers {∅} H

theorem KahnKalai.coverCost_le_one {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (H : Finset (Finset α)) : coverCost p H ≤ 1

theorem KahnKalai.covers_set_nonempty {α : Type u_1} [DecidableEq α] [Fintype α] (p : ℝ) (H : Finset (Finset α)) : ((fun (G : Finset (Finset α)) => expectation p G) '' {G : Finset (Finset α) | Covers G H}).Nonempty

theorem KahnKalai.covers_set_finite {α : Type u_1} [DecidableEq α] [Fintype α] (p : ℝ) (H : Finset (Finset α)) : ((fun (G : Finset (Finset α)) => expectation p G) '' {G : Finset (Finset α) | Covers G H}).Finite

theorem KahnKalai.exists_cover_eq_coverCost {α : Type u_1} [DecidableEq α] [Fintype α] (p : ℝ) (H : Finset (Finset α)) : ∃ (G : Finset (Finset α)), Covers G H ∧ expectation p G = coverCost p H

theorem KahnKalai.coverCost_empty {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) : coverCost p ∅ = 0

theorem KahnKalai.coverCost_eq_zero_of_empty {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) {H : Finset (Finset α)} (hH : H = ∅) : coverCost p H = 0

theorem KahnKalai.coverCost_pos_imp_nonempty {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) {H : Finset (Finset α)} (h : 0 < coverCost p H) : H.Nonempty

theorem KahnKalai.coverCost_of_mem_empty {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) {H : Finset (Finset α)} (h : ∅ ∈ H) : coverCost p H = 1

theorem KahnKalai.coverCost_mono {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) {H₁ H₂ : Finset (Finset α)} (h : H₁ ⊆ H₂) : coverCost p H₁ ≤ coverCost p H₂

theorem KahnKalai.coverCost_union_le {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (H₁ H₂ : Finset (Finset α)) : coverCost p (H₁ ∪ H₂) ≤ coverCost p H₁ + coverCost p H₂

theorem KahnKalai.coverCost_sdiff_ge {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (H₁ H₂ : Finset (Finset α)) : coverCost p H₁ - coverCost p H₂ ≤ coverCost p (H₁ \ H₂)

theorem KahnKalai.coverCost_union_ge_sub {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (A B : Finset (Finset α)) : coverCost p A - coverCost p B ≤ coverCost p (A ∪ B) - coverCost p B

theorem KahnKalai.coverCost_ge_union_sub {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (A B : Finset (Finset α)) : coverCost p (A ∪ B) - coverCost p B ≤ coverCost p A

Subadditivity rearranged: f(A) ≥ f(A ∪ B) - f(B).

def KahnKalai.minimals {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) : Finset (Finset α)

The inclusion-minimal members of a finite family.

Equations

• KahnKalai.minimals F = {T ∈ F | ∀ U ∈ F, U ⊆ T → U = T}

theorem KahnKalai.minimals_subset {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) : minimals F ⊆ F

theorem KahnKalai.mem_minimals {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {T : Finset α} : T ∈ minimals F ↔ T ∈ F ∧ ∀ U ∈ F, U ⊆ T → U = T

theorem KahnKalai.exists_minimal_subset {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {S : Finset α} (hS : S ∈ F) : ∃ T ∈ minimals F, T ⊆ S

theorem KahnKalai.covers_minimals {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) : Covers (minimals F) F

theorem KahnKalai.covers_of_covers_minimals {α : Type u_1} [DecidableEq α] [Fintype α] {G F : Finset (Finset α)} (h : Covers G (minimals F)) : Covers G F

theorem KahnKalai.coverCost_minimals {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (F : Finset (Finset α)) : coverCost p (minimals F) = coverCost p F

def KahnKalai.restrictFamily {α : Type u_1} [DecidableEq α] (H : Finset (Finset α)) (W : Finset α) : Finset (Finset α)

Restrict a family by removing every element of W from each member.

Equations

• KahnKalai.restrictFamily H W = Finset.image (fun (S : Finset α) => S \ W) H

theorem KahnKalai.mem_restrictFamily {α : Type u_1} [DecidableEq α] {H : Finset (Finset α)} {W T : Finset α} : T ∈ restrictFamily H W ↔ ∃ S ∈ H, S \ W = T

theorem KahnKalai.restrictFamily_disjoint {α : Type u_1} [DecidableEq α] {H : Finset (Finset α)} {W T : Finset α} (h : T ∈ restrictFamily H W) : Disjoint T W

theorem KahnKalai.restrictFamily_subset_sdiff {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W T : Finset α} (h : T ∈ restrictFamily H W) : T ⊆ Finset.univ \ W

theorem KahnKalai.covers_restrict_of_covers {α : Type u_1} [DecidableEq α] [Fintype α] {G H : Finset (Finset α)} {W : Finset α} (h : Covers G (restrictFamily H W)) : Covers G H

theorem KahnKalai.coverCost_le_restrict {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (H : Finset (Finset α)) (W : Finset α) : coverCost p H ≤ coverCost p (restrictFamily H W)

theorem KahnKalai.coverCost_le_minimals_restrict {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (H : Finset (Finset α)) (W : Finset α) : coverCost p H ≤ coverCost p (minimals (restrictFamily H W))

noncomputable def KahnKalai.largeMinimals {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (W : Finset α) (ℓ : ℕ) : Finset (Finset α)

Members of F with size strictly larger than 0.9 ℓ.

Equations

• KahnKalai.largeMinimals H W ℓ = {T ∈ KahnKalai.minimals (KahnKalai.restrictFamily H W) | ⌊9 / 10 * ↑ℓ⌋₊ + 1 ≤ T.card}

noncomputable def KahnKalai.smallMinimals {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (W : Finset α) (ℓ : ℕ) : Finset (Finset α)

Minimal restricted members whose size is at most 0.9 ℓ.

Equations

• KahnKalai.smallMinimals H W ℓ = {T ∈ KahnKalai.minimals (KahnKalai.restrictFamily H W) | T.card ≤ ⌊9 / 10 * ↑ℓ⌋₊}

theorem KahnKalai.largeMinimals_union_small {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (W : Finset α) (ℓ : ℕ) : largeMinimals H W ℓ ∪ smallMinimals H W ℓ = minimals (restrictFamily H W)

theorem KahnKalai.largeMinimals_disjoint_small {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (W : Finset α) (ℓ : ℕ) : Disjoint (largeMinimals H W ℓ) (smallMinimals H W ℓ)

theorem KahnKalai.coverCost_small_ge {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) (H : Finset (Finset α)) (W : Finset α) (ℓ : ℕ) : coverCost p (minimals (restrictFamily H W)) - coverCost p (largeMinimals H W ℓ) ≤ coverCost p (smallMinimals H W ℓ)

theorem KahnKalai.IsBounded.image_sdiff {α : Type u_1} [DecidableEq α] {H : Finset (Finset α)} {ℓ : ℕ} (hb : IsBounded H ℓ) (W : Finset α) : IsBounded (restrictFamily H W) ℓ

theorem KahnKalai.IsBounded.minimals {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {ℓ : ℕ} (hb : IsBounded F ℓ) : IsBounded (KahnKalai.minimals F) ℓ

theorem KahnKalai.IsBounded.largeMinimals {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {ℓ : ℕ} (hb : IsBounded H ℓ) (W : Finset α) : IsBounded (KahnKalai.largeMinimals H W ℓ) ℓ

theorem KahnKalai.IsBounded.smallMinimals {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W : Finset α} {ℓ ℓ₁ : ℕ} (hℓ₁ : ℓ₁ = ⌊9 / 10 * ↑ℓ⌋₊) : IsBounded (KahnKalai.smallMinimals H W ℓ) ℓ₁

theorem KahnKalai.largeMinimals_card_gt {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} {W T : Finset α} {ℓ : ℕ} (h : T ∈ largeMinimals H W ℓ) : ⌊9 / 10 * ↑ℓ⌋₊ + 1 ≤ T.card

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

theorem KahnKalai.filter_card_eq_powersetCard {α : Type u_1} [Fintype α] (n : ℕ) : {S : Finset α | S.card = n} = Finset.powersetCard n Finset.univ

theorem KahnKalai.card_level {α : Type u_1} [Fintype α] (n : ℕ) : {S : Finset α | S.card = n}.card = (Fintype.card α).choose n

theorem KahnKalai.generate_level_frac_le {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) {s t : ℕ} (hst : s ≤ t) (ht : t ≤ Fintype.card α) : ↑{S ∈ generate F | S.card = s}.card / ↑((Fintype.card α).choose s) ≤ ↑{S ∈ generate F | S.card = t}.card / ↑((Fintype.card α).choose t)

theorem KahnKalai.expectation_mono_p {α : Type u_1} {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) (G : Finset (Finset α)) : expectation p G ≤ expectation q G

theorem KahnKalai.coverCost_mono_p {α : Type u_1} [DecidableEq α] [Fintype α] {p q : ℝ} (hp : 0 ≤ p) (hpq : p ≤ q) (H : Finset (Finset α)) : coverCost p H ≤ coverCost q H

theorem KahnKalai.expectation_zero {α : Type u_1} [DecidableEq α] (G : Finset (Finset α)) : expectation 0 G = if ∅ ∈ G then 1 else 0

theorem KahnKalai.coverCost_zero_of_not_mem_empty {α : Type u_1} [DecidableEq α] [Fintype α] {H : Finset (Finset α)} (h : ∅ ∉ H) : coverCost 0 H = 0