Coordinate matrix of a continuous linear operator

Definition

KLSModular_FunctionalInequalities_Analysis_BakryEmery_WeakHessian

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a continuous linear operator $L : \mathbb{R}^n \to \mathbb{R}^n$ , n10_matrix L is the real matrix whose $(r,s)$ entry is the inner product of $L(e_r)$ with the standard basis vector $e_s$ of EuclideanSpace ℝ (Fin n). It is a private coordinate representation used by the weak-Hessian development.

Original module imports

import FunctionalInequalities.Analysis.BakryEmery.HessianOperator
import FunctionalInequalities.Analysis.WeakDerivative.Calculus

Original declaration excerpt

Shown in the original module context.

private def n10_matrix {n : ℕ}
    (L : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) :
    Matrix (Fin n) (Fin n) ℝ :=
  fun r s =>
    (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin n)))
      (L (EuclideanSpace.basisFun (Fin n) ℝ r))
      (EuclideanSpace.basisFun (Fin n) ℝ s)

Module navigation

Direct project imports: Analysis/BakryEmery/HessianOperator, Analysis/WeakDerivative/Calculus.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.BakryEmery.WeakHessian · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_HessianOperator
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_WeakDerivative_Calculus

open MeasureTheory
open FunctionalInequalities.Analysis.BakryEmery
open scoped RealInnerProductSpace ContDiff
noncomputable section HessianEntryBounds
open MeasureTheory
open FunctionalInequalities.Probability.Stein
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace Probability
namespace Stein
 def n10_matrix {n : ℕ}
    (L : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n)) :
    Matrix (Fin n) (Fin n) ℝ :=
  fun r s =>
    (InnerProductSpace.toDual ℝ (EuclideanSpace ℝ (Fin n)))
      (L (EuclideanSpace.basisFun (Fin n) ℝ r))
      (EuclideanSpace.basisFun (Fin n) ℝ s)
end Stein
end Probability
end FunctionalInequalities
end HessianEntryBounds

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/BakryEmery/WeakHessian.lean#L352-L358 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.BakryEmery.WeakHessian`, definition bundle `KLSModular_FunctionalInequalities_Analysis_BakryEmery_WeakHessian`; the repository is private at upload time).

View graph