Coordinate-tensor relabelling

Definition

KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_TaylorRecursion

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

The private definition recast relabels the index positions of a coordinate tensor when natural numbers $N$ and $N'$ are identified by an equality $h : N = N'$ . For a tensor $A : \mathrm{Coord}(n,N)$ , it produces an element of $\mathrm{Coord}(n,N')$ by precomposing $A$ with Fin.cast h and representing the resulting function in the $L^2$ space using WithLp.toLp 2.

Original module imports

import FunctionalInequalities.KLS.BKL.PoissonIterate.Taylor
import FunctionalInequalities.KLS.BKL.PoissonIterate.Symmetry

Original declaration excerpt

Shown in the original module context.

private def recast {N' : ℕ} (h : N = N') (A : Coord n N) : Coord n N' :=
  WithLp.toLp 2 fun J => A (J ∘ Fin.cast h)

Module navigation

Direct project imports: KLS/BKL/PoissonIterate/Taylor, KLS/BKL/PoissonIterate/Symmetry.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.PoissonIterate.TaylorRecursion · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Taylor
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Symmetry

noncomputable section
open MeasureTheory Finset
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.Analysis.Tensor
open scoped ContDiff
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace PoissonIterate
section Coordinates
variable {n N : ℕ}
/-- Relabelling the index positions of a coordinate tensor along `N = N'`. -/
 def recast {N' : ℕ} (h : N = N') (A : Coord n N) : Coord n N' :=
  WithLp.toLp 2 fun J => A (J ∘ Fin.cast h)
end Coordinates
end PoissonIterate
end LogConcave
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/TaylorRecursion.lean#L163-L165 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.TaylorRecursion`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_TaylorRecursion`; the repository is private at upload time).

View graph