Finite-copy suspension potential

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Basic

by Lazyfill · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a potential $V:E\to\mathbb{R}$ , function $f:E\to\mathbb{R}$ , real parameters $\beta,\sigma$ , copy count $N$ , and point $(s,x_1,\ldots,x_N)$ , potential V f beta sigma N is $\sum_iV(x_i)+\beta\left|\sigma s-\frac{\sum_i f(x_i)}{\sqrt N}\right|$ . The definition is made on $\mathbb{R}\times(\mathrm{Fin}\,N\to E)$ and does not impose positivity of $\beta$ , a relation between $\sigma$ and $\beta$ , or convexity.

Original module imports

import FunctionalInequalities.Analysis.BakryEmery.Curvature

Original declaration excerpt

Shown in the original module context.

def potential (V f : E → ℝ) (beta sigma : ℝ) (N : ℕ) (p : ℝ × (Fin N → E)) : ℝ :=
  (∑ i, V (p.2 i)) + beta * |sigma * p.1 - (∑ i, f (p.2 i)) / Real.sqrt N|

Module navigation

Direct project imports: Analysis/BakryEmery/Curvature.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Suspension.Basic · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Curvature

noncomputable section
open scoped ContDiff
open FunctionalInequalities.Analysis.BakryEmery
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace Suspension
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- The potential (109) on one auxiliary coordinate and `N` copies of the original space.
In the paper `sigma = sqrt (1 + 2 / beta²)`. Convexity holds for every real `sigma`. -/
def potential (V f : E → ℝ) (beta sigma : ℝ) (N : ℕ) (p : ℝ × (Fin N → E)) : ℝ :=
  (∑ i, V (p.2 i)) + beta * |sigma * p.1 - (∑ i, f (p.2 i)) / Real.sqrt N|
end Suspension
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Suspension/Basic.lean#L24-L27 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Suspension.Basic`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Basic`; the repository is private at upload time).

View graph