Action of a Stein kernel matrix

Definition

KLSModular_FunctionalInequalities_Probability_Stein_Kernel

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a KernelMatrix n $T$ and $v \in \operatorname{EuclideanSpace}(\mathbb{R},\operatorname{Fin} n)$ , action T v is the Euclidean vector obtained by applying the matrix-vector product $T v$ in the underlying $L^2$ representation and converting it back to EuclideanSpace. This is the basic action associated with the Stein-kernel object.

Original module imports

import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.Analysis.Matrix.Normed
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import FunctionalInequalities.L2.Pairing
import FunctionalInequalities.Analysis.BakryEmery.Calculus
import FunctionalInequalities.Analysis.Operator.Coordinates

Original declaration excerpt

Shown in the original module context.

def action {n : ℕ} (T : KernelMatrix n) (v : EuclideanSpace ℝ (Fin n)) : EuclideanSpace ℝ (Fin n) :=
  WithLp.toLp 2 (T.mulVec v.ofLp)

Module navigation

Direct project imports: L2/Pairing, Analysis/BakryEmery/Calculus, Analysis/Operator/Coordinates.

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Probability.Stein.Kernel · Frozen source 408915f.

Definition code

import Mathlib.MeasureTheory.Measure.ProbabilityMeasure
import Mathlib.Analysis.Matrix.Normed
import Mathlib.MeasureTheory.Function.LocallyIntegrable
import Definitions.Def_KLSModular_FunctionalInequalities_L2_Pairing
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Calculus
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Operator_Coordinates

open MeasureTheory Filter
open FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace Topology ContDiff Matrix.Norms.Frobenius
noncomputable section
namespace FunctionalInequalities
namespace Probability
namespace Stein
/-- The action `T v` of a kernel matrix on a Euclidean vector. -/
def action {n : ℕ} (T : KernelMatrix n) (v : EuclideanSpace ℝ (Fin n)) : EuclideanSpace ℝ (Fin n) :=
  WithLp.toLp 2 (T.mulVec v.ofLp)
end Stein
end Probability
end FunctionalInequalities
end

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Probability/Stein/Kernel.lean#L24-L26 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Probability.Stein.Kernel`, definition bundle `KLSModular_FunctionalInequalities_Probability_Stein_Kernel`; the repository is private at upload time).

View graph