Affine coordinate maps

Definition

KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Affine

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

affineHomeomorph packages the affine homeomorphism $x\mapsto Lx+c$ associated with a continuous linear equivalence $L$ . inverseAffineEquiv packages its inverse $y\mapsto L^{-1}(y-c)$ as a measurable equivalence. This module provides the coordinate maps themselves; the regularity and measure-transport statements are separate declarations.

Original module imports

import FunctionalInequalities.KLS.LogConcave.Regular.Basic
import FunctionalInequalities.Probability.Transport
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

Original declaration excerpt

Shown in the original module context.

def affineHomeomorph (L : E ≃L[ℝ] E) (c : E) : E ≃ₜ E :=
  L.toHomeomorph.trans (Homeomorph.addRight c)

Module navigation

Direct project imports: KLS/LogConcave/Regular/Basic, Probability/Transport.

Theorems in source order:

RegularPotential.law_comp_affine

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.LogConcave.Regular.Affine · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Basic
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Transport
import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar

open MeasureTheory
open scoped RealInnerProductSpace ContDiff
noncomputable section
namespace FunctionalInequalities
namespace KLS
variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
  [CompleteSpace E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
/-- The affine homeomorphism `x ↦ L x + c`. -/
def affineHomeomorph (L : E ≃L[ℝ] E) (c : E) : E ≃ₜ E :=
  L.toHomeomorph.trans (Homeomorph.addRight c)
/-- The inverse affine map `y ↦ L⁻¹(y − c)` as a measurable equivalence. -/
def inverseAffineEquiv (L : E ≃L[ℝ] E) (c : E) : E ≃ᵐ E :=
  (affineHomeomorph L c).symm.toMeasurableEquiv
end KLS
end FunctionalInequalities
end

Source

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

View graph