Permutation for cumulant slot reindexing

Definition

KLSModular_FunctionalInequalities_KLS_BKL_Localization_CumulantDerivative

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

The private definition snocToCons m is a permutation of Fin (m+1) that moves the final slot to the first position and shifts the preceding slots, with explicit inverse and left/right inverse proofs. It is a technical reindexing device for parameter derivatives of posterior cumulants; the module's public cumulant-derivative statements are not included in this declaration bundle.

Original module imports

import FunctionalInequalities.KLS.BKL.Localization.Coefficients
import FunctionalInequalities.Probability.Posterior.LogPartition
import FunctionalInequalities.Analysis.BakryEmery.Cumulant.Local

Original declaration excerpt

Shown in the original module context. Body omitted.

private def snocToCons (m : ℕ) : Equiv.Perm (Fin (m + 1))

Module navigation

Direct project imports: KLS/BKL/Localization/Coefficients, Probability/Posterior/LogPartition, Analysis/BakryEmery/Cumulant/Local.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.KLS.BKL.Localization.CumulantDerivative · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_Coefficients
import Definitions.Def_KLSModular_FunctionalInequalities_Probability_Posterior_LogPartition
import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_BakryEmery_Cumulant_Local

noncomputable section
open MeasureTheory
open scoped RealInnerProductSpace ContDiff
open FunctionalInequalities.Probability.Posterior FunctionalInequalities.Analysis
  FunctionalInequalities.Analysis.BakryEmery
namespace FunctionalInequalities
namespace KLS
namespace BKL
namespace Localization
 def snocToCons (m : ℕ) : Equiv.Perm (Fin (m + 1)) :=
  Equiv.mk
    (Fin.cases (Fin.last m) (fun i => i.castSucc))
    (Fin.lastCases 0 (fun i => i.succ))
    (by
      intro i
      refine Fin.cases ?_ (fun j => ?_) i
      · simp
      · simp)
    (by
      intro i
      refine Fin.lastCases ?_ (fun j => ?_) i
      · simp
      · simp)
variable {n : ℕ} (μ : ProbabilityMeasure (EuclideanSpace ℝ (Fin n)))
  (hc : IsCompact (μ : Measure (EuclideanSpace ℝ (Fin n))).support)
end Localization
end BKL
end KLS
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/CumulantDerivative.lean#L53-L66 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.CumulantDerivative`, definition bundle `KLSModular_FunctionalInequalities_KLS_BKL_Localization_CumulantDerivative`; the repository is private at upload time).

View graph