Weighted Tests as Covariance-Gradient Tests

Proved

FunctionalInequalities.Energy.CovarianceGradient.weightedTest_iff_exists_test_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This characterizes weighted-gradient tests as covariance-gradient tests.

Let $V$ be a complete real inner-product space with its measurable structure, let $\nu$ be a probability measure on $V$ , and let $B:V\to V$ be a continuous linear map. Assume that for every $v\in V$ ,

\langle \operatorname{Cov}(\nu)v,v\rangle=\|Bv\|^2.

Then for every function $g:V\to\mathbb R$ ,

\operatorname{IsTest}(\nu,B,g) \quad\Longleftrightarrow\quad \exists f\in\operatorname{Test}(\nu),\ f=g.

Here IsTest ν B g is the weighted-gradient test condition and Test ν is the covariance-gradient test class.

The equivalence transfers between the two test descriptions whenever the covariance quadratic form is represented by the squared norm of $B$ .

Formalization Note No finite-dimensionality assumption is required by this declaration.

Original Lean declaration header

Within namespace FunctionalInequalities.Energy.CovarianceGradient. Shown in its original module context. Proof omitted.

theorem weightedTest_iff_exists_test
    (hB : ∀ v, inner ℝ (Covariance.operator (ν : Measure V) v) v = ‖B v‖ ^ 2) (g : V → ℝ) :
    IsTest ν B g ↔ ∃ f : Test ν, f.toFun = g

Module navigation

Module: Energy/WeightedGradient/Basic.

Definition modules: Probability/Covariance/Basic, Energy/CovarianceGradient/Basic.

Next: relaxation_eq_ofLinearPMap.

Source excerpt, lines 310–312 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_Energy_WeightedGradient_Basic

open MeasureTheory Filter Topology InnerProductSpace
universe u
variable {V : Type u} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V]
variable [MeasurableSpace V] (ν : MeasureTheory.ProbabilityMeasure V) (B : V →L[ℝ] V)
variable [BorelSpace V] [SecondCountableTopology V] [FiniteDimensional ℝ V]
  {m : MeasureTheory.Measure V} [m.IsAddHaarMeasure]
open FunctionalInequalities.Energy.WeightedGradient
omit [FiniteDimensional ℝ V]

Formal statement


theorem FunctionalInequalities.Energy.CovarianceGradient.weightedTest_iff_exists_test_readable
    (hB : ∀ v, inner ℝ (Covariance.operator (ν : Measure V) v) v = ‖B v‖ ^ 2) (g : V → ℝ) :
    IsTest ν B g ↔ ∃ f : Test ν, f.toFun = g := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Energy/WeightedGradient/Basic.lean#L308-L323 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Energy.WeightedGradient.Basic`, declaration `FunctionalInequalities.Energy.CovarianceGradient.weightedTest_iff_exists_test`; the repository is private at upload time).

View graph