Project idea: Talagrand's isoperimetric inequality

Stream: LFTCM 2024

[Rémy Degenne]

I am not attending LftCM and I don't know how projects are organized this year, but I just had an idea for a cool project, so here it is.

Michel Talagrand was awarded the Abel price yesterday. His two most well known works are isoperimetric inequalities and generic chaining. While generic chaining is very technical, the basic versions of Talagrand's isoperimetric inequality have short proofs that should be formalizable in Lean.

When hearing "isoperimetric inequality", one thinks about the fact that the solid with lowest surface for a given volume is a ball. Another formulation is that for a given volume, the ball minimizes the volume of the sets of points within distance $t$ of itself (the limit $t \to 0$ gives the surface/volume statement).
In a more abstract formulation, let $A$ be a set in a product space $\Omega^N$ with a product measure $P$. Then the isoperimetric inequalities of Talagrand are upper bounds similar in shape to $P(A_t^c) P(A) \le e^{-t^2/N}$, where $A_t$ is the set of points at "distance" $t$ of $A$ (and the bound depends on the "distance").

The project is to formalize Proposition 2.1.1 from https://link.springer.com/article/10.1007/BF02699376 (also https://arxiv.org/abs/math/9406212). The proof is two pages on paper, and is mostly about bounding some integrals. I was looking for the main difficulty and I am not certain of what we have in mathlib about the extrema of convex functions, but there is a "it is well known" in the middle of the proof of lemma 2.1.2 which might require some work... or a well placed sorry depending on the interests of the project participants.

[Vincent Beffara]

Good idea ! It sounds like a doable project.

BTW, free access to the published version here http://www.numdam.org/item/PMIHES_1995__81__73_0/

[Frédéric Dupuis]

There is also the book "The concentration of measure phenomenon" by Michel Ledoux that would be a good reference for this topic, and probably a good source of related projects.