Tran–Vu Remark 2.5: binomial mixture of level fractions plus a 2^{-X} Markov tail, yielding Park–Pham from the covering theorem.

def KahnKalai.parkPhamK : ℝ

The explicit constant in the formalized Park–Pham threshold bound.

Equations

• KahnKalai.parkPhamK = 100000

theorem KahnKalai.parkPhamK_pos : 0 < parkPhamK

theorem KahnKalai.parkPhamK_ge_two : 2 ≤ parkPhamK

theorem KahnKalai.logb_two_ell_ge_one {ℓ : ℕ} (hℓ : 2 ≤ ℓ) : 1 ≤ Real.logb 2 ↑ℓ

theorem KahnKalai.ell_add_one_le_sq {ℓ : ℕ} (hℓ : 2 ≤ ℓ) : ℓ + 1 ≤ ℓ ^ 2

theorem KahnKalai.logb_ell_add_one_le_two {ℓ : ℕ} (hℓ : 2 ≤ ℓ) : Real.logb 2 (↑ℓ + 1) ≤ 2 * Real.logb 2 ↑ℓ

theorem KahnKalai.logb_min_add_one_le {ℓ N : ℕ} (hℓ : 2 ≤ ℓ) : Real.logb 2 (↑(min ℓ N) + 1) ≤ 2 * Real.logb 2 ↑ℓ

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

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

def KahnKalai.binomProb (N : ℕ) (p : ℝ) (k : ℕ) : ℝ

Binomial point mass C(N,k) p^k (1-p)^{N-k}.

Equations

• KahnKalai.binomProb N p k = ↑(N.choose k) * p ^ k * (1 - p) ^ (N - k)

theorem KahnKalai.binomProb_nonneg {N : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (k : ℕ) : 0 ≤ binomProb N p k

theorem KahnKalai.binom_sum (N : ℕ) (p : ℝ) : ∑ k ∈ Finset.range (N + 1), binomProb N p k = (p + (1 - p)) ^ N

theorem KahnKalai.binom_sum_one (N : ℕ) (p : ℝ) : ∑ k ∈ Finset.range (N + 1), binomProb N p k = 1

theorem KahnKalai.binom_mgf_half (N : ℕ) (p : ℝ) : ∑ k ∈ Finset.range (N + 1), (1 / 2) ^ k * binomProb N p k = (1 - p / 2) ^ N

theorem KahnKalai.binom_left_tail (N m : ℕ) {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hm : m ≤ N) : ∑ k ∈ Finset.range m, binomProb N p k ≤ 2 ^ m * (1 - p / 2) ^ N

theorem KahnKalai.one_sub_half_p_le_exp {p : ℝ} : 1 - p / 2 ≤ Real.exp (-(p / 2))

theorem KahnKalai.two_pow_le_exp (m : ℕ) : 2 ^ m ≤ Real.exp ↑m

theorem KahnKalai.exp_neg_four_le_one_div_five : Real.exp (-4) ≤ 1 / 5

theorem KahnKalai.binom_left_tail_of_mean {N m : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hmN : m ≤ N) (hmμ : ↑m ≤ ↑N * p / 4) (hμ : 16 ≤ ↑N * p) : ∑ k ∈ Finset.range m, binomProb N p k ≤ 1 / 5

theorem KahnKalai.measure_one {α : Type u_1} [DecidableEq α] [Fintype α] (S : Finset α) : measure 1 S = if S = Finset.univ then 1 else 0

theorem KahnKalai.measureFamily_one {α : Type u_1} [DecidableEq α] [Fintype α] (G : Finset (Finset α)) : measureFamily 1 G = if Finset.univ ∈ G then 1 else 0

theorem KahnKalai.measureFamily_univ {α : Type u_1} [Fintype α] (p : ℝ) : measureFamily p Finset.univ = (p + (1 - p)) ^ Fintype.card α

theorem KahnKalai.measureFamily_univ_one {α : Type u_1} [Fintype α] {p : ℝ} : measureFamily p Finset.univ = 1

theorem KahnKalai.measureFamily_generate_eq {α : Type u_1} [DecidableEq α] [Fintype α] (p : ℝ) (F : Finset (Finset α)) : measureFamily p (generate F) = ∑ k ∈ Finset.range (Fintype.card α + 1), ↑{S ∈ generate F | S.card = k}.card * p ^ k * (1 - p) ^ (Fintype.card α - k)

theorem KahnKalai.threshold_le_of_measure {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {p : ℝ} (hp : p ∈ Set.Icc 0 1) (h : 1 / 2 ≤ measureFamily p (generate F)) : threshold F ≤ p

theorem KahnKalai.threshold_le_one_of_nonempty {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} (hF : F.Nonempty) : threshold F ≤ 1

theorem KahnKalai.threshold_eq_zero_of_empty_mem {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} (h : ∅ ∈ F) : threshold F = 0

theorem KahnKalai.threshold_eq_zero_of_empty {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} (hF : F = ∅) : threshold F = 0

theorem KahnKalai.expectationThreshold_nonneg {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) : 0 ≤ expectationThreshold F

theorem KahnKalai.expectationThreshold_le_one {α : Type u_1} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) : expectationThreshold F ≤ 1

theorem KahnKalai.coverCost_gt_half_of_gt_q {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {p : ℝ} (hp : p ∈ Set.Icc 0 1) (h : expectationThreshold F < p) : 1 / 2 < coverCost p F

theorem KahnKalai.empty_mem_of_q_eq_zero {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} (h : expectationThreshold F = 0) : ∅ ∈ F

theorem KahnKalai.sdiff_range_binom (N m : ℕ) (p : ℝ) (hm : m ≤ N) : ∑ k ∈ Finset.range (N + 1) \ Finset.range m, binomProb N p k = 1 - ∑ k ∈ Finset.range m, binomProb N p k

theorem KahnKalai.measureFamily_ge_occupation {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {p : ℝ} {m : ℕ} {α0 : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hm : m ≤ Fintype.card α) (hocc : α0 * ↑((Fintype.card α).choose m) ≤ ↑{S ∈ generate F | S.card = m}.card) : α0 * ∑ k ∈ Finset.range (Fintype.card α + 1) \ Finset.range m, binomProb (Fintype.card α) p k ≤ measureFamily p (generate F)

theorem KahnKalai.threshold_le_parkPham_of_level_gt_card {α : Type u_1} [DecidableEq α] [Fintype α] {F : Finset (Finset α)} {ℓ ℓ' N m : ℕ} {q p : ℝ} (hq0 : 0 ≤ q) (hlog : 1 ≤ Real.logb 2 ↑ℓ) (hlog' : Real.logb 2 (↑ℓ' + 1) ≤ 2 * Real.logb 2 ↑ℓ) (hp : p = 2 * q) (hmle : ↑m ≤ 1000 * p * ↑N * Real.logb 2 (↑ℓ' + 1)) (hmN : N < m) (hth1 : threshold F ≤ 1) : threshold F ≤ parkPhamK * q * Real.logb 2 ↑ℓ

theorem KahnKalai.park_pham_bound {α : Type} [DecidableEq α] [Fintype α] (F : Finset (Finset α)) (ℓ : ℕ) (hℓ : 2 ≤ ℓ) (_hb : IsBounded F ℓ) : threshold F ≤ parkPhamK * expectationThreshold F * Real.logb 2 ↑ℓ

Explicit Park–Pham bound.