Compact Regular Approximation by Isotropic Uniformly Convex Laws

Proved

FunctionalInequalities.KLS.LogConcave.exists_regularClass_seq_of_compact_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readableletwin2026log-concave

This formalizes the compactly supported part of Lemma A.1 of Letwin (arXiv:2607.24164v1).

Let $n\in\mathbb N$ , let $μ$ be a probability measure on EuclideanSpace ℝ (Fin n), and assume that $μ$ is log-concave, isotropic, and has compact measure support. Then there exists a sequence $(ζ_j)$ of probability measures such that, for every $j$ , $ζ_j$ is isotropic and there exist $K_j$ , $W_j$ , and $κ_j$ with:

$κ_j>0$ , $K_j$ compact and convex, and $\operatorname{int}K_j$ nonempty;
$W_j$ is $C^\infty$ and $y\mapsto W_j(y)-(κ_j/2)\|y\|^2$ is convex on the whole space;
$ζ_j$ has density ENNReal.ofReal (exp (-W_j)) restricted to $K_j$ with respect to volume;
for every $d\le4$ and every $v:\operatorname{Fin}(d)\to\mathbb R^n$ , the mixed moments converge:

\int\prod_i\langle v_i,x\rangle\,dζ_j(x) \longrightarrow \int\prod_i\langle v_i,x\rangle\,dμ(x).

The dimension parameter is arbitrary, including $n=0$ , exactly as in the Lean statement.

Original Lean declaration header

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

theorem exists_regularClass_seq_of_compact {n : ℕ}
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))) (hLC : KLS.LogConcave μ) (hiso : KLS.Isotropic μ)
    (hcompact : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support) :
    ∃ ζ : ℕ → ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
      (∀ j, KLS.Isotropic (ζ j) ∧ ∃ (K : Set (EuclideanSpace ℝ (Fin n))) (W : EuclideanSpace ℝ (Fin n) → ℝ)
        (κ : ℝ), 0 < κ ∧ IsCompact K ∧ Convex ℝ K ∧ (interior K).Nonempty ∧ ContDiff ℝ ∞ W ∧
          ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2) ∧
          (ζ j : Measure (EuclideanSpace ℝ (Fin n))) =
            (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity
              (K.indicator fun p => ENNReal.ofReal (Real.exp (-W p)))) ∧
      ∀ d ≤ 4, ∀ v : Fin d → EuclideanSpace ℝ (Fin n),
        Tendsto (fun j => ∫ x, ∏ i, ⟪v i, x⟫ ∂(ζ j : Measure (EuclideanSpace ℝ (Fin n)))) atTop
          (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure (EuclideanSpace ℝ (Fin n)))))

Module navigation

Module: KLS/Letwin/Approximation.

Definition modules: Probability/LogConcave, KLS/Isotropic.

Selected supporting theorems: exists_metric_diagonal, row_joint_tendsto, smoothedLaw_covarianceBilin, smoothedLaw_integral_bounded_tendsto, smoothedLaw_mean.

Source excerpt, lines 91–103 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_Letwin_Approximation

open MeasureTheory Set Filter Topology
open scoped RealInnerProductSpace ContDiff

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.exists_regularClass_seq_of_compact_readable {n : ℕ}
    (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n))) (hLC : KLS.LogConcave μ) (hiso : KLS.Isotropic μ)
    (hcompact : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support) :
    ∃ ζ : ℕ → ProbabilityMeasure (EuclideanSpace ℝ (Fin n)),
      (∀ j, KLS.Isotropic (ζ j) ∧ ∃ (K : Set (EuclideanSpace ℝ (Fin n))) (W : EuclideanSpace ℝ (Fin n) → ℝ)
        (κ : ℝ), 0 < κ ∧ IsCompact K ∧ Convex ℝ K ∧ (interior K).Nonempty ∧ ContDiff ℝ ∞ W ∧
          ConvexOn ℝ univ (fun y => W y - (κ / 2) * ‖y‖ ^ 2) ∧
          (ζ j : Measure (EuclideanSpace ℝ (Fin n))) =
            (volume : Measure (EuclideanSpace ℝ (Fin n))).withDensity
              (K.indicator fun p => ENNReal.ofReal (Real.exp (-W p)))) ∧
      ∀ d ≤ 4, ∀ v : Fin d → EuclideanSpace ℝ (Fin n),
        Tendsto (fun j => ∫ x, ∏ i, ⟪v i, x⟫ ∂(ζ j : Measure (EuclideanSpace ℝ (Fin n)))) atTop
          (𝓝 (∫ x, ∏ i, ⟪v i, x⟫ ∂(μ : Measure (EuclideanSpace ℝ (Fin n))))) := by sorry

Source

Source: Letwin, The KLS constant is O(log^(1/4) n) (arXiv:2607.24164v1), Lemma A.1. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/Letwin/Approximation.lean#L87-L245 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.Letwin.Approximation`, declaration `FunctionalInequalities.KLS.LogConcave.exists_regularClass_seq_of_compact`; the repository is private at upload time).

View graph