# Talagrand’s expectation thresholds, discrete convexity, and graph decompositions

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Integral and fractional expectation thresholds are equivalent](../../preprints/Integral-and-fractional-expectation-thresholds-are-equivalent-September-23-2026/paper.pdf)
- [Talagrand's discrete-convexity conjecture](../../preprints/Talagrands-discrete-convexity-conjecture-September-23-2026/paper.pdf)

## Scope

Talagrand's expectation-threshold conjecture asks whether the fractional and integral expectation thresholds are comparable by an absolute constant. The formalized result proves $q_f(\mathcal F)\le25\cdot512^4 q(\mathcal F)$ for every nonempty proper increasing family on a finite nonempty ground set. Both thresholds use cover budget $1/2$, and fractional covers may assign weights to every subset, including the empty set.

The formalized result proves Talagrand's discrete-convexity assertion with $k=2^{75}$. If a family of subsets of a finite nonempty ground set has Bernoulli-$p$ measure at least $1-1/k$, then the sets not contained in a union of $k$ members form a $p$-small family: they have a containment cover of total $p$-cost at most $1/2$. This holds for every $0<p<1$, with repeated members allowed in the union and no monotonicity assumption.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Integral–fractional expectation-threshold comparison | [TalagrandExpectationThreshold.lean](../ComparatorChallenges/TalagrandExpectationThreshold.lean) |
| Talagrand discrete convexity | [TalagrandDiscreteConvexity.lean](../ComparatorChallenges/TalagrandDiscreteConvexity.lean) |