Translation preserves log-concavity

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_Translation

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a log-concave probability law μ on a finite-dimensional real inner-product space and any vector b, LogConcave.translateLaw proves that the translated law Probability.translateLaw μ b is log-concave. The statement is valid without the completeness, second-countability, and finite-dimensionality assumptions omitted by the theorem. This declaration does not assert translation invariance of a Poincaré constant, a Poincaré inequality, or any KLS bound.

Original module imports

import FunctionalInequalities.KLS.LogConcave.Covariance
import FunctionalInequalities.Poincare.CovarianceGradient.Translation

Original declaration excerpt

Shown in the original module context.

theorem translateLaw (hμ : LogConcave μ) (b : E) :
    LogConcave (Probability.translateLaw μ b) := by
  refine hμ.of_affineIsometry_map (Probability.translateLaw μ b)
    (AffineIsometryEquiv.constVAdd ℝ E (-b)).toAffineIsometry ?_
  have hf : ⇑(AffineIsometryEquiv.constVAdd ℝ E (-b)).toAffineIsometry = fun x ↦ -b + x := by
    funext x
    rfl
  rw [hf]
  exact (Probability.measurePreserving_translate_symm μ b).map_eq

Module navigation

Direct project imports: KLS/LogConcave/Covariance, Poincare/CovarianceGradient/Translation.

Theorems in source order:

memLp_id_two

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.Translation · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Covariance
import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_CovarianceGradient_Translation

noncomputable section
open MeasureTheory Filter Topology
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
open Energy.Euclidean Probability
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
  {μ : ProbabilityMeasure E}
omit [CompleteSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E] in
/-- Translating a log-concave law in the ambient space keeps it log-concave. -/
theorem translateLaw (hμ : LogConcave μ) (b : E) :
    LogConcave (Probability.translateLaw μ b) := by
  refine hμ.of_affineIsometry_map (Probability.translateLaw μ b)
    (AffineIsometryEquiv.constVAdd ℝ E (-b)).toAffineIsometry ?_
  have hf : ⇑(AffineIsometryEquiv.constVAdd ℝ E (-b)).toAffineIsometry = fun x ↦ -b + x := by
    funext x
    rfl
  rw [hf]
  exact (Probability.measurePreserving_translate_symm μ b).map_eq
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/LogConcave/Translation.lean#L38-L48 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.LogConcave.Translation`, definition bundle `KLSModular_FunctionalInequalities_KLS_LogConcave_Translation`; the repository is private at upload time).

View graph