Self-Adjoint Trace Rearrangement

Proved

FunctionalInequalities.KLS.BKL.Localization.sum_bilin_inverseSqrt_eq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is a finite-dimensional trace rearrangement for a self-adjoint operator.

Let $n\in\mathbb N$ , let $B$ be a bilinear form on $\mathbb R^n$ represented on EuclideanSpace ℝ (Fin n), and let $\sigma$ be a continuous linear map on that space. Assume

\langle\sigma u,v\rangle=\langle u,\sigma v\rangle\quad\text{for all }u,v.

Using the standard coordinate vectors $e_k$ , one has

\sum_k B(\sigma e_k,\sigma e_k) =\sum_i B(\sigma^2e_i,e_i).

This technical identity allows a quadratic sum involving an inverse square root to be rewritten as a trace-type expression.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.BKL.Localization. Shown in its original module context. Proof omitted.

theorem sum_bilin_inverseSqrt_eq (B : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ)
    (σ : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hσ : ∀ u v, ⟪σ u, v⟫ = ⟪u, σ v⟫) :
    ∑ k, B (σ (EuclideanSpace.single k 1)) (σ (EuclideanSpace.single k 1)) =
      ∑ i, B (σ (σ (EuclideanSpace.single i 1))) (EuclideanSpace.single i 1)

Module navigation

Module: KLS/BKL/Localization/LogLaplaceGenerator.

Previous: fderiv_fderiv_fst_dir · Next: sum_inner_inverseSqrt_sq.

Source excerpt, lines 100–104 · Frozen source 408915f.

Preamble

import Definitions.Def_KLSModular_FunctionalInequalities_KLS_BKL_Localization_LogLaplaceGenerator

open scoped RealInnerProductSpace
variable {n : ℕ}

Formal statement


theorem FunctionalInequalities.KLS.BKL.Localization.sum_bilin_inverseSqrt_eq_readable (B : EuclideanSpace ℝ (Fin n) →ₗ[ℝ] EuclideanSpace ℝ (Fin n) →ₗ[ℝ] ℝ)
    (σ : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hσ : ∀ u v, ⟪σ u, v⟫ = ⟪u, σ v⟫) :
    ∑ k, B (σ (EuclideanSpace.single k 1)) (σ (EuclideanSpace.single k 1)) =
      ∑ i, B (σ (σ (EuclideanSpace.single i 1))) (EuclideanSpace.single i 1) := by sorry

Source

Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/LogLaplaceGenerator.lean#L99-L140 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.LogLaplaceGenerator`, declaration `FunctionalInequalities.KLS.BKL.Localization.sum_bilin_inverseSqrt_eq`; the repository is private at upload time).

View graph