Optimal monotone families for the discrete isoperimetric inequality

References:

• mathoverflow/10799 asked by user Gil Kalai
• Optimal Monotone Families for the Discrete Isoperimetric Inequality by Gil Kalai (2026), a Polymath project with AI agents
• An Isoperimetric Inequality for the Hamming Cube and Integrality Gaps in Bounded-Degree Graphs by Jeff Kahn and Gil Kalai (2006)
• A Proof of the Kahn–Kalai Conjecture by Jinyoung Park and Huy Tuan Pham (2022)

noncomputable def Mathoverflow10799.μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ

Start with a set $X=\{1,2,...,n\}$ of $n$ elements and the family $2^X$ of all subsets of $X$. For a real number $p$ between zero and one, we consider a probability distribution $\mu_p$ on $2^X$ where the probability that $i \in S$ is $p$, independently for different $i$'s. Thus for $p=1/2$ we get the uniform probability distribution.

For $S \subseteq \{0, \ldots, n-1\}$, its probability is $p^{|S|} (1-p)^{n - |S|}$.

Equations

• Mathoverflow10799.μ p S = p ^ S.card * (1 - p) ^ (n - S.card)

theorem Mathoverflow10799.μ_half_eq_uniform {n : ℕ} (S : Finset (Fin n)) : μ (1 / 2) S = (1 / 2) ^ n

For $p = 1/2$, the $p$-biased measure is the uniform distribution: $\mu_{1/2}(S) = (1/2)^n$ for every $S \subseteq [n]$.

noncomputable def Mathoverflow10799.μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ

The $p$-biased measure of a family $\mathcal F \subseteq 2^{[n]}$, i.e. $\mu_p(\mathcal F) = \sum_{S \in \mathcal F} \mu_p(S)$.

Equations

• Mathoverflow10799.μFamily p F = ∑ S ∈ F, Mathoverflow10799.μ p S

def Mathoverflow10799.boundaryCount (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : ℕ

Given a family $F$, for a subset $S$ of $X$, we write $h(S)$ as the number of subsets $T$ in $X$ such that (1) $T$ differs from $S$ in exactly one element (2) Exactly one set among $S$ and $T$ belongs to $F$.

Equations

• Mathoverflow10799.boundaryCount n F S = {i : Fin n | Xor' (S ∈ F) (symmDiff S {i} ∈ F)}.card

theorem Mathoverflow10799.boundaryCount_equiv (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : boundaryCount n F S = {T : Finset (Fin n) | (symmDiff S T).card = 1 ∧ Xor' (S ∈ F) (T ∈ F)}.card

Test lemma showing that boundaryCount is equivalent to counting subsets $T$ that differ from $S$ in exactly one element and exactly one of $S, T$ belongs to $F$.

noncomputable def Mathoverflow10799.edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ

The edge-boundary of $F$ is the expectation of $h(S)$ (according to $\mu_p$) over all subsets $S$ of $X$. It is denoted by $I^p(F)$.

Equations

• Mathoverflow10799.edgeBoundary n p F = ∑ S : Finset (Fin n), Mathoverflow10799.μ p S * ↑(Mathoverflow10799.boundaryCount n F S)

@[reducible, inline]

abbrev Mathoverflow10799.IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop

A family $F$ of subsets of $2^X$ is monotone increasing if when $S$ belongs to $F$ and $T$ contains $S$ then $T$ also belongs to $F$. (Monotone increasing families also also called "filtes" and "up-families".) From now on we will restrict our attention to the case of monotone increasing families.

This is Mathlib's IsUpperSet applied to the coercion of $\mathcal F$ to a set, using the fact that ≤ on Finset is ⊆.

Equations

• Mathoverflow10799.IsMonotoneIncreasing F = IsUpperSet ↑F

noncomputable def Mathoverflow10799.IsOptimal {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : Prop

We say that a family is optimal for $\mu_p$ if the isoperimetric inequality (IR) is sharp up to a multiplicative constant $1000 \log (1/p)$.

Since the lower bound from (IR) is $$\frac{\mu_p(\mathcal F) \cdot \log(1/\mu_p(\mathcal F))}{p \cdot \log(1/p)},$$ multiplying by $1000 \log(1/p)$ gives the condition $$I^p(\mathcal F) \le \frac{1000}{p} \cdot \mu_p(\mathcal F) \cdot \log \frac{1}{\mu_p(\mathcal F)}.$$

Equations

• Mathoverflow10799.IsOptimal p F = (Mathoverflow10799.edgeBoundary n p F ≤ 1000 * Real.log (1 / p) * (Mathoverflow10799.μFamily p F * Real.logb p (Mathoverflow10799.μFamily p F) / p))

theorem Mathoverflow10799.mathoverflow_10799 : False ↔ ∀ (n : ℕ), 2 ≤ n → ∀ (F : Finset (Finset (Fin n))), IsMonotoneIncreasing F → ∀ (s t : ℝ), 0 < s → s ≤ t → t < 1 → t / s > 1000 * Real.log ↑n → ∃ (p : ℝ), s ≤ p ∧ p ≤ t ∧ IsOptimal p F

Problem: For every monotone increasing family $F$, given an interval $[s,t]$ of real numbers so that $t/s > 1000 \log n$ we have some $p$ in the interval $[s,t]$ so that $F$ is optimal with respect to $\mu_p$.

This was a "missing lemma" in the work of Kahn and Kalai on threshold behavior of monotone properties. The related Kahn–Kalai conjecture was settled by Park and Pham.

This conjecture is false without the additional assumption $\mu_t(F) = 1/2$. A counterexample was found by Shlomo Perles (April 7, 2026).

theorem Mathoverflow10799.mathoverflow_10799.variants.kahn_kalai_conjecture_7 : True ↔ ∀ (n : ℕ), 2 ≤ n → ∀ (F : Finset (Finset (Fin n))), IsMonotoneIncreasing F → ∀ (s t : ℝ), 0 < s → s ≤ t → t < 1 → μFamily t F = 1 / 2 → t / s > 1000 * Real.log ↑n → ∃ (p : ℝ), s ≤ p ∧ p ≤ t ∧ IsOptimal p F

Conjecture 7 from Kahn–Kalai 2006: the same statement as the original conjecture, but with the additional assumption that $t$ is the critical probability for $F$, namely $\mu_t(F) = 1/2$.

theorem Mathoverflow10799.mathoverflow_10799.variants.weak_kahn_kalai (ε : ℝ) : ε > 0 → ∃ C > 0, ∀ (n : ℕ), 2 ≤ n → ∀ (F : Finset (Finset (Fin n))), IsMonotoneIncreasing F → ∀ (s t : ℝ), 0 < s → s ≤ t → t < 1 → t / s > C * ↑n ^ ε → ∃ (p : ℝ), s ≤ p ∧ p ≤ t ∧ IsOptimal p F

Weaker version proven by Kahn–Kalai: the same conclusion holds when $1000 \log n$ is replaced by $C_\varepsilon \, n^\varepsilon$ for every fixed $\varepsilon > 0$.

theorem Mathoverflow10799.discrete_isoperimetric_inequality (n : ℕ) (p : ℝ) (hp : 0 < p) (hp' : p < 1) (F : Finset (Finset (Fin n))) : have m := μFamily p F; edgeBoundary n p F ≥ m * Real.logb p m / p

Now a famous isoperimetric relation asserts that (IR) $I^p(F) \ge \frac{1}{p} \mu_p(F) \log_p \mu_p(F)$ This relation is true for every family $F$ and every $p$. It is especially famous and simple when $p=1/2$ and $\mu_p(F)=1/2$. In this case, it says that given a set of half the vertices of the discrete cube $2^X$, the number of edges between $F$ and its complement is at least $2^{n-1}$.

Note on translation: We use Real.logb p m to represent the logarithm base $p$ directly. The factor of $p$ in the denominator (equivalent to $1/p$ in front) is consistent with the definition of IsOptimal used in the counterexample proof.

theorem Mathoverflow10799.μ_sum_eq_one (n : ℕ) (p : ℝ) : ∑ S : Finset (Fin n), μ p S = 1

The $p$-biased measure is a probability distribution: it sums to $1$ over all subsets. This is the binomial identity $(p + (1-p))^n = 1$.

theorem Mathoverflow10799.μFamily_univ (n : ℕ) (p : ℝ) : μFamily p Finset.univ = 1

The measure of the full power set is $1$.

theorem Mathoverflow10799.boundaryCount_empty (n : ℕ) (S : Finset (Fin n)) : boundaryCount n ∅ S = 0

The boundary count is zero for the empty family (no set is in $\mathcal F$).

theorem Mathoverflow10799.edgeBoundary_empty (n : ℕ) (p : ℝ) : edgeBoundary n p ∅ = 0

The edge boundary is zero for the empty family.

theorem Mathoverflow10799.boundaryCount_univ (n : ℕ) (S : Finset (Fin n)) : boundaryCount n Finset.univ S = 0

The boundary count is zero for the full family (every set is in $\mathcal F$).

theorem Mathoverflow10799.edgeBoundary_univ (n : ℕ) (p : ℝ) : edgeBoundary n p Finset.univ = 0

The edge boundary is zero for the full family.