Probability of compactly supported quadratic posteriors

Definition

KLSModular_FunctionalInequalities_Probability_Posterior_CompactQuadratic

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a probability measure $\mu$ on a finite-dimensional real inner-product space with compact topological support, isProbabilityMeasure_tilted_quadraticExponent_of_compact states that the tilt by quadraticExponent c Q is a probability measure for every $c\in E$ and continuous linear map $Q:E\to E$ . The assertion includes arbitrary finite parameters, with no positivity or symmetry assumption on $Q$ .

Original module imports

import FunctionalInequalities.Probability.Posterior.CompactPrior
import FunctionalInequalities.Probability.Posterior.Coercive

Original declaration excerpt

Shown in the original module context.

theorem isProbabilityMeasure_tilted_quadraticExponent_of_compact (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (c : E) (Q : E →L[ℝ] E) :
    IsProbabilityMeasure ((μ : Measure E).tilted (quadraticExponent c Q)) := by
  apply isProbabilityMeasure_tilted_of_compact μ hc
  unfold quadraticExponent
  fun_prop

Module navigation

Direct project imports: Probability/Posterior/CompactPrior, Probability/Posterior/Coercive.

Theorems in source order:

exists_uniform_norm_moments_tilted_quadraticExponent_of_compact

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_CompactPrior
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_Coercive

noncomputable section
open MeasureTheory Filter Topology ProbabilityTheory
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace Probability
namespace Posterior
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
/-- Every posterior of a compactly supported prior is a probability law. -/
theorem isProbabilityMeasure_tilted_quadraticExponent_of_compact (μ : ProbabilityMeasure E)
    (hc : IsCompact (μ : Measure E).support) (c : E) (Q : E →L[ℝ] E) :
    IsProbabilityMeasure ((μ : Measure E).tilted (quadraticExponent c Q)) := by
  apply isProbabilityMeasure_tilted_of_compact μ hc
  unfold quadraticExponent
  fun_prop
end Posterior
end Probability
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Posterior/CompactQuadratic.lean#L41-L47 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Posterior.CompactQuadratic`, definition bundle `KLSModular_FunctionalInequalities_Probability_Posterior_CompactQuadratic`; the repository is private at upload time).

View graph