Spatial slice of the suspension space

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Derivatives

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For natural numbers $N,n$ , jointSpatialSlice N n is the continuous linear map from $(\mathbb{R}^n)^N$ into the suspension JointSpace N n that sends the auxiliary coordinate to $0$ and sends the $(i,j)$ spatial coordinate to the $j$ th coordinate of the $i$ th copy. The simp theorems jointSpatialSlice_none and jointSpatialSlice_some state these two coordinate formulas exactly; the module also contains derivative and cumulant auxiliary results for the suspension construction.

Original module imports

import FunctionalInequalities.KLS.BKL.Suspension.Density
import FunctionalInequalities.KLS.BKL.Suspension.Cumulant
import FunctionalInequalities.KLS.LogConcave.Regular.Basic

Original declaration excerpt

Shown in the original module context.

private noncomputable def jointSpatialSlice (N n : ℕ) :
    (Fin N → EuclideanSpace ℝ (Fin n)) →L[ℝ]
      FunctionalInequalities.KLS.LogConcave.Suspension.JointSpace N n :=
  (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Option (Fin N × Fin n) => ℝ)).symm.toContinuousLinearMap.comp
    (ContinuousLinearMap.pi fun o => match o with
      | none => 0
      | some ij => (EuclideanSpace.proj ij.2).comp (ContinuousLinearMap.proj ij.1))

Module navigation

Direct project imports: KLS/BKL/Suspension/Density, KLS/BKL/Suspension/Cumulant, KLS/LogConcave/Regular/Basic.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Suspension.Derivatives · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Density
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Cumulant
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_Regular_Basic

open MeasureTheory FunctionalInequalities FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.Probability.Line
open scoped RealInnerProductSpace
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace Suspension
open FunctionalInequalities.KLS.LogConcave.Suspension
open scoped Topology ContDiff
open FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.KLS.LogConcave.Suspension
open scoped Topology
open FunctionalInequalities
open scoped ContDiff
variable {E F G : Type*}
  [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
  [NormedAddCommGroup G] [NormedSpace ℝ G]
set_option autoImplicit false
open Filter Set
open scoped ContDiff Topology
variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F]
open scoped ContDiff Topology
open Filter Set
variable {E G : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup G] [NormedSpace ℝ G]
/-- Actual spatial slice in the source's joint space: auxiliary coordinate zero, copies intact. -/
 noncomputable def jointSpatialSlice (N n : ℕ) :
    (Fin N → EuclideanSpace ℝ (Fin n)) →L[ℝ]
      FunctionalInequalities.KLS.LogConcave.Suspension.JointSpace N n :=
  (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Option (Fin N × Fin n) => ℝ)).symm.toContinuousLinearMap.comp
    (ContinuousLinearMap.pi fun o => match o with
      | none => 0
      | some ij => (EuclideanSpace.proj ij.2).comp (ContinuousLinearMap.proj ij.1))
@[simp] theorem jointSpatialSlice_none {N n : ℕ} (x : Fin N → EuclideanSpace ℝ (Fin n)) :
    FunctionalInequalities.KLS.LogConcave.Suspension.jointSpatialSlice N n x none = 0 := rfl
@[simp] theorem jointSpatialSlice_some {N n : ℕ} (x : Fin N → EuclideanSpace ℝ (Fin n))
    (i : Fin N) (j : Fin n) : FunctionalInequalities.KLS.LogConcave.Suspension.jointSpatialSlice N n x (some (i, j)) = x i j := rfl
open MeasureTheory FunctionalInequalities FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.KLS.LogConcave.Suspension
open scoped RealInnerProductSpace ContDiff Topology
open MeasureTheory FunctionalInequalities FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.KLS.LogConcave.Suspension
end Suspension
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Suspension/Derivatives.lean#L675-L688 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Suspension.Derivatives`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Suspension_Derivatives`; the repository is private at upload time).

View graph