Poincaré Inequality Invariance Under Isometries

Proved

FunctionalInequalities.Poincare.SmoothTest.holds_map_linearIsometryEquiv_iff_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the transport equivalence for the fixed-constant smooth-test Poincaré statement.

Let $E$ and $F$ be complete real inner-product normed spaces equipped with measurable Borel structures. Let $e:E\simeq F$ be a linear isometry equivalence, let $\mu$ be a probability measure on $E$ , and let $C\in\mathbb R$ . Then

\operatorname{Holds}(e_*\mu,C) \iff \operatorname{Holds}(\mu,C),

where $e_*\mu=\operatorname{Measure.map}(e,\mu)$ .

The declaration records that the repository's smooth-test Poincaré inequality with constant $C$ is unchanged by a linear isometric equivalence of the underlying space.

Formalization Note: Holds is the fixed-constant predicate used by the smooth-test Poincaré development. The statement is an iff and does not identify Holds with a closed Dirichlet-form domain.

Original Lean declaration header

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

theorem holds_map_linearIsometryEquiv_iff {C : ℝ} :
    Holds (μ.map e) C ↔ Holds μ C

Module navigation

Module: Poincare/SmoothTest/Transport.

Definition modules: Poincare/SmoothTest/Basic.

Supporting theorems: admissible_map_linearIsometryEquiv_iff, gradient_comp_projection.

Previous: admissible_map_linearIsometryEquiv_iff.

Source excerpt, lines 189–190 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_SmoothTest_Transport

variable {E F : Type*}
  [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E]
  [NormedAddCommGroup F] [InnerProductSpace ℝ F] [CompleteSpace F]
variable [MeasurableSpace E] [BorelSpace E] [MeasurableSpace F] [BorelSpace F]
variable (e : E ≃ₗᵢ[ℝ] F) (μ : MeasureTheory.Measure E) [MeasureTheory.IsProbabilityMeasure μ]

Formal statement


theorem FunctionalInequalities.Poincare.SmoothTest.holds_map_linearIsometryEquiv_iff_readable {C : ℝ} :
    Holds (μ.map e) C ↔ Holds μ C := by sorry

Source

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

View graph