Rayleigh maps between Poincaré test families

Definition

KLSModular_FunctionalInequalities_Poincare_Comparison

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

A Poincare.TestFamily.RayleighMap from a test family F to a test family G consists of a function sending each F-test to a G-test such that variance does not decrease and energy does not increase. Consequently, the image test has a Rayleigh quotient at least as large as the original one; all comparisons are stated directly in ENNReal, with no nonzero-energy hypothesis.

Original module imports

import FunctionalInequalities.Poincare.SmoothTest.Optimal

Original declaration excerpt

Shown in the original module context.

structure RayleighMap (F : TestFamily.{u}) (G : TestFamily.{v}) where
  /-- The image test. -/
  toFun : F.Test → G.Test
  /-- Variance does not decrease under the map. -/
  variance_le : ∀ f, F.variance f ≤ G.variance (toFun f)
  /-- Energy does not increase under the map. -/
  energy_le : ∀ f, G.energy (toFun f) ≤ F.energy f

Module navigation

Direct project imports: Poincare/SmoothTest/Optimal.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Poincare.Comparison · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Poincare_SmoothTest_Optimal

noncomputable section
namespace FunctionalInequalities
namespace Poincare
namespace TestFamily
universe u v
/-- A map from `F`-tests to `G`-tests that can only increase their Rayleigh quotients. -/
structure RayleighMap (F : TestFamily.{u}) (G : TestFamily.{v}) where
  /-- The image test. -/
  toFun : F.Test → G.Test
  /-- Variance does not decrease under the map. -/
  variance_le : ∀ f, F.variance f ≤ G.variance (toFun f)
  /-- Energy does not increase under the map. -/
  energy_le : ∀ f, G.energy (toFun f) ≤ F.energy f
namespace RayleighMap
variable {F : TestFamily.{u}} {G : TestFamily.{v}}
instance : CoeFun (RayleighMap F G) fun _ ↦ F.Test → G.Test :=
  ⟨RayleighMap.toFun⟩
end RayleighMap
end TestFamily
end Poincare
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Poincare/Comparison.lean#L19-L33 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Poincare.Comparison`, definition bundle `KLSModular_FunctionalInequalities_Poincare_Comparison`; the repository is private at upload time).

View graph