Barycenters under translation of probability laws

Definition

KLSModular_FunctionalInequalities_Probability_IntrinsicTranslation

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Probability.integral_id_translateLaw states that, for an integrable identity function, translating a probability law by c translates its barycenter by c: $\int x\,d(\operatorname{translateLaw}(\nu,c))=c+\int x\,d\nu$ . integral_id_translateLaw_neg_integral specializes this to translation by the negative barycenter and concludes that the translated law has barycenter zero. The statements do not require finite-dimensionality, although the surrounding module supplies stronger ambient structure.

Original module imports

import FunctionalInequalities.Probability.Transport
import FunctionalInequalities.Probability.AffineSupport

Original declaration excerpt

Shown in the original module context.

theorem integral_id_translateLaw (ν : ProbabilityMeasure V) (hint : Integrable id (ν : Measure V))
    (c : V) : ∫ x, x ∂(translateLaw ν c : Measure V) = c + ∫ x, x ∂(ν : Measure V) := by
  rw [coe_translateLaw, integral_map (measurable_const_add c).aemeasurable
    continuous_id'.aestronglyMeasurable]
  have hint' : Integrable (fun x : V ↦ x) (ν : Measure V) := hint
  rw [integral_add (integrable_const c) hint', integral_const, probReal_univ, one_smul]

Module navigation

Direct project imports: Probability/Transport, Probability/AffineSupport.

Theorems in source order:

affineSupport_translateLaw

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.IntrinsicTranslation · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_AffineSupport

noncomputable section
open MeasureTheory Filter Topology
namespace FunctionalInequalities
namespace Probability
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
  [MeasurableSpace V] [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
omit [FiniteDimensional ℝ V] in
/-- The barycenter of a translated law is the translated barycenter. -/
theorem integral_id_translateLaw (ν : ProbabilityMeasure V) (hint : Integrable id (ν : Measure V))
    (c : V) : ∫ x, x ∂(translateLaw ν c : Measure V) = c + ∫ x, x ∂(ν : Measure V) := by
  rw [coe_translateLaw, integral_map (measurable_const_add c).aemeasurable
    continuous_id'.aestronglyMeasurable]
  have hint' : Integrable (fun x : V ↦ x) (ν : Measure V) := hint
  rw [integral_add (integrable_const c) hint', integral_const, probReal_univ, one_smul]
omit [FiniteDimensional ℝ V] in
/-- Translating by the negative barycenter centers the law. -/
theorem integral_id_translateLaw_neg_integral (ν : ProbabilityMeasure V)
    (hint : Integrable id (ν : Measure V)) :
    ∫ x, x ∂(translateLaw ν (-∫ x, x ∂(ν : Measure V)) : Measure V) = 0 := by
  rw [integral_id_translateLaw ν hint]
  simp
end Probability
end FunctionalInequalities

Source

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

View graph