Compactly supported quadratic posterior law

Definition

KLSModular_FunctionalInequalities_Probability_Posterior_CompactDomain

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

bkl2026functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a probability measure $\mu$ on a finite-dimensional real inner-product space with compact support, compactPosterior μ hc c Q is the probability measure whose underlying measure is the tilt of $\mu$ by $x\mapsto\langle c,x\rangle-\frac12\langle Qx,x\rangle$ . The probability structure is justified by isProbabilityMeasure_tilted_quadraticExponent_of_compact, and the definition permits every $c$ and continuous linear map $Q$ .

Original module imports

import FunctionalInequalities.Probability.Posterior.CompactQuadratic
import FunctionalInequalities.Probability.Covariance.Positivity
import FunctionalInequalities.Probability.Transport

Original declaration excerpt

Shown in the original module context.

def compactPosterior (μ : ProbabilityMeasure E) (hc : IsCompact (μ : Measure E).support)
    (c : E) (Q : E →L[ℝ] E) : ProbabilityMeasure E :=
  ⟨(μ : Measure E).tilted (quadraticExponent c Q), isProbabilityMeasure_tilted_quadraticExponent_of_compact μ hc c Q⟩

Module navigation

Direct project imports: Probability/Posterior/CompactQuadratic, Probability/Covariance/Positivity, Probability/Transport.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.Posterior.CompactDomain · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactQuadratic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Covariance_Positivity
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport

noncomputable section
open MeasureTheory
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace Probability
namespace Posterior
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
/-- The BKL posterior `μ.tilted (⟪c,·⟫ − ½⟪Q·,·⟫)` of a compactly supported prior, as a probability law
(every finite `(c, Q)`, including `0` and negative `Q`). -/
def compactPosterior (μ : ProbabilityMeasure E) (hc : IsCompact (μ : Measure E).support)
    (c : E) (Q : E →L[ℝ] E) : ProbabilityMeasure E :=
  ⟨(μ : Measure E).tilted (quadraticExponent c Q), isProbabilityMeasure_tilted_quadraticExponent_of_compact μ hc c Q⟩
end Posterior
end Probability
end FunctionalInequalities

Source

Source: Bizeul–Klartag–Lehec, Presenting a proof of the Kannan–Lovász–Simonovits conjecture (arXiv:2610.05474v1), item E67. Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/CompactDomain.lean#L26-L30 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.CompactDomain`, definition bundle `KLSModular_FunctionalInequalities_Probability_Posterior_CompactDomain`; the repository is private at upload time).

View graph