Affine Support Under A Continuous Linear Equivalence

Proved

FunctionalInequalities.Probability.affineSupport_mapContinuousLinearEquiv_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This theorem describes the affine support of a pushforward probability law.

Let $V_1$ and $V_2$ be normed real inner-product spaces with measurable Borel structures, let $\nu$ be a probability measure on $V_1$ , and let $T:V_1\to V_2$ be a continuous linear equivalence. Assume the second-countable and finite-dimensional hypotheses stated in the type. Then

\operatorname{affineSupport}(T_\#\nu) = T\bigl(\operatorname{affineSupport}(\nu)\bigr),

where the image on the right is the affine-subspace map induced by the linear equivalence. In Lean, the pushforward is mapContinuousLinearEquiv and the affine-subspace image is formed with AffineSubspace.map. This is a transport lemma for affine support and does not assert anything about covariance or moments.

Original Lean declaration header

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

theorem Probability.affineSupport_mapContinuousLinearEquiv :
    affineSupport (mapContinuousLinearEquiv ν T) = (affineSupport ν).map (T : V₁ →ₗ[ℝ] V₂).toAffineMap

Module navigation

Module: Probability/Transport.

Definition modules: Probability/AffineSupport.

Previous: Covariance.operator_map_continuousLinearEquiv.

Source excerpt, lines 378–379 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport

universe u v
variable {V₁ : Type u} [NormedAddCommGroup V₁] [InnerProductSpace ℝ V₁]
  [MeasurableSpace V₁] [BorelSpace V₁]
variable {V₂ : Type v} [NormedAddCommGroup V₂] [InnerProductSpace ℝ V₂]
  [MeasurableSpace V₂] [BorelSpace V₂]
variable (ν : MeasureTheory.ProbabilityMeasure V₁) (T : V₁ ≃L[ℝ] V₂)
variable [CompleteSpace V₁] [SecondCountableTopology V₁] [CompleteSpace V₂] [SecondCountableTopology V₂]
variable [FiniteDimensional ℝ V₁] [FiniteDimensional ℝ V₂]
omit [CompleteSpace V₁] [CompleteSpace V₂] [FiniteDimensional ℝ V₁]

Formal statement


theorem FunctionalInequalities.Probability.affineSupport_mapContinuousLinearEquiv_readable :
    affineSupport (mapContinuousLinearEquiv ν T) = (affineSupport ν).map (T : V₁ →ₗ[ℝ] V₂).toAffineMap := by sorry

Source

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

View graph