Admissibility Under a Linear Isometry Equivalence

Proved

FunctionalInequalities.Poincare.SmoothTest.admissible_map_linearIsometryEquiv_iff_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the exact test-domain correspondence for a linear isometry equivalence.

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 $f:F\to\mathbb R$ . Then

\operatorname{Admissible}(e_*\mu,f) \iff \operatorname{Admissible}(\mu,f\circ e),

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

This result allows the smooth admissible test class to be transferred in either direction across an isometric change of variables.

Formalization Note: Admissible is the repository's fixed smooth test-domain predicate. The measure transport is μ.map e, and the equivalence is used together with its inverse.

Original Lean declaration header

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

theorem admissible_map_linearIsometryEquiv_iff {f : F → ℝ} :
    Admissible (μ.map e) f ↔ Admissible μ (f ∘ e)

Module navigation

Module: Poincare/SmoothTest/Transport.

Definition modules: Poincare/SmoothTest/Basic.

Supporting theorems: gradient_comp_projection.

Previous: gradient_comp_projection · Next: holds_map_linearIsometryEquiv_iff.

Source excerpt, lines 152–153 · 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.admissible_map_linearIsometryEquiv_iff_readable {f : F → ℝ} :
    Admissible (μ.map e) f ↔ Admissible μ (f ∘ e) := by sorry

Source

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

View graph