Convexity of the Finite-Copy Suspension Potential

This auxiliary convexity statement formalizes the convexity component of Proposition 7.1, p. 28, equations (109)–(110), of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a real inner product space and let $V,f:E\to\mathbb R$ be $C^2$. Let $a,M,\beta,\sigma\in\mathbb R$ and $N\in\mathbb N$. Assume:

1. $\beta\ge0$.
2. $D^2V(x)[v,v]\ge a\|v\|^2$ for every $x,v\in E$, with the bilinear second derivative represented by bilinearIteratedFDerivTwo.
3. $\|D(Df)(x)\|\le M$ for every $x\in E$, using fderiv and its operator norm.
4. $(\beta/\sqrt N)M\le a$.

The function defined by potential,

is convex on all of $\mathbb R\times(\operatorname{Fin}N\to E)$.

This isolates the deterministic convexity condition used in the suspension construction, rather than the full proposition.

Formalization Note No positivity restriction on $N$, $a$, $M$, or $\sigma$ is added. In particular $N=0$ is allowed, with Lean's totalized real division.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.Suspension. Shown in its original module context. Proof omitted.

theorem convexOn_potential {V f : E → ℝ} (hV : ContDiff ℝ 2 V) (hf : ContDiff ℝ 2 f)
    {a M beta sigma : ℝ} (hbeta : 0 ≤ beta)
    (hVlower : ∀ x v, a * ‖v‖ ^ 2 ≤ bilinearIteratedFDerivTwo ℝ V x v v)
    (hfbound : ∀ x, ‖fderiv ℝ (fderiv ℝ f) x‖ ≤ M)
    (N : ℕ) (hN : beta / Real.sqrt N * M ≤ a) :
    ConvexOn ℝ Set.univ (potential V f beta sigma N)

Module navigation

Module: KLS/BKL/Suspension/Basic.

Supporting theorems: convexOn_of_hessian_ge.

Next: exists_copies.

Source excerpt, lines 85–90 · Frozen source 408915f.