Entrywise Formula for Partial Symmetrization

Proved

FunctionalInequalities.KLS.LogConcave.PoissonIterate.symmetrize_apply_comp_cast_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

Let $N,q,r,n\in\mathbb N$ with $N=q+r$ , let $A$ be an $N$ -index coordinate tensor over an $n$ -element coordinate space, and let $J:\mathrm{Fin}(N)\to\mathrm{Fin}(n)$ . Then the entry of the symmetrization over the first $q$ positions is the average over permutations of those positions, while the last $r$ positions remain fixed:

S_qA(J)=\frac1{q!}\sum_{\tau\in\operatorname{Perm}(q)} A\bigl(J\circ(\tau\text{ on the first }q\text{ slots})\,\text{ followed by }J\text{ on the last }r\text{ slots}\bigr).

The equality includes the necessary cast from the equality $N=q+r$ and is an entrywise coordinate identity. It is used to expand symmetrized Taylor fields.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.PoissonIterate. Shown in its original module context. Proof omitted.

theorem symmetrize_apply_comp_cast {n N q r : ℕ} (h : N = q + r) (A : Coord n N)
    (J : Fin (q + r) → Fin n) :
    symmetrize n N q A (J ∘ Fin.cast h) =
      (q.factorial : ℝ)⁻¹ * ∑ τ : Equiv.Perm (Fin q),
        A (Fin.append (J ∘ Fin.castAdd r ∘ τ) (J ∘ Fin.natAdd q) ∘ Fin.cast h)

Module navigation

Module: KLS/BKL/PoissonIterate/Taylor.

Definition modules: Analysis/Tensor/Coordinate.

Previous: taylorTensor_center · Next: taylorTensor_gen_apply.

Source excerpt, lines 201–205 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_PoissonIterate_Taylor

open FunctionalInequalities.Analysis.Tensor

Formal statement


theorem FunctionalInequalities.KLS.LogConcave.PoissonIterate.symmetrize_apply_comp_cast_readable {n N q r : ℕ} (h : N = q + r) (A : Coord n N)
    (J : Fin (q + r) → Fin n) :
    symmetrize n N q A (J ∘ Fin.cast h) =
      (q.factorial : ℝ)⁻¹ * ∑ τ : Equiv.Perm (Fin q),
        A (Fin.append (J ∘ Fin.castAdd r ∘ τ) (J ∘ Fin.natAdd q) ∘ Fin.cast h) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/PoissonIterate/Taylor.lean#L199-L216 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.PoissonIterate.Taylor`, declaration `FunctionalInequalities.KLS.LogConcave.PoissonIterate.symmetrize_apply_comp_cast`; the repository is private at upload time).

View graph