Block decompositions of finite-dimensional von Neumann algebras and algebraic (relative) entropy (Harlow TASI §5.3)

Definition

HarlowTASI_OperatorAlgebras

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

holographyoperator-algebrasquantum-error-correctionquantum-information

Vocabulary of §5.3 of Harlow's lectures: von Neumann algebras on a finite-dimensional Hilbert space, their block decomposition, and the algebraic entropy and relative entropy of a state on such an algebra.

A von Neumann algebra on $\mathcal H=\mathbb C^{C}$ (Definition 5.3: closed under products, sums and adjoints, and containing every $\lambda I$ ) is a $*$ -subalgebra $M$ of the $C\times C$ complex matrices; its commutant $M'$ (Definition 5.4) is the set of matrices commuting with all of $M$ , and its center is $Z_M=M\cap M'$ (Definition 5.5).

A block decomposition $\mathcal H\cong\bigoplus_{\alpha}\big(\mathcal H_{r_\alpha}\otimes\mathcal H_{\overline r_\alpha}\big)$ , eq. (5.12), is encoded by a number $N$ of blocks, dimensions $d_{r_\alpha},d_{\overline r_\alpha}$ , and a unitary $U:\mathcal H\to\bigoplus_\alpha\mathbb C^{d_{r_\alpha}}\otimes\mathbb C^{d_{\overline r_\alpha}}$ . Transported back by $U$ we get the three sets of eq. (5.13):

\textstyle\bigoplus_\alpha\mathcal L(\mathcal H_{r_\alpha})\otimes I_{\overline r_\alpha},\qquad \bigoplus_\alpha I_{r_\alpha}\otimes\mathcal L(\mathcal H_{\overline r_\alpha}),\qquad \bigoplus_\alpha\lambda_\alpha I_{r_\alpha\overline r_\alpha}.

For a state $\rho$ on $\mathcal H$ , write the diagonal blocks of $U\rho U^\dagger$ as $p_\alpha\rho_{r_\alpha\overline r_\alpha}$ with $p_\alpha=\mathrm{Tr}$ of the block, eq. (5.15), and set $\rho_{r_\alpha}=\mathrm{Tr}_{\overline r_\alpha}\rho_{r_\alpha\overline r_\alpha}$ , $\rho_{\overline r_\alpha}=\mathrm{Tr}_{r_\alpha}\rho_{r_\alpha\overline r_\alpha}$ . For $M=\bigoplus_\alpha\mathcal L(\mathcal H_{r_\alpha})\otimes I_{\overline r_\alpha}$ the algebraic entropy (5.16) and algebraic relative entropy (5.18) are

S(\rho,M)=-\sum_\alpha p_\alpha\log p_\alpha+\sum_\alpha p_\alpha S(\rho_{r_\alpha}),\qquad S(\rho|\sigma,M)=\sum_\alpha p^{\{\rho\}}_\alpha\log\frac{p^{\{\rho\}}_\alpha}{p^{\{\sigma\}}_\alpha}+\sum_\alpha p^{\{\rho\}}_\alpha S(\rho_{r_\alpha}|\sigma_{r_\alpha}),

and the same formulas with $\overline r_\alpha$ in place of $r_\alpha$ give $S(\rho,M')$ and $S(\rho|\sigma,M')$ .

These definitions are the language of Theorem 5.1 and of the entanglement wedge reconstruction theorem (Theorem 5.2).

Formalization Note Blocks are indexed by Fin N with block dimensions given by functions Fin N → ℕ. When $p_\alpha=0$ the normalized block state is the zero matrix and contributes nothing. The classical term $p\log(p/q)$ is $0$ for $p=0$ and $+\infty$ for $p\neq0=q$ ; relative entropies are valued in EReal. The entropies are defined relative to a chosen block decomposition $U$ ; since the value does not depend on the choice, every statement using them quantifies over an arbitrary decomposition realizing the given algebra.

Definition code

import Mathlib
import Definitions.Def_HarlowTASI_QuantumBasics

/-!
# Harlow, TASI Lectures — von Neumann algebras on finite-dimensional spaces and their entropies

A von Neumann algebra on the finite-dimensional space `ℂ^C` in the sense of Definition 5.3
(closed under products, sums, adjoints, and containing all `λ I`) is a
`StarSubalgebra ℂ (Matrix C C ℂ)`; its commutant `M'` (Definition 5.4) is
`StarSubalgebra.centralizer ℂ M` and its center `Z_M = M ∩ M'` (Definition 5.5) is
`M ⊓ StarSubalgebra.centralizer ℂ M`.

A block decomposition (5.12) `H = ⊕_α (H_{r_α} ⊗ H_{r̄_α})` is encoded by a number `N` of
blocks, block dimensions `dr α = dim H_{r_α}`, `drb α = dim H_{r̄_α}`, and a unitary
`U : H → ⊕_α (ℂ^{dr α} ⊗ ℂ^{drb α})`. The algebraic entropies (5.16) and (5.18) are computed
from the diagonal blocks (5.15) of a state in such a decomposition.
-/

namespace HarlowTASI

open Matrix
open scoped Kronecker ComplexOrder

noncomputable section

/-- Index type of `⊕_{α < N} (ℂ^{dr α} ⊗ ℂ^{drb α})`. -/
abbrev BlockIndex (N : ℕ) (dr drb : Fin N → ℕ) : Type :=
  Σ a : Fin N, Fin (dr a) × Fin (drb a)

variable {N : ℕ} {dr drb : Fin N → ℕ}

/-- The block-diagonal operator `⊕_α (x_α ⊗ I_{r̄_α})`. -/
def blockLeftOp (x : ∀ a, Matrix (Fin (dr a)) (Fin (dr a)) ℂ) :
    Matrix (BlockIndex N dr drb) (BlockIndex N dr drb) ℂ :=
  blockDiagonal' fun a => x a ⊗ₖ (1 : Matrix (Fin (drb a)) (Fin (drb a)) ℂ)

/-- The block-diagonal operator `⊕_α (I_{r_α} ⊗ y_α)`. -/
def blockRightOp (y : ∀ a, Matrix (Fin (drb a)) (Fin (drb a)) ℂ) :
    Matrix (BlockIndex N dr drb) (BlockIndex N dr drb) ℂ :=
  blockDiagonal' fun a => (1 : Matrix (Fin (dr a)) (Fin (dr a)) ℂ) ⊗ₖ y a

/-- The block-diagonal operator `⊕_α λ_α I_{r_α r̄_α}`. -/
def blockScalarOp (c : Fin N → ℂ) : Matrix (BlockIndex N dr drb) (BlockIndex N dr drb) ℂ :=
  blockDiagonal' fun a => c a • (1 : Matrix (Fin (dr a) × Fin (drb a)) (Fin (dr a) × Fin (drb a)) ℂ)

variable {C : Type} [Fintype C] [DecidableEq C]

/-- `⊕_α L(H_{r_α}) ⊗ I_{r̄_α}`, transported to `ℂ^C` by the unitary `U`:
the set of all `U† (⊕_α x_α ⊗ I) U`. -/
def blockAlgebraLeft (U : Matrix (BlockIndex N dr drb) C ℂ) : Set (Matrix C C ℂ) :=
  {X | ∃ x : ∀ a, Matrix (Fin (dr a)) (Fin (dr a)) ℂ, X = Uᴴ * blockLeftOp (drb := drb) x * U}

/-- `⊕_α I_{r_α} ⊗ L(H_{r̄_α})`, transported to `ℂ^C` by `U`. -/
def blockAlgebraRight (U : Matrix (BlockIndex N dr drb) C ℂ) : Set (Matrix C C ℂ) :=
  {X | ∃ y : ∀ a, Matrix (Fin (drb a)) (Fin (drb a)) ℂ, X = Uᴴ * blockRightOp (dr := dr) y * U}

/-- `⊕_α λ_α I_{r_α r̄_α}`, transported to `ℂ^C` by `U`. -/
def blockAlgebraCenter (U : Matrix (BlockIndex N dr drb) C ℂ) : Set (Matrix C C ℂ) :=
  {X | ∃ c : Fin N → ℂ, X = Uᴴ * blockScalarOp (dr := dr) (drb := drb) c * U}

/-- The diagonal block `ρ_{r_α r̄_α, r_α r̄_α}` (unnormalized, i.e. `p_α ρ_{r_α r̄_α}` in (5.15))
of the operator `U ρ U†`. -/
def diagBlock (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ : Matrix C C ℂ) (a : Fin N) :
    Matrix (Fin (dr a) × Fin (drb a)) (Fin (dr a) × Fin (drb a)) ℂ :=
  (U * ρ * Uᴴ).submatrix
    (Sigma.mk (β := fun b => Fin (dr b) × Fin (drb b)) a)
    (Sigma.mk (β := fun b => Fin (dr b) × Fin (drb b)) a)

/-- The block probability `p_α = Tr (diagonal block α)` (real part). -/
def blockWeight (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ : Matrix C C ℂ) (a : Fin N) : ℝ :=
  (diagBlock U ρ a).trace.re

/-- `ρ_{r_α} = Tr_{r̄_α} ρ_{r_α r̄_α}` with `ρ_{r_α r̄_α} = p_α⁻¹ · (diagonal block α)`
(the zero matrix when `p_α = 0`). -/
def blockStateLeft (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ : Matrix C C ℂ) (a : Fin N) :
    Matrix (Fin (dr a)) (Fin (dr a)) ℂ :=
  ((blockWeight U ρ a : ℂ))⁻¹ • traceRight (diagBlock U ρ a)

/-- `ρ_{r̄_α} = Tr_{r_α} ρ_{r_α r̄_α}` (the zero matrix when `p_α = 0`). -/
def blockStateRight (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ : Matrix C C ℂ) (a : Fin N) :
    Matrix (Fin (drb a)) (Fin (drb a)) ℂ :=
  ((blockWeight U ρ a : ℂ))⁻¹ • traceLeft (diagBlock U ρ a)

/-- Algebraic entropy (5.16) of `ρ` on `M = U† (⊕_α L(H_{r_α}) ⊗ I) U`:
`S(ρ, M) = -∑_α p_α log p_α + ∑_α p_α S(ρ_{r_α})`. -/
def algebraicEntropyLeft (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ : Matrix C C ℂ) : ℝ :=
  ∑ a, Real.negMulLog (blockWeight U ρ a) +
    ∑ a, blockWeight U ρ a * vonNeumannEntropy (blockStateLeft U ρ a)

/-- Algebraic entropy of `ρ` on the commutant `M' = U† (⊕_α I ⊗ L(H_{r̄_α})) U`:
`S(ρ, M') = -∑_α p_α log p_α + ∑_α p_α S(ρ_{r̄_α})`. -/
def algebraicEntropyRight (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ : Matrix C C ℂ) : ℝ :=
  ∑ a, Real.negMulLog (blockWeight U ρ a) +
    ∑ a, blockWeight U ρ a * vonNeumannEntropy (blockStateRight U ρ a)

/-- The classical term `p log (p / q)` of (5.18) in the extended reals:
`0` if `p = 0`, `+∞` if `p ≠ 0 = q`, and `p log (p/q)` otherwise. -/
def classicalRelTerm (p q : ℝ) : EReal :=
  if p = 0 then 0 else if q = 0 then ⊤ else ((p * Real.log (p / q) : ℝ) : EReal)

/-- Algebraic relative entropy (5.18) on `M = U† (⊕_α L(H_{r_α}) ⊗ I) U`:
`S(ρ|σ, M) = ∑_α p_α^ρ log (p_α^ρ / p_α^σ) + ∑_α p_α^ρ S(ρ_{r_α} | σ_{r_α})`. -/
def algebraicRelEntropyLeft (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ σ : Matrix C C ℂ) :
    EReal :=
  ∑ a, classicalRelTerm (blockWeight U ρ a) (blockWeight U σ a) +
    ∑ a, ((blockWeight U ρ a : ℝ) : EReal) *
      relativeEntropy (blockStateLeft U ρ a) (blockStateLeft U σ a)

/-- Algebraic relative entropy on the commutant `M' = U† (⊕_α I ⊗ L(H_{r̄_α})) U`. -/
def algebraicRelEntropyRight (U : Matrix (BlockIndex N dr drb) C ℂ) (ρ σ : Matrix C C ℂ) :
    EReal :=
  ∑ a, classicalRelTerm (blockWeight U ρ a) (blockWeight U σ a) +
    ∑ a, ((blockWeight U ρ a : ℝ) : EReal) *
      relativeEntropy (blockStateRight U ρ a) (blockStateRight U σ a)

end

end HarlowTASI

Source

Daniel Harlow, TASI Lectures on the Emergence of Bulk Physics in AdS/CFT, PoS(TASI2017)002 (2018), arXiv:1802.01040, §5.3 (pp. 43–45): Definitions 5.3–5.5, eqs. (5.12)–(5.13) of Theorem 5.1, eqs. (5.15), (5.16), (5.18).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) - NON-BLIND: same agent that drafted the statements

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source lectures and of the intended meaning. It was not produced blind by an independent auditor, so it must not be mistaken for independent testimony; reviewers should treat it as the drafter's own rendering of the code and check the Lean text directly.

This file builds on the basic quantum definitions (partial traces $\mathrm{Tr}_{\overline r},\mathrm{Tr}_r$ , entropy $S(\cdot)$ , relative entropy $S(\cdot|\cdot)$ as defined there). Fix $N\in\mathbb N$ and functions $d_r,d_{\overline r}:\{0,\dots,N-1\}\to\mathbb N$ .

Block index set. $\mathcal B=\{(\alpha,i,j):\alpha<N,\ i<d_r(\alpha),\ j<d_{\overline r}(\alpha)\}$ ; matrices indexed by $\mathcal B$ are operators on $\bigoplus_\alpha\mathbb C^{d_r(\alpha)}\otimes\mathbb C^{d_{\overline r}(\alpha)}$ .
Block operators. Given matrices $x_\alpha$ of size $d_r(\alpha)$ : $\mathrm{L}(x)=\bigoplus_\alpha (x_\alpha\otimes I_{d_{\overline r}(\alpha)})$ (block diagonal, zero off the diagonal blocks). Given $y_\alpha$ of size $d_{\overline r}(\alpha)$ : $\mathrm{R}(y)=\bigoplus_\alpha(I_{d_r(\alpha)}\otimes y_\alpha)$ . Given scalars $c_\alpha\in\mathbb C$ : $\mathrm{Z}(c)=\bigoplus_\alpha c_\alpha I$ .
Transported sets. For a finite set $C$ and a matrix $U$ with rows indexed by $\mathcal B$ and columns by $C$ (no unitarity is assumed in these definitions): $\mathcal A_L(U)=\{U^\dagger\mathrm L(x)U\}$ , $\mathcal A_R(U)=\{U^\dagger\mathrm R(y)U\}$ , $\mathcal A_Z(U)=\{U^\dagger\mathrm Z(c)U\}$ , each ranging over all choices of $x$ , $y$ , $c$ respectively; these are sets of $C\times C$ matrices.
Diagonal block and weight. For a $C\times C$ matrix $\rho$ and $\alpha<N$ : $B_\alpha(\rho)$ is the $(\alpha,\alpha)$ diagonal block of $U\rho U^\dagger$ (a matrix indexed by pairs $(i,j)$ ), and $p_\alpha(\rho)=\operatorname{Re}\mathrm{Tr}\,B_\alpha(\rho)$ .
Block states. $\rho_{r_\alpha}=p_\alpha(\rho)^{-1}\,\mathrm{Tr}_{\overline r}B_\alpha(\rho)$ and $\rho_{\overline r_\alpha}=p_\alpha(\rho)^{-1}\,\mathrm{Tr}_{r}B_\alpha(\rho)$ , with the convention $0^{-1}=0$ (so they are the zero matrix when $p_\alpha(\rho)=0$ ).
Algebraic entropies (real numbers).

S_L(\rho)=\sum_\alpha\big(-p_\alpha\log p_\alpha\big)+\sum_\alpha p_\alpha\,S(\rho_{r_\alpha}),\qquad S_R(\rho)=\sum_\alpha\big(-p_\alpha\log p_\alpha\big)+\sum_\alpha p_\alpha\,S(\rho_{\overline r_\alpha}),

with $p_\alpha=p_\alpha(\rho)$ and $-0\log0=0$ .

Classical term (extended real). $c(p,q)=0$ if $p=0$ ; $=+\infty$ if $p\neq0$ and $q=0$ ; $=p\log(p/q)$ otherwise.
Algebraic relative entropies (extended reals).

S_L(\rho|\sigma)=\sum_\alpha c\big(p_\alpha(\rho),p_\alpha(\sigma)\big)+\sum_\alpha p_\alpha(\rho)\cdot S(\rho_{r_\alpha}|\sigma_{r_\alpha}),

and $S_R(\rho|\sigma)$ the same with $\rho_{\overline r_\alpha},\sigma_{\overline r_\alpha}$ ; here the product of the real number $p_\alpha(\rho)$ with an extended real uses extended-real multiplication (in particular $0\cdot(+\infty)=0$ ).

The file also records, in its header comment only, the convention that a von Neumann algebra on $\mathbb C^C$ is a $*$ -subalgebra (containing the scalars) of the $C\times C$ complex matrices, with commutant the centralizer and center the intersection; these are library notions, not new definitions.

Human review

Endorsed by Shuze Chen · Oct 10, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 10, 2026
Confirmed by the mission captain (proposal self-audit).

View graph