Optimal Rayleigh constant for a test family

Definition

KLSModular_FunctionalInequalities_Poincare_SmoothTest_Optimal

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

Poincare.TestFamily records a test type together with finite nonnegative NNReal variance and energy values, without choosing a measure or gradient. rayleigh is the extended quotient $\operatorname{variance}(f)/\operatorname{energy}(f)$ in ENNReal, and constant is the supremum over all tests, so it may be $\top$ . Holds F C means that the finite constant C bounds every variance by C times the corresponding energy.

Original module imports

import Mathlib.Data.ENNReal.Inv

Original declaration excerpt

Shown in the original module context.

structure TestFamily where
  /-- The chosen test domain; it need not contain every ambient function. -/
  Test : Type u
  /-- Finite nonnegative variance assigned to each test. -/
  variance : Test → NNReal
  /-- Finite nonnegative energy assigned to each test; zero is allowed. -/
  energy : Test → NNReal

Module navigation

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Poincare.SmoothTest.Optimal · Frozen source 408915f.

Definition code

import Mathlib.Data.ENNReal.Inv

noncomputable section
namespace FunctionalInequalities
namespace Poincare
universe u
/-- A family of tests whose variance and energy are both finite and nonnegative. -/
structure TestFamily where
  /-- The chosen test domain; it need not contain every ambient function. -/
  Test : Type u
  /-- Finite nonnegative variance assigned to each test. -/
  variance : Test → NNReal
  /-- Finite nonnegative energy assigned to each test; zero is allowed. -/
  energy : Test → NNReal
namespace TestFamily
/-- The extended Rayleigh quotient of a test. -/
def rayleigh (F : TestFamily) (f : F.Test) : ENNReal :=
  (F.variance f : ENNReal) / (F.energy f : ENNReal)
/-- The optimal constant, including infinity when the Rayleigh quotients are unbounded. -/
def constant (F : TestFamily) : ENNReal :=
  ⨆ f, rayleigh F f
/-- A finite constant is valid when it bounds variance by that constant times energy. -/
def Holds (F : TestFamily) (C : NNReal) : Prop :=
  ∀ f, F.variance f ≤ C * F.energy f
end TestFamily
end Poincare
end FunctionalInequalities

Source

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

View graph