Prove2Me

Self-Adjoint Coordinate Expansion

Proved
FunctionalInequalities.KLS.BKL.Localization.sum_inner_inverseSqrt_sq_readable

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

functional-inequalitieskls-conjecturekls-modularkls-readablelog-concave

This is the coordinate expansion of a quadratic form for a self-adjoint operator.

Let σ:Rn→Rn\sigma:\mathbb{R}^n\to\mathbb{R}^n be a continuous linear map satisfying

⟨σu,v⟩=⟨u,σv⟩\langle\sigma u,v\rangle=\langle u,\sigma v\rangle

for all u,v∈Rnu,v\in\mathbb{R}^n. Then, for every v∈Rnv\in\mathbb{R}^n,

∑k⟨σek,v⟩2=⟨v,σ(σv)⟩,\sum_k\langle\sigma e_k,v\rangle^2 =\langle v,\sigma(\sigma v)\rangle,

where eke_k are the Euclidean coordinate basis vectors. This elementary identity is used to rewrite sums involving the inverse square root of a covariance operator.

Original Lean declaration header

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

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

Module navigation

Module: KLS/BKL/Localization/LogLaplaceGenerator.

Previous: sum_bilin_inverseSqrt_eq · Next: generator_posteriorExpectation_exp_inner.

Source excerpt, lines 143–146 · 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_inner_inverseSqrt_sq_readable (σ : EuclideanSpace ℝ (Fin n) →L[ℝ] EuclideanSpace ℝ (Fin n))
    (hσ : ∀ u v, ⟪σ u, v⟫ = ⟪u, σ v⟫) (v : EuclideanSpace ℝ (Fin n)) :
    ∑ k, ⟪σ (EuclideanSpace.single k 1), v⟫ * ⟪σ (EuclideanSpace.single k 1), v⟫ =
      ⟪v, σ (σ v)⟫ := by sorry
Source
Lean source: https://github.com/human-ai-mathematics/kls-lean/blob/408915f/formalization/FunctionalInequalities/KLS/BKL/Localization/LogLaplaceGenerator.lean#L142-L158 (repository human-ai-mathematics/kls-lean, commit 408915f, module `FunctionalInequalities.KLS.BKL.Localization.LogLaplaceGenerator`, declaration `FunctionalInequalities.KLS.BKL.Localization.sum_inner_inverseSqrt_sq`; the repository is private at upload time).

View graph