Kahn–Kalai expectation-threshold theorem

Source: arxiv:2303.02144, doi:10.37236/12266, url:https://github.com/dcposch/kahn-kalai-lean Authors: Dan Clemens Posch Status: verified Main declarations: KahnKalai.covering_theorem, KahnKalai.park_pham Tags: probabilistic-combinatorics, random-structures, threshold-phenomena, set-systems MSC: 05C80, 60C05

theorem KahnKalai.covering_theorem {α : Type u_1} [DecidableEq α] [Fintype α] (H : Finset (Finset α)) (ℓ : ℕ) (p : ℝ) (hℓ : ℓ ≤ Fintype.card α) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hb : IsBounded H ℓ) (hf : 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

Tran–Vu, Theorem 2.3. If ℓ is at most the ground-set cardinality, p ∈ [0, 1], H is ℓ-bounded, and f(H) ≥ 1/2 - 2^{-(ℓ+2)}, then the cardinality of ⟨H⟩ at the selected level m_ℓ is at least (2/3 + 2^{-(ℓ+2)}) * choose(N, m_ℓ). When m_ℓ ≤ N, this is the corresponding level-density bound; when N < m_ℓ, both cardinalities vanish.

theorem KahnKalai.park_pham : ∃ (K : ℝ), 0 < K ∧ ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Fintype α] (F : Finset (Finset α)) (ℓ : ℕ), 2 ≤ ℓ → IsBounded F ℓ → threshold F ≤ K * expectationThreshold F * Real.logb 2 ↑ℓ

Park–Pham / Kahn–Kalai (Tran–Vu, Theorem 1.1). There is an absolute constant K such that every ℓ-bounded family with ℓ ≥ 2 satisfies p_c(F) ≤ K q(F) log₂ ℓ.