Extension of a permutation on tensor slots

Definition

KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Taylor

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

For permutations $τ$ of the first $q$ positions and natural numbers $q,r$ , extendPerm τ is the permutation of Fin (q+r) that acts by $τ$ on the first $q$ slots and by the identity on the remaining $r$ slots. It is a private indexing helper for the Taylor-field and Poisson-iterate identities described in the module.

Original module imports

import FunctionalInequalities.KLS.BKL.PoissonIterate.Domain
import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Tilt
import FunctionalInequalities.KLS.LogConcave.HeatSemigroup.Temperate

Original declaration excerpt

Shown in the original module context.

private def extendPerm {q r : ℕ} (τ : Equiv.Perm (Fin q)) : Equiv.Perm (Fin (q + r)) :=
  finSumFinEquiv.permCongr (Equiv.Perm.sumCongr τ 1)

Module navigation

Direct project imports: KLS/BKL/PoissonIterate/Domain, KLS/LogConcave/HeatSemigroup/Tilt, KLS/LogConcave/HeatSemigroup/Temperate.

Theorems in source order:

Project result: The KLS conjecture.

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

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Domain
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Tilt
import Definitions.Def_KLSModular_FunctionalInequalities_KLS_LogConcave_HeatSemigroup_Temperate

noncomputable section
open MeasureTheory
open FunctionalInequalities.Analysis.Semigroup FunctionalInequalities.Analysis.BakryEmery
open FunctionalInequalities.Analysis.Tensor
open scoped RealInnerProductSpace ContDiff
namespace FunctionalInequalities
namespace KLS
namespace LogConcave
namespace PoissonIterate
section Slots
/-- A permutation of the first `q` of `q + r` positions, extended by the identity. -/
 def extendPerm {q r : ℕ} (τ : Equiv.Perm (Fin q)) : Equiv.Perm (Fin (q + r)) :=
  finSumFinEquiv.permCongr (Equiv.Perm.sumCongr τ 1)
end Slots
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/Taylor.lean#L141-L143 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Taylor`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Taylor`; the repository is private at upload time).

View graph