Import Kahn-Kalai expectation-threshold theorem

LeanPool.lean

@@ -2054,6 +2054,13 @@ import LeanPool.JohnsonLindenstraussLean.QJLDistortion
 import LeanPool.JohnsonLindenstraussLean.Rotation
 import LeanPool.JohnsonLindenstraussLean.SquaredGaussian
 import LeanPool.JohnsonLindenstraussLean.Verify
+import LeanPool.KahnKalai
+import LeanPool.KahnKalai.Basic
+import LeanPool.KahnKalai.Cost
+import LeanPool.KahnKalai.Covering
+import LeanPool.KahnKalai.DoubleCount
+import LeanPool.KahnKalai.Numeric
+import LeanPool.KahnKalai.ParkPham
 import LeanPool.KaltonRoberts
 import LeanPool.KaltonRoberts.Collections
 import LeanPool.KaltonRoberts.Defs

LeanPool/KahnKalai.lean

@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2026 Dan Clemens Posch. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dan Clemens Posch
+-/
+
+import LeanPool.KahnKalai.ParkPham
+
+/-!
+# 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
+-/
+
+namespace KahnKalai
+
+/-- **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 covering_theorem {α : Type*} [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 α) ℓ) : ℝ) ≤
+      (((generate H).filter
+          (fun S => S.card = coveringLevel p (Fintype.card α) ℓ)).card : ℝ) :=
+  covering_aux ℓ H p hℓ hp0 hp1 hb hf
+
+/-- **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₂ ℓ`. -/
+theorem park_pham :
+    ∃ K : ℝ, 0 < K ∧
+      ∀ {α : Type} [DecidableEq α] [Fintype α]
+        (F : Finset (Finset α)) (ℓ : ℕ),
+        2 ≤ ℓ → IsBounded F ℓ →
+        threshold F ≤ K * expectationThreshold F * Real.logb 2 (ℓ : ℝ) :=
+  ⟨parkPhamK, parkPhamK_pos, park_pham_bound⟩
+
+end KahnKalai

LeanPool/KahnKalai/Basic.lean

@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2026 Dan Clemens Posch. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dan Clemens Posch
+-/
+import Mathlib.Analysis.SpecialFunctions.Log.Base
+
+/-!
+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).
+-/
+
+open Finset
+
+namespace KahnKalai
+
+variable {α : Type*} [DecidableEq α] [Fintype α]
+
+/-- The upward closure generated by a finite family of finite sets. -/
+def generate (F : Finset (Finset α)) : Finset (Finset α) :=
+  univ.filter fun T => ∃ S ∈ F, S ⊆ T
+
+/-- `G` covers `F` when every member of `F` contains a member of `G`. -/
+def Covers (G F : Finset (Finset α)) : Prop := F ⊆ generate G
+
+/-- The expectation polynomial of a finite family at parameter `p`. -/
+def expectation (p : ℝ) (G : Finset (Finset α)) : ℝ :=
+  ∑ S ∈ G, p ^ S.card
+
+/-- The infimum expectation among all covers of `H`. -/
+noncomputable def coverCost (p : ℝ) (H : Finset (Finset α)) : ℝ :=
+  sInf ((fun G : Finset (Finset α) => expectation p G) '' {G | Covers G H})
+
+/-- The `p`-biased product measure of a single finite set. -/
+def measure (p : ℝ) (S : Finset α) : ℝ :=
+  p ^ S.card * (1 - p) ^ (Fintype.card α - S.card)
+
+/-- The `p`-biased measure of a finite family of sets. -/
+def measureFamily (p : ℝ) (F : Finset (Finset α)) : ℝ :=
+  ∑ S ∈ F, measure p S
+
+/-- The least parameter where the upward closure of `F` has measure at least one half. -/
+noncomputable def threshold (F : Finset (Finset α)) : ℝ :=
+  sInf {p : ℝ | p ∈ Set.Icc 0 1 ∧ 1 / 2 ≤ measureFamily p (generate F)}
+
+/-- The largest parameter where the covering cost of `F` is at most one half. -/
+noncomputable def expectationThreshold (F : Finset (Finset α)) : ℝ :=
+  sSup {p : ℝ | p ∈ Set.Icc 0 1 ∧ coverCost p F ≤ 1 / 2}
+
+/-- A family is `ℓ`-bounded when each of its members has cardinality at most `ℓ`. -/
+def IsBounded (F : Finset (Finset α)) (ℓ : ℕ) : Prop :=
+  ∀ S ∈ F, S.card ≤ ℓ
+
+/-- The explicit constant in the formalized Tran–Vu covering theorem. -/
+def coveringConstant : ℝ := 1000
+
+/-- The level supplied by the quantitative covering theorem. -/
+noncomputable def coveringLevel (p : ℝ) (N ℓ : ℕ) : ℕ :=
+  ⌊coveringConstant * p * N * Real.logb 2 (ℓ + 1 : ℝ)⌋₊
+
+lemma mem_generate {F : Finset (Finset α)} {T : Finset α} :
+    T ∈ generate F ↔ ∃ S ∈ F, S ⊆ T := by
+  simp [generate]
+
+lemma subset_mem_generate {F : Finset (Finset α)} {S T : Finset α}
+    (hST : S ⊆ T) (hS : S ∈ generate F) : T ∈ generate F := by
+  rw [mem_generate] at hS ⊢
+  obtain ⟨U, hU, hUS⟩ := hS
+  exact ⟨U, hU, hUS.trans hST⟩
+
+lemma generate_mono {F G : Finset (Finset α)} (h : F ⊆ G) :
+    generate F ⊆ generate G := by
+  intro T hT
+  rw [mem_generate] at hT ⊢
+  obtain ⟨S, hS, hST⟩ := hT
+  exact ⟨S, h hS, hST⟩
+
+lemma covers_self (H : Finset (Finset α)) : Covers H H := by
+  intro T hT
+  exact mem_generate.mpr ⟨T, hT, Subset.rfl⟩
+
+omit [DecidableEq α] [Fintype α] in
+lemma expectation_nonneg {p : ℝ} (hp : 0 ≤ p) (G : Finset (Finset α)) :
+    0 ≤ expectation p G :=
+  sum_nonneg fun _ _ => pow_nonneg hp _
+
+lemma coverCost_nonneg {p : ℝ} (hp : 0 ≤ p) (H : Finset (Finset α)) :
+    0 ≤ coverCost p H := by
+  refine Real.sInf_nonneg fun x hx => ?_
+  obtain ⟨G, _, rfl⟩ := hx
+  exact expectation_nonneg hp G
+
+lemma coverCost_le_expectation {p : ℝ} (hp : 0 ≤ p) {G H : Finset (Finset α)}
+    (h : Covers G H) : coverCost p H ≤ expectation p G := by
+  refine csInf_le ?_ ⟨G, h, rfl⟩
+  exact ⟨0, fun x hx => by
+    obtain ⟨G', _, rfl⟩ := hx
+    exact expectation_nonneg hp G'⟩
+
+/-- Fact 2.1, integer form: an upset’s level sizes satisfy the shadow inequality. -/
+lemma generate_card_mono (F : Finset (Finset α)) (t : ℕ) :
+    #((generate F).filter (fun S => S.card = t)) * (Fintype.card α - t)
+      ≤ #((generate F).filter (fun S => S.card = t + 1)) * (t + 1) := by
+  classical
+  set N := Fintype.card α
+  set Ft := (generate F).filter (fun S => S.card = t)
+  set Ft1 := (generate F).filter (fun S => S.card = t + 1)
+  let Src := (A : ↥Ft) × ↥(univ \ A.1)
+  let Tgt := (B : ↥Ft1) × ↥B.1
+  have hx_not_mem : ∀ (A : ↥Ft) (x : ↥(univ \ A.1)), (x : α) ∉ (A : Finset α) := by
+    intro A x
+    exact (mem_sdiff.mp x.2).2
+  let f : Src → Tgt := fun ⟨A, x⟩ =>
+    ⟨⟨insert (x : α) (A : Finset α), by
+        have hA := A.2
+        have hAgen : (A : Finset α) ∈ generate F := (mem_filter.mp hA).1
+        have hAcard : (A : Finset α).card = t := (mem_filter.mp hA).2
+        refine mem_filter.mpr ⟨subset_mem_generate (subset_insert _ _) hAgen, ?_⟩
+        rw [card_insert_of_notMem (hx_not_mem A x), hAcard]⟩,
+      ⟨x, mem_insert_self _ _⟩⟩
+  have hf : Function.Injective f := by
+    intro a b h
+    rcases a with ⟨A, x⟩
+    rcases b with ⟨A', x'⟩
+    have hx : (x : α) = (x' : α) := congrArg (fun z : Tgt => (z.2 : α)) h
+    have hB :
+        insert (x : α) (A : Finset α) = insert (x' : α) (A' : Finset α) :=
+      congrArg (fun z : Tgt => (z.1 : Finset α)) h
+    have hxA' : (x : α) ∉ (A' : Finset α) := by
+      simpa [hx] using hx_not_mem A' x'
+    have hB' : insert (x : α) (A : Finset α) = insert (x : α) (A' : Finset α) := by
+      simpa [hx] using hB
+    have hAeq : (A : Finset α) = (A' : Finset α) :=
+      (erase_insert (hx_not_mem A x)).symm.trans <|
+        (congrArg (fun s : Finset α => s.erase (x : α)) hB').trans
+          (erase_insert hxA')
+    have hA' : A = A' := Subtype.ext hAeq
+    subst hA'
+    exact Sigma.ext rfl (heq_of_eq (Subtype.ext hx))
+  have hSrc : Fintype.card Src = #Ft * (N - t) := by
+    dsimp [Src]
+    rw [Fintype.card_sigma]
+    have hA : ∀ A : ↥Ft, Fintype.card ↥(univ \ A.1) = N - t := by
+      intro A
+      rw [Fintype.card_coe, card_sdiff_of_subset (subset_univ _), card_univ]
+      have : A.1.card = t := (mem_filter.mp A.2).2
+      rw [this]
+    simp_rw [hA]
+    simp [sum_const, Nat.mul_comm]
+  have hTgt : Fintype.card Tgt = #Ft1 * (t + 1) := by
+    dsimp [Tgt]
+    rw [Fintype.card_sigma]
+    have hB : ∀ B : ↥Ft1, Fintype.card ↥B.1 = t + 1 := by
+      intro B
+      have : B.1.card = t + 1 := (mem_filter.mp B.2).2
+      simpa [Fintype.card_coe] using this
+    simp_rw [hB]
+    simp [sum_const, Nat.mul_comm]
+  have : Fintype.card Src ≤ Fintype.card Tgt :=
+    Fintype.card_le_of_injective f hf
+  calc
+    #Ft * (N - t) = Fintype.card Src := hSrc.symm
+    _ ≤ Fintype.card Tgt := this
+    _ = #Ft1 * (t + 1) := hTgt
+
+/-- Fact 2.1: the fraction of an upset on level `t` is nondecreasing in `t`. -/
+lemma generate_level_frac_mono (F : Finset (Finset α)) (t : ℕ)
+    (ht : t < Fintype.card α) :
+    (((generate F).filter (fun S => S.card = t)).card : ℝ) /
+        ((Fintype.card α).choose t : ℝ) ≤
+      (((generate F).filter (fun S => S.card = t + 1)).card : ℝ) /
+        ((Fintype.card α).choose (t + 1) : ℝ) := by
+  set N := Fintype.card α
+  set a := #((generate F).filter (fun S => S.card = t))
+  set b := #((generate F).filter (fun S => S.card = t + 1))
+  have hch0 : 0 < (N.choose t : ℝ) := Nat.cast_pos.mpr (Nat.choose_pos ht.le)
+  have hch1 : 0 < (N.choose (t + 1) : ℝ) :=
+    Nat.cast_pos.mpr (Nat.choose_pos (Nat.succ_le_of_lt ht))
+  have hmul : a * N.choose (t + 1) ≤ b * N.choose t := by
+    have h0 : a * (N - t) ≤ b * (t + 1) := generate_card_mono F t
+    have hC : N.choose (t + 1) * (t + 1) = N.choose t * (N - t) :=
+      Nat.choose_succ_right_eq N t
+    have h5 : a * (N.choose (t + 1) * (t + 1)) ≤ b * (N.choose t * (t + 1)) := by
+      calc
+        a * (N.choose (t + 1) * (t + 1))
+            = a * (N.choose t * (N - t)) := by rw [hC]
+        _ = N.choose t * (a * (N - t)) := by ring
+        _ ≤ N.choose t * (b * (t + 1)) := Nat.mul_le_mul_left _ h0
+        _ = b * (N.choose t * (t + 1)) := by ring
+    have h6 : a * N.choose (t + 1) * (t + 1) ≤ b * N.choose t * (t + 1) := by
+      simpa [Nat.mul_assoc, Nat.mul_left_comm, Nat.mul_comm] using h5
+    exact Nat.le_of_mul_le_mul_right h6 (Nat.succ_pos t)
+  rw [div_le_div_iff₀ hch0 hch1]
+  exact_mod_cast hmul
+
+end KahnKalai