Affine Support Under Translation

Proved

FunctionalInequalities.Probability.affineSupport_translateLaw_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the affine-support transport identity for translated probability laws.

Let $E$ be a finite-dimensional real inner-product normed space with Borel and second-countable structure. Let $\mu$ be a probability measure on $E$ and let $b\in E$ . If translateLaw μ b is the pushforward of $\mu$ by $x\mapsto b+x$ , then

\operatorname{affineSupport}(\operatorname{translateLaw}(\mu,b)) =\bigl(\operatorname{affineSupport}(\mu)\bigr)+b.

The right side is expressed in Lean as the affine-subspace map under AffineEquiv.constVAdd. This is a geometric support-transport lemma.

Original Lean declaration header

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

theorem affineSupport_translateLaw :
    affineSupport (translateLaw μ b) =
      (affineSupport μ).map (AffineEquiv.constVAdd ℝ E b).toAffineMap

Module navigation

Module: Probability/IntrinsicTranslation.

Definition modules: Probability/AffineSupport, Probability/Transport.

Source excerpt, lines 30–32 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_IntrinsicTranslation

universe u
variable {E : Type u} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E] [FiniteDimensional ℝ E]
variable (μ : MeasureTheory.ProbabilityMeasure E) (b : E)

Formal statement


theorem FunctionalInequalities.Probability.affineSupport_translateLaw_readable :
    affineSupport (translateLaw μ b) =
      (affineSupport μ).map (AffineEquiv.constVAdd ℝ E b).toAffineMap := by sorry

Source

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

View graph