Boolean selection of derivative slots

Definition

KLSModular_FunctionalInequalities_Analysis_IteratedDerivative_Bilinear

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

functional-inequalitiesklskls-conjecturekls-modularlog-concavemodule-context

selected h q takes an ordered family $h:\mathrm{Fin}\,m\to E$ and a Boolean mask $q:\mathrm{Fin}\,m\to\mathrm{Bool}$ , retaining precisely the slots for which $q$ is true, in their inherited order. The empty family yields the empty list, and the recursion proceeds through Fin.tail; this is the slot-allocation object used in raw bilinear Leibniz expansions.

Original module imports

import FunctionalInequalities.Analysis.IteratedDerivative.Symmetry
import Mathlib.Analysis.Calculus.FDeriv.Bilinear
import Mathlib.Algebra.BigOperators.Group.Finset.Pi

Original declaration excerpt

Shown in the original module context.

def selected : {m : ℕ} → (Fin m → E) → (Fin m → Bool) → List E
  | 0, _, _ => []
  | _m+1, h, q => if q 0 then h 0 :: selected (Fin.tail h) (Fin.tail q)
      else selected (Fin.tail h) (Fin.tail q)

Module navigation

Direct project imports: Analysis/IteratedDerivative/Symmetry.

Theorems in source order:

Project result: The KLS conjecture.

Original module · FunctionalInequalities.Analysis.IteratedDerivative.Bilinear · Frozen source 408915f.

Definition code

import Definitions.Def_KLSModular_FunctionalInequalities_Analysis_IteratedDerivative_Symmetry
import Mathlib.Analysis.Calculus.FDeriv.Bilinear
import Mathlib.Algebra.BigOperators.Group.Finset.Pi

noncomputable section
open scoped ContDiff
namespace FunctionalInequalities
namespace Analysis
variable {E F G H : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
  [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G]
  [NormedAddCommGroup H] [NormedSpace ℝ H]
/-- Select a subset of the original ordered slots using its Boolean indicator. -/
def selected : {m : ℕ} → (Fin m → E) → (Fin m → Bool) → List E
  | 0, _, _ => []
  | _m+1, h, q => if q 0 then h 0 :: selected (Fin.tail h) (Fin.tail q)
      else selected (Fin.tail h) (Fin.tail q)
end Analysis
end FunctionalInequalities

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/Analysis/IteratedDerivative/Bilinear.lean#L26-L30 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.Analysis.IteratedDerivative.Bilinear`, definition bundle `KLSModular_FunctionalInequalities_Analysis_IteratedDerivative_Bilinear`; the repository is private at upload time).

View graph