Log-Concavity Under Convex Conditioning

Proved

FunctionalInequalities.KLS.LogConcave.cond_readable

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

bkl2026functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This formalizes the conditioning statement used in the compact-support reduction for Theorem 4.1 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $E$ be a real normed space with Borel measurable structure, and let $\mu$ be a log-concave probability measure. Let $C\subseteq E$ be convex and closed, and assume $\mu(C)\ne0$ . Form the conditional probability measure $\mu[\mid C]$ using cond_readable.

Then the conditional law remains log-concave:

\operatorname{LogConcave}(\mu[\mid C]).

The result applies the compact-set definition of log-concavity and is particularly suited to conditioning on closed balls. It makes no assertion about isotropy or compactness of the conditional law beyond the stated hypotheses.

Original Lean declaration header

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

theorem cond {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E] {μ : ProbabilityMeasure E} (hμ : LogConcave μ)
    {C : Set E} (hC : Convex ℝ C) (hCc : IsClosed C) (hpos : (μ : Measure E) C ≠ 0) :
    LogConcave (⟨(μ : Measure E)[|C], cond_isProbabilityMeasure hpos⟩ : ProbabilityMeasure E)

Module navigation

Module: KLS/LogConcave/Transport.

Definition modules: Probability/LogConcave.

Previous: map_affineIsometry.

Source excerpt, lines 216–219 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Transport

open MeasureTheory Set Topology
open ProbabilityTheory

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.cond_readable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [MeasurableSpace E] [BorelSpace E] {μ : ProbabilityMeasure E} (hμ : LogConcave μ)
    {C : Set E} (hC : Convex ℝ C) (hCc : IsClosed C) (hpos : (μ : Measure E) C ≠ 0) :
    LogConcave (⟨(μ : Measure E)[|C], cond_isProbabilityMeasure hpos⟩ : ProbabilityMeasure E) := by sorry

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), Theorem 4.1, p. 18. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Transport.lean#L212-L360 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Transport`, declaration `FunctionalInequalities.KLS.LogConcave.cond`; the repository is private at upload time).

View graph