Coordinate matrix of a continuous linear map

Definition

KLSModular_FunctionalInequalities_Analysis_Matrix_Piola

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For a continuous linear map $L : \mathbb{R}^n \to \mathbb{R}^n$ , the private n10_matrix records the coefficients $\langle L(e_r),e_s\rangle$ in the standard Euclidean basis. It is a coordinate helper for the Piola and inverse-Hessian divergence development, not itself a Piola identity.

Original module imports

import FunctionalInequalities.Analysis.Matrix.WeakDerivative
import FunctionalInequalities.Analysis.BakryEmery.HessianOperator
import FunctionalInequalities.Analysis.Matrix.DeterminantDerivative
import FunctionalInequalities.Analysis.Mollification.Hessian
import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
import Mathlib.Analysis.Calculus.Rademacher

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/Matrix/WeakDerivative, Analysis/BakryEmery/HessianOperator, Analysis/Matrix/DeterminantDerivative, Analysis/Mollification/Hessian.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Matrix.Piola · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_WeakDerivative
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_HessianOperator
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Matrix_DeterminantDerivative
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_Mollification_Hessian
import Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
import Mathlib.Analysis.Calculus.Rademacher

noncomputable section
open Matrix
open FunctionalInequalities.Probability.Stein
section LN10AInverseHessianDivergence
open MeasureTheory Set Filter
open scoped Topology
open FunctionalInequalities.Probability.Stein
namespace FunctionalInequalities
namespace Analysis
section StructuredSpace
variable {E : Type*}
variable [NormedAddCommGroup E]
 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 StructuredSpace
end Analysis
end FunctionalInequalities
end LN10AInverseHessianDivergence

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Matrix/Piola.lean#L641-L647 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Matrix.Piola`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Matrix_Piola`; the repository is private at upload time).

View graph