Simplex edge matrix and volume

Definition

KLSModular_FunctionalInequalities_Analysis_Convex_Normalization

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For vertices $v_0,\ldots,v_n\in\mathbb{R}^n$ , simplexEdgeMatrix v is the matrix whose column $j$ is $v_{j+1}-v_0$ , and simplexVolume v is the absolute value of its determinant. The module supplies auxiliary facts about maximal-volume simplices, simplex coordinates, and inclusions between standard simplices, balls, and boxes.

Original module imports

import Mathlib

Original declaration excerpt

Shown in the original module context.

def simplexEdgeMatrix {n : ℕ} (v : Fin (n + 1) → EuclideanSpace ℝ (Fin n)) :
    Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j => (v j.succ - v 0) i

Module navigation

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.Convex.Normalization · Frozen source 408915f.

Definition code

import Mathlib

noncomputable section
open Set Matrix
namespace FunctionalInequalities
namespace Analysis
/-- The edge matrix of a simplex with vertices `v 0, …, v n` in `ℝⁿ`: column `j` is `v (j+1) − v 0`. -/
def simplexEdgeMatrix {n : ℕ} (v : Fin (n + 1) → EuclideanSpace ℝ (Fin n)) :
    Matrix (Fin n) (Fin n) ℝ :=
  Matrix.of fun i j => (v j.succ - v 0) i
 def simplexVolume {n : ℕ} :
    (Fin (n + 1) → EuclideanSpace ℝ (Fin n)) → ℝ :=
  fun v => |(simplexEdgeMatrix v).det|
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/Convex/Normalization.lean#L20-L27 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.Convex.Normalization`, definition bundle `KLSModular_FunctionalInequalities_Analysis_Convex_Normalization`; the repository is private at upload time).

View graph