Foundational lemmas for the Tran–Vu covering argument: upset calculus, cover cost as an attained infimum, and Fact 2.1 (level fractions of an upset are nondecreasing).

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

The upward closure generated by a finite family of finite sets.

Equations

• KahnKalai.generate F = {T : Finset α | ∃ S ∈ F, S ⊆ T}

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

G covers F when every member of F contains a member of G.

Equations

• KahnKalai.Covers G F = (F ⊆ KahnKalai.generate G)

def KahnKalai.expectation {α : Type u_1} (p : ℝ) (G : Finset (Finset α)) : ℝ

The expectation polynomial of a finite family at parameter p.

Equations

• KahnKalai.expectation p G = ∑ S ∈ G, p ^ S.card

noncomputable def KahnKalai.coverCost {α : Type u_1} [DecidableEq α] [Fintype α] (p : ℝ) (H : Finset (Finset α)) : ℝ

The infimum expectation among all covers of H.

Equations

• KahnKalai.coverCost p H = sInf ((fun (G : Finset (Finset α)) => KahnKalai.expectation p G) '' {G : Finset (Finset α) | KahnKalai.Covers G H})

def KahnKalai.measure {α : Type u_1} [Fintype α] (p : ℝ) (S : Finset α) : ℝ

The p-biased product measure of a single finite set.

Equations

• KahnKalai.measure p S = p ^ S.card * (1 - p) ^ (Fintype.card α - S.card)

def KahnKalai.measureFamily {α : Type u_1} [Fintype α] (p : ℝ) (F : Finset (Finset α)) : ℝ

The p-biased measure of a finite family of sets.

Equations

• KahnKalai.measureFamily p F = ∑ S ∈ F, KahnKalai.measure p S

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

The least parameter where the upward closure of F has measure at least one half.

Equations

• KahnKalai.threshold F = sInf {p : ℝ | p ∈ Set.Icc 0 1 ∧ 1 / 2 ≤ KahnKalai.measureFamily p (KahnKalai.generate F)}

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

The largest parameter where the covering cost of F is at most one half.

Equations

• KahnKalai.expectationThreshold F = sSup {p : ℝ | p ∈ Set.Icc 0 1 ∧ KahnKalai.coverCost p F ≤ 1 / 2}

def KahnKalai.IsBounded {α : Type u_1} (F : Finset (Finset α)) (ℓ : ℕ) : Prop

A family is ℓ-bounded when each of its members has cardinality at most ℓ.

Equations

• KahnKalai.IsBounded F ℓ = ∀ S ∈ F, S.card ≤ ℓ

def KahnKalai.coveringConstant : ℝ

The explicit constant in the formalized Tran–Vu covering theorem.

Equations

• KahnKalai.coveringConstant = 1000

noncomputable def KahnKalai.coveringLevel (p : ℝ) (N ℓ : ℕ) : ℕ

The level supplied by the quantitative covering theorem.

Equations

• KahnKalai.coveringLevel p N ℓ = ⌊KahnKalai.coveringConstant * p * ↑N * Real.logb 2 (↑ℓ + 1)⌋₊

theorem KahnKalai.mem_generate {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {T : Finset α} : T ∈ generate F ↔ ∃ S ∈ F, S ⊆ T

theorem KahnKalai.subset_mem_generate {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {S T : Finset α} (hST : S ⊆ T) (hS : S ∈ generate F) : T ∈ generate F

theorem KahnKalai.generate_mono {α : Type u_1} [DecidableEq α] [Fintype α] {F G : Finset (Finset α)} (h : F ⊆ G) : generate F ⊆ generate G

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

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

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

theorem KahnKalai.coverCost_le_expectation {α : Type u_1} [DecidableEq α] [Fintype α] {p : ℝ} (hp : 0 ≤ p) {G H : Finset (Finset α)} (h : Covers G H) : coverCost p H ≤ expectation p G

theorem KahnKalai.generate_card_mono {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) (t : ℕ) : {S ∈ generate F | S.card = t}.card * (Fintype.card α - t) ≤ {S ∈ generate F | S.card = t + 1}.card * (t + 1)

Fact 2.1, integer form: an upset’s level sizes satisfy the shadow inequality.

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

Fact 2.1: the fraction of an upset on level t is nondecreasing in t.