Talagrands Convexity Conjecture

### What is the conjecture

A compact set $A \subseteq \mathbb{R}^N$ is **balanced** if whenever $x \in A$ and $\lambda \in \mathbb{R}$ with $|\lambda| \leq 1$, we have $\lambda x \in A$. Let $\gamma_N$ denote the standard Gaussian measure on $\mathbb{R}^N$.

**Talagrand's Convexity Problem** asks: Does there exist an integer $q$ (independent of the dimension $N$) such that for all $N$ and every compact balanced set $A \subseteq \mathbb{R}^N$ with $\gamma_N(A) \geq 1/2$, one can find a convex compact set $C \subseteq A + \cdots + A$ ($q$ terms in the Minkowski sum) such that $\gamma_N(C) \geq 1/2$?"

In other words, can one always create a convex set of high Gaussian measure by taking a finite (dimension-independent) number of Minkowski sums of a balanced set with high Gaussian measure?

(This description may contain subtle errors especially on more complex problems; for exact details, refer to the sources.)

A proof is worth 1000$ (I think, see sources for details).

**Sources:**
- https://michel.talagrand.net/prizes/convexity.tex | Michel Talagrand, "Are all sets of positive measure essentially convex?", Operator Theory: Advances and Applications, Vol. 77, Birkhäuser, 1995, pp. 295–310

### Prerequisites needed

**Formalizability Rating:** 1/5 (0 is best) (as of 2026-01-22)

Building blocks (from Mathlib):
- `Metric.Compact` for compact sets in ℝ^N
- `MeasureTheory.gaussianMeasure` for the Gaussian measure γ_N
- `Convex` for convexity
- Minkowski sum operations (basic algebraic structures)

Missing pieces:
- Formal definition of balanced set (simple: `∀ x ∈ A, ∀ λ ∈ ℝ, |λ| ≤ 1 → λ • x ∈ A`)
- Wrapper for the universal quantifier over dimensions and q-fold Minkowski sums

Rating justification: All essential building blocks (compact sets, Gaussian measure, convex sets, Minkowski sums) exist in Mathlib. The definition of balanced sets is straightforward. The statement itself is expressible using existing infrastructure with only minor helper definitions needed.

### [AMS categories](https://github.com/google-deepmind/formal-conjectures/labels?q=ams-)

* ams-52
* ams-28
* ams-46

### Choose either option

- [ ] I plan on adding this conjecture to the repository
- [x] This issue is up for grabs: I would like to see this conjecture added by somebody else

---
This issue was generated by an AI agent and reviewed by me.

See more information here: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Custom.20Agent.20for.20Issue.20Generation/with/569221879)

Feedback on mistakes/hallucinations: [link](https://leanprover.zulipchat.com/#narrow/channel/524981-Formal-conjectures/topic/Issue.20Agent.20Feedback.20Topic/with/569223911)

Start with the linked Talagrand source, then inspect the repository's existing formalized conjecture declarations and the available Mathlib definitions listed in the issue. Formalize the balanced-set and dimension-independent Minkowski-sum statement, ensuring the resulting Lean declaration typechecks and matches the source's intended quantifiers.

Written by the indexing model from the issue text.