10799.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

20 declarations, 4 contain sorry, 0 declared as axioms

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)

Imports (1)

FormalConjecturesUtil

Imported by 1 file

FormalConjectures/Subsets/FC100SolvedSet1.lean

def Mathoverflow10799.μ Start with a set $X=\{1,2,...,n\}$ of $n$ elements and the family $2^X$ of all subsets of $X$ line 49 source
Source documentation
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|}$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Fin
Proof uses: HMul.hMul, HPow.hPow, Finset.card, HSub.hSub, OfNat.ofNat
11 instances, coercions and auxiliary constants left out.
```
noncomputable def μ {n : ℕ} (p : ℝ) (S : Finset (Fin n)) : ℝ :=
…
```
theorem Mathoverflow10799.μ_half_eq_uniform For $p = 1/2$, the $p$-biased measure is the uniform distribution: $\mu_{1/2}(S) = (1/2)^n$ for every $S \subseteq [n]$ line 55 source
Source documentation
For $p = 1/2$, the $p$-biased measure is the uniform distribution: $\mu_{1/2}(S) = (1/2)^n$ for every $S \subseteq [n]$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, Real, Mathoverflow10799.μ, HDiv.hDiv, OfNat.ofNat, HPow.hPow
Proof uses: LE.le, Finset.card, LE.le.trans_eq, Fintype.card, Finset.card_le_univ, Fintype.card_fin, id, Eq.mpr, HMul.hMul, HSub.hSub, congrArg, Mathlib.Tactic.Ring.of_eq, HAdd.hAdd, NNRat.rawCast, Mathlib.Tactic.Ring.Common.sub_congr, Nat.rawCast, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.div_congr and 40 more
82 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem μ_half_eq_uniform {n : ℕ} (S : Finset (Fin n)) :
    μ (1/2) S = (1/2 : ℝ) ^ n := by
…
```
Mentions: Mathoverflow10799.μ
def Mathoverflow10799.μFamily 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)$ line 65 source
Source documentation
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)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Fin
Proof uses: Finset.sum, Mathoverflow10799.μ
1 instances, coercions and auxiliary constants left out.
```
noncomputable def μFamily {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
…
```
def Mathoverflow10799.boundaryCount Given a family line 74 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin
Proof uses: Finset.card, Finset.filter, Xor, Membership.mem, symmDiff, Singleton.singleton, Finset.univ
12 instances, coercions and auxiliary constants left out.
```
def boundaryCount (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) : ℕ :=
…
```
theorem Mathoverflow10799.boundaryCount_equiv 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$ line 82 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, Mathoverflow10799.boundaryCount, Finset.card, Finset.filter, And, symmDiff, OfNat.ofNat, Xor, Membership.mem, Finset.univ
Proof uses: id, Finset.ext, Eq.mpr, Iff, Or, Not, congrFun', congrArg, Eq.trans, congr, Iff.intro, Iff.mp, not_or, Decidable.not_and_iff_not_or_not', False.elim, Decidable.of_not_not, Iff.mpr, Classical.or_iff_not_imp_left, And.intro, False and 20 more
43 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
theorem boundaryCount_equiv (n : ℕ) (F : Finset (Finset (Fin n))) (S : Finset (Fin n)) :
    boundaryCount n F S = (Finset.univ.filter fun T : Finset (Fin n) ↦
      (symmDiff S T).card = 1 ∧ Xor (S ∈ F) (T ∈ F)).card := by
…
```
Mentions: Mathoverflow10799.boundaryCount
def Mathoverflow10799.edgeBoundary The edge-boundary of $F$ is the expectation of $h(S)$ (according to $\mu_p$) over all subsets $S$ of $X$ line 118 source
Source documentation
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)$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Fin
Proof uses: Finset.sum, Finset.univ, HMul.hMul, Mathoverflow10799.μ, Mathoverflow10799.boundaryCount
7 instances, coercions and auxiliary constants left out.
```
noncomputable def edgeBoundary (n : ℕ) (p : ℝ) (F : Finset (Finset (Fin n))) : ℝ :=
…
```
abbrev Mathoverflow10799.IsMonotoneIncreasing 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$ line 130 source
Source documentation
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 ⊆.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin
Proof uses: IsUpperSet
5 instances, coercions and auxiliary constants left out.
```
abbrev IsMonotoneIncreasing {n : ℕ} (F : Finset (Finset (Fin n))) : Prop :=
…
```
def Mathoverflow10799.IsOptimal 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)$ line 142 source
Source documentation
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)}.$$

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Fin
Proof uses: Mathoverflow10799.μFamily, LE.le, Mathoverflow10799.edgeBoundary, HMul.hMul, OfNat.ofNat, Real.log, HDiv.hDiv, Real.logb
11 instances, coercions and auxiliary constants left out.
```
noncomputable def IsOptimal {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) : Prop :=
…
```
def Mathoverflow10799.IsOptimalWith Documented declaration: IsOptimalWith line 152 source
Source documentation
Following Kahn–Kalai, a family is $(C \log(1/p), p)$-optimal if the isoperimetric inequality (IR) is sharp up to the multiplicative constant $C \log(1/p)$, i.e. $$I^p(\mathcal F) \le \frac{C}{p} \cdot \mu_p(\mathcal F) \cdot \log \frac{1}{\mu_p(\mathcal F)}.$$ IsOptimal is the special case $C = 1000$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Fin
Proof uses: Mathoverflow10799.μFamily, LE.le, Mathoverflow10799.edgeBoundary, HMul.hMul, Real.log, HDiv.hDiv, OfNat.ofNat, Real.logb
8 instances, coercions and auxiliary constants left out.
```
noncomputable def IsOptimalWith {n : ℕ} (C p : ℝ) (F : Finset (Finset (Fin n))) : Prop :=
…
```
theorem Mathoverflow10799.isOptimal_iff_isOptimalWith IsOptimal is IsOptimalWith for the constant $C = 1000$ line 158 source
Source documentation
IsOptimal is IsOptimalWith for the constant $C = 1000$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Finset, Fin, Iff, Mathoverflow10799.IsOptimal, Mathoverflow10799.IsOptimalWith, OfNat.ofNat
Proof uses: Iff.rfl
5 instances, coercions and auxiliary constants left out.
```
theorem isOptimal_iff_isOptimalWith {n : ℕ} (p : ℝ) (F : Finset (Finset (Fin n))) :
    IsOptimal p F ↔ IsOptimalWith 1000 p F :=
…
```
Mentions: Mathoverflow10799.IsOptimal, Mathoverflow10799.IsOptimalWith
theorem Mathoverflow10799.mathoverflow_10799 sorry line 177 source
depends on sorry what this means
Statement uses: Iff, False, Nat, LE.le, OfNat.ofNat, Finset, Fin, Mathoverflow10799.IsMonotoneIncreasing, Real, LT.lt, GT.gt, HDiv.hDiv, HMul.hMul, Real.log, Exists, And, Mathoverflow10799.IsOptimal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow10799.mathoverflow_10799.variants.kahn_kalai_conjecture_7 sorry line 200 source
depends on sorry what this means
Statement uses: Iff, False, Nat, LE.le, OfNat.ofNat, Finset, Fin, Mathoverflow10799.IsMonotoneIncreasing, Real, LT.lt, Eq, Mathoverflow10799.μFamily, HDiv.hDiv, GT.gt, HMul.hMul, Real.log, Exists, And, Mathoverflow10799.IsOptimal
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
36 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Mathoverflow10799.mathoverflow_10799.variants.weak_kahn_kalai Weaker version proven by Kahn–Kalai (2006): for every fixed sorry line 216 source
Source documentation
Weaker version proven by Kahn–Kalai (2006): for every fixed $\varepsilon > 0$ there is a constant $C = C_\varepsilon$ such that for every monotone increasing family $F$ with critical probability $t$, i.e. $\mu_t(F) = 1/2$, there is some $p \in [n^{-\varepsilon} t, t]$ for which $F$ is $(C \log(1/p), p)$-optimal.

depends on sorry what this means
Statement uses: Real, GT.gt, OfNat.ofNat, Exists, And, Nat, LE.le, Finset, Fin, Mathoverflow10799.IsMonotoneIncreasing, LT.lt, Eq, Mathoverflow10799.μFamily, HDiv.hDiv, HMul.hMul, HPow.hPow, Neg.neg, Mathoverflow10799.IsOptimalWith
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
42 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem mathoverflow_10799.variants.weak_kahn_kalai :
    ∀ ε > (0 : ℝ), ∃ C > (0 : ℝ), ∀ (n : ℕ) (_ : 2 ≤ n)
    (F : Finset (Finset (Fin n))) (_ : IsMonotoneIncreasing F)
    (t : ℝ) (_ : 0 < t) (_ : t < 1) (_ : μFamily t F = 1 / 2),
    ∃ p, (n : ℝ) ^ (-ε) * t ≤ p ∧ p ≤ t ∧ IsOptimalWith C p F := by
…
```
Mentions: Mathoverflow10799.IsMonotoneIncreasing, Mathoverflow10799.μFamily, Mathoverflow10799.IsOptimalWith
theorem Mathoverflow10799.discrete_isoperimetric_inequality 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 holds for monotone increasing families $F$ and $0 < p < 1$ sorry line 236 source
Source documentation
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 holds for monotone increasing families $F$ and $0 < p < 1$. 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.

depends on sorry what this means
Statement uses: Nat, Real, LT.lt, OfNat.ofNat, Finset, Fin, Mathoverflow10799.IsMonotoneIncreasing, Mathoverflow10799.μFamily, GE.ge, Mathoverflow10799.edgeBoundary, HDiv.hDiv, HMul.hMul, Real.logb
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
23 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem discrete_isoperimetric_inequality (n : ℕ) (p : ℝ) (hp : 0 < p) (hp' : p < 1)
    (F : Finset (Finset (Fin n))) (hF : IsMonotoneIncreasing F) :
    let m := μFamily p F
…
```
Mentions: Mathoverflow10799.IsMonotoneIncreasing, Mathoverflow10799.μFamily
theorem Mathoverflow10799.μ_sum_eq_one The $p$-biased measure is a probability distribution: it sums to $1$ over all subsets line 247 source
Source documentation
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$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Finset.sum, Finset, Fin, Finset.univ, Mathoverflow10799.μ, OfNat.ofNat
Proof uses: id, HMul.hMul, HPow.hPow, Finset.card, HSub.hSub, Fintype.card, HAdd.hAdd, Fintype.sum_pow_mul_eq_add_pow, Eq.mpr, congrArg, Eq.mp, Fintype.card_fin, of_eq_true, Eq.trans, True, congrFun', add_sub_cancel, one_pow, eq_self
31 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
theorem μ_sum_eq_one (n : ℕ) (p : ℝ) :
    ∑ S : Finset (Fin n), μ p S = 1 := by
…
```
Mentions: Mathoverflow10799.μ
theorem Mathoverflow10799.μFamily_univ The measure of the full power set is $1$ line 257 source
Source documentation
The measure of the full power set is $1$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Mathoverflow10799.μFamily, Finset.univ, Finset, Fin, OfNat.ofNat
Proof uses: id, Mathoverflow10799.μ_sum_eq_one
8 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem μFamily_univ (n : ℕ) (p : ℝ) :
    μFamily p (Finset.univ : Finset (Finset (Fin n))) = 1 := by
…
```
Mentions: Mathoverflow10799.μFamily
theorem Mathoverflow10799.boundaryCount_empty The boundary count is zero for the empty family (no set is in $\mathcal F$) line 264 source
Source documentation
The boundary count is zero for the empty family (no set is in $\mathcal F$).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, Mathoverflow10799.boundaryCount, EmptyCollection.emptyCollection, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Xor, Membership.mem, symmDiff, Singleton.singleton, Finset.univ, Finset.card, False, Finset.filter_congr, Iff.of_eq, congr, xor_self, Finset.filter_false, eq_self
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem boundaryCount_empty (n : ℕ) (S : Finset (Fin n)) :
    boundaryCount n ∅ S = 0 := by
…
```
Mentions: Mathoverflow10799.boundaryCount
theorem Mathoverflow10799.edgeBoundary_empty The edge boundary is zero for the empty family line 270 source
Source documentation
The edge boundary is zero for the empty family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Mathoverflow10799.edgeBoundary, EmptyCollection.emptyCollection, Finset, Fin, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.sum, Finset.univ, HMul.hMul, Mathoverflow10799.μ, Mathoverflow10799.boundaryCount, Finset.sum_congr, Eq.refl, Membership.mem, Mathoverflow10799.boundaryCount_empty, CharP.cast_eq_zero, MulZeroClass.mul_zero, Finset.sum_const_zero, eq_self
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem edgeBoundary_empty (n : ℕ) (p : ℝ) :
    edgeBoundary n p ∅ = 0 := by
…
```
Mentions: Mathoverflow10799.edgeBoundary
theorem Mathoverflow10799.boundaryCount_univ The boundary count is zero for the full family (every set is in $\mathcal F$) line 276 source
Source documentation
The boundary count is zero for the full family (every set is in $\mathcal F$).

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Finset, Fin, Eq, Mathoverflow10799.boundaryCount, Finset.univ, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.filter, Xor, Membership.mem, symmDiff, Singleton.singleton, EmptyCollection.emptyCollection, Finset.card, False, Finset.filter_congr, Iff.of_eq, congr, xor_self, Finset.filter_false, eq_self
20 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem boundaryCount_univ (n : ℕ) (S : Finset (Fin n)) :
    boundaryCount n Finset.univ S = 0 := by
…
```
Mentions: Mathoverflow10799.boundaryCount
theorem Mathoverflow10799.edgeBoundary_univ The edge boundary is zero for the full family line 282 source
Source documentation
The edge boundary is zero for the full family.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Real, Eq, Mathoverflow10799.edgeBoundary, Finset.univ, Finset, Fin, OfNat.ofNat
Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Finset.sum, HMul.hMul, Mathoverflow10799.μ, Mathoverflow10799.boundaryCount, Finset.sum_congr, Eq.refl, Membership.mem, Mathoverflow10799.boundaryCount_univ, CharP.cast_eq_zero, MulZeroClass.mul_zero, Finset.sum_const_zero, eq_self
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem edgeBoundary_univ (n : ℕ) (p : ℝ) :
    edgeBoundary n p Finset.univ = 0 := by
…
```
Mentions: Mathoverflow10799.edgeBoundary