Definitions for Entanglement Renyi entropies in holographic theories

Definition

QAlgorithms_Papers_Independent_Intakethird100_P41

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

The objects the formalized statements of Entanglement Renyi entropies in holographic theories (arXiv:1006.0047) are stated in. Each was checked against the paper by a blind read-back and a moderator.

densityPerturbation: PDF p.7, (2.8): the affine density-operator perturbation, with real parameter.
IsSupportPreservingPerturbation: PDF p.7: normalized Hermitian perturbations with unchanged occupied support for small real parameters of both signs. For Hermitian finite matrices, the kernel condition on rho1 is equivalent to image(rho1) being contained in image(rho0). The final condition states equality of occupied supports near zero, rather than assuming an entropy formula.
occupiedPower: PDF pp.5,7: spectral powers on occupied support, extended by zero on the kernel. In particular a negative exponent never assigns an infinite value to a zero eigenvalue.
regulatedRenyiNats: PDF p.5, (2.1)-(2.2): reuse the accepted natural-log Renyi entropy after reindexing an arbitrary finite basis to Fin(card I). This is only a basis adapter; it preserves the accepted order-zero rank and order-one entropy branches. The theorems below use positive orders.
mutualRenyiNats: PDF pp.7-8, (2.7),(2.12): mutual Renyi information from the actual two partial traces.
centeredPower: PDF p.8, (2.12): the centered, normalized spectral factor. Subtracting the full identity is harmless off occupied support because the perturbation annihilates it.
cosecantPowerSum: PDF p.36, (A.22): the sine sum at k = 2d. The endpoint n = 1 is an empty sum. At n = 0 the definition also returns zero, but the theorem excludes that input.
binomialDenominator: PDF p.37, (A.24)-(A.25): polynomial coefficients of ((1+u)^n-1)/(n*u). The coefficient of u^m is (n-1)...(n-m)/(m+1)!. The empty product is one. The variable of each coefficient polynomial represents n, not u.
sineSumPolynomial: PDF p.37, (A.24)-(A.25): explicit polynomial obtained from minus the residue at t=1. Removing the Laurent factor u^-1 changes coefficient 2k-1 to coefficient 2k. The inverse uses constant coefficient one, so this is a construction over R[n], not an existence choice or interpolation axiom.
residueCoefficient: PDF p.37, (A.24): scalar version of the residue coefficient for an integer n. For n>=1 this denominator series has constant coefficient one.
scalarPairContinuation: PDF p.36, (A.22): the specified continuation of the scalar-pair coefficient. For k=2d and t>0 this is t^(1-4d) P_k(t)/2. It is not claimed to be the unique analytic interpolation among arbitrary analytic functions.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Defs_Ensemble
import Definitions.Def_QAlgorithms_Defs_Measurement
import Definitions.Def_QAlgorithms_Papers_Independent_Advance50_P21
import Definitions.Def_QAlgorithms_Papers_Independent_Information100_P56

/-!
Statements from Headrick, arXiv:1006.0047v3. PDF page numbers are used throughout.
Section 2.2 is stated on arbitrary finite occupied-support realizations of regulated
systems; no infinite-rank differentiability assertion is made. The CFT and geometric
results without a constructed interface are individually recorded in HARD.md.
-/

namespace QAlgorithms.Papers.Independent.Intakethird100.P41

open Filter
open QAlgorithms.Papers.Independent.Information100.P56 (entropy)
open scoped Topology

/-- PDF p.7, (2.8): the affine density-operator perturbation, with real parameter. -/
noncomputable def densityPerturbation {I : Type*} [Fintype I]
    (rho0 rho1 : Matrix I I ℂ) (t : ℝ) : Matrix I I ℂ :=
  rho0 + (t : ℂ) • rho1

/-- PDF p.7: normalized Hermitian perturbations with unchanged occupied support for
small real parameters of both signs. For Hermitian finite matrices, the kernel condition
on rho1 is equivalent to image(rho1) being contained in image(rho0). The final condition
states equality of occupied supports near zero, rather than assuming an entropy formula. -/
def IsSupportPreservingPerturbation {I : Type*} [Fintype I]
    (rho0 rho1 : Matrix I I ℂ) : Prop :=
  QAlgorithms.IsDensityMatrix rho0 ∧ rho1.IsHermitian ∧ rho1.trace = 0 ∧
  (∀ v : I → ℂ, rho0.mulVec v = 0 → rho1.mulVec v = 0) ∧
  ∀ᶠ t : ℝ in 𝓝 0,
    QAlgorithms.IsDensityMatrix (densityPerturbation rho0 rho1 t) ∧
    ∀ v : I → ℂ,
      (densityPerturbation rho0 rho1 t).mulVec v = 0 ↔ rho0.mulVec v = 0

/-- PDF pp.5,7: spectral powers on occupied support, extended by zero on the kernel.
In particular a negative exponent never assigns an infinite value to a zero eigenvalue. -/
noncomputable def occupiedPower {I : Type*} [Fintype I] [DecidableEq I]
    (a : ℝ) (rho : Matrix I I ℂ) : Matrix I I ℂ :=
  cfc (fun x : ℝ => if x = 0 then 0 else Real.rpow x a) rho

/-- PDF p.5, (2.1)-(2.2): reuse the accepted natural-log Renyi entropy after
reindexing an arbitrary finite basis to Fin(card I). This is only a basis adapter;
it preserves the accepted order-zero rank and order-one entropy branches.
The theorems below use positive orders. -/
noncomputable def regulatedRenyiNats {I : Type*} [Fintype I] [DecidableEq I]
    (a : ℝ) (rho : Matrix I I ℂ) : ℝ :=
  QAlgorithms.Papers.Independent.Advance50.P21.renyiNats a
    (Matrix.reindexAlgEquiv ℂ ℂ (Fintype.equivFin I) rho)

/-- PDF pp.7-8, (2.7),(2.12): mutual Renyi information from the actual two partial traces. -/
noncomputable def mutualRenyiNats {A B : Type*} [Fintype A] [Fintype B]
    [DecidableEq A] [DecidableEq B] (a : ℝ)
    (rho : Matrix (A × B) (A × B) ℂ) : ℝ :=
  regulatedRenyiNats a (QAlgorithms.traceRight rho) +
    regulatedRenyiNats a (QAlgorithms.traceLeft rho) - regulatedRenyiNats a rho

/-- PDF p.8, (2.12): the centered, normalized spectral factor. Subtracting the
full identity is harmless off occupied support because the perturbation annihilates it. -/
noncomputable def centeredPower {I : Type*} [Fintype I] [DecidableEq I]
    (a : ℝ) (rho : Matrix I I ℂ) : Matrix I I ℂ :=
  (((occupiedPower a rho).trace.re)⁻¹ : ℂ) • occupiedPower (a - 1) rho - 1

example {I : Type*} [Fintype I] (rho0 rho1 : Matrix I I ℂ) :
    densityPerturbation rho0 rho1 0 = rho0 := by
  simp [densityPerturbation]

example {I : Type*} [Fintype I] (rho : Matrix I I ℂ)
    (hrho : QAlgorithms.IsDensityMatrix rho) :
    IsSupportPreservingPerturbation rho 0 := by
  refine ⟨hrho, by simp [Matrix.IsHermitian], by simp, ?_, ?_⟩
  · intro v hv
    simp
  · apply Filter.Eventually.of_forall
    intro t
    constructor
    · simpa [densityPerturbation] using hrho
    · intro v
      simp [densityPerturbation]

example {I : Type*} [Fintype I] [DecidableEq I] (a : ℝ) :
    occupiedPower a (1 : Matrix I I ℂ) = 1 := by
  simp [occupiedPower, cfc_one]

example {I : Type*} [Fintype I] [DecidableEq I] :
    entropy (1 : Matrix I I ℂ) = 0 := by
  simp [entropy, cfc_one]

/-- PDF p.5: a one-dimensional pure density has zero Renyi entropy at every order. -/
example (a : ℝ) : regulatedRenyiNats a (1 : Matrix (Fin 1) (Fin 1) ℂ) = 0 := by
  simp [regulatedRenyiNats, QAlgorithms.Papers.Independent.Advance50.P21.renyiNats,
    QAlgorithms.Papers.Independent.Dependency50.P05.renyiEntropy, cfc_one]

/-- PDF p.36, (A.22): the sine sum at k = 2d. The endpoint n = 1 is an empty
sum. At n = 0 the definition also returns zero, but the theorem excludes that input. -/
noncomputable def cosecantPowerSum (k n : ℕ) : ℝ :=
  ∑ j ∈ Finset.Icc 1 (n - 1),
    ((2 : ℝ) * Real.sin (Real.pi * (j : ℝ) / (n : ℝ)))⁻¹ ^ (2 * k)

/-- PDF p.37, (A.24)-(A.25): polynomial coefficients of ((1+u)^n-1)/(n*u).
The coefficient of u^m is (n-1)...(n-m)/(m+1)!. The empty product is one.
The variable of each coefficient polynomial represents n, not u. -/
noncomputable def binomialDenominator : PowerSeries (Polynomial ℝ) :=
  PowerSeries.mk fun m =>
    Polynomial.C (((m + 1).factorial : ℝ)⁻¹) *
      ∏ j ∈ Finset.Icc 1 m, (Polynomial.X - Polynomial.C (j : ℝ))

/-- PDF p.37, (A.24)-(A.25): explicit polynomial obtained from minus the residue
at t=1. Removing the Laurent factor u^-1 changes coefficient 2k-1 to coefficient 2k.
The inverse uses constant coefficient one, so this is a construction over R[n], not an
existence choice or interpolation axiom. -/
noncomputable def sineSumPolynomial (k : ℕ) : Polynomial ℝ :=
  Polynomial.C ((-1 : ℝ) ^ (k + 1)) *
    PowerSeries.coeff (2 * k)
      (((1 + PowerSeries.X : PowerSeries (Polynomial ℝ)) ^ (k - 1)) *
        PowerSeries.invOfUnit binomialDenominator 1)

/-- PDF p.37, (A.24): scalar version of the residue coefficient for an integer n.
For n>=1 this denominator series has constant coefficient one. -/
noncomputable def residueCoefficient (k n : ℕ) : ℝ :=
  (-1 : ℝ) ^ (k + 1) * PowerSeries.coeff (2 * k)
    (((1 + PowerSeries.X : PowerSeries ℝ) ^ (k - 1)) *
      (PowerSeries.mk fun m => (n.choose (m + 1) : ℝ) / (n : ℝ))⁻¹)

/-- PDF p.36, (A.22): the specified continuation of the scalar-pair coefficient.
For k=2d and t>0 this is t^(1-4d) P_k(t)/2. It is not claimed to be the unique
analytic interpolation among arbitrary analytic functions. -/
noncomputable def scalarPairContinuation (k : ℕ) (t : ℝ) : ℝ :=
  (sineSumPolynomial k).eval t / (2 * t ^ (2 * k - 1))

example (k : ℕ) : cosecantPowerSum k 1 = 0 := by
  simp [cosecantPowerSum]

example : PowerSeries.constantCoeff binomialDenominator = 1 := by
  simp [binomialDenominator, PowerSeries.constantCoeff_mk]

example (k : ℕ) : scalarPairContinuation k 1 =
    (sineSumPolynomial k).eval 1 / 2 := by
  simp [scalarPairContinuation]

end QAlgorithms.Papers.Independent.Intakethird100.P41

Source

Entanglement Renyi entropies in holographic theories, arXiv:1006.0047v3, https://arxiv.org/abs/1006.0047v3

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

`QAlgorithms.Papers.Independent.Intakethird100.P41.IsSupportPreservingPerturbation`

For any finite index type $I$ and complex $I\times I$ matrices $\rho_0,\rho_1$ , this predicate means that $\rho_0$ is positive semidefinite with trace $1$ , that $\rho_1$ is Hermitian with trace $0$ , that $\rho_0v=0$ implies $\rho_1v=0$ for every vector $v:I\to\mathbb C$ , and that there is a real neighborhood of $0$ on which, for every $t$ , the matrix $\rho_0+t\rho_1$ is positive semidefinite with trace $1$ and satisfies

(\rho_0+t\rho_1)v=0\quad\Longleftrightarrow\quad \rho_0v=0 \qquad\text{for every }v:I\to\mathbb C.

The neighborhood condition includes both positive and negative sufficiently small $t$ , as well as $t=0$ . Positive definiteness is not required. If $I$ is empty, the trace- $1$ requirement cannot hold.

`QAlgorithms.Papers.Independent.Intakethird100.P41.binomialDenominator`

This defines a formal power series in a variable $z$ , with coefficients in the real polynomial ring $\mathbb R[x]$ , by

D(x,z)=\sum_{m=0}^{\infty} \left(\frac{1}{(m+1)!}\prod_{j=1}^{m}(x-j)\right)z^m.

The product is over the inclusive integer interval $1,\ldots,m$ ; for $m=0$ it is the empty product $1$ , so the constant coefficient of the series is the constant polynomial $1$ . This is a formal series and makes no assertion about analytic convergence.

`QAlgorithms.Papers.Independent.Intakethird100.P41.centeredPower`

For any finite index type $I$ with decidable equality, any real $a$ , and any complex $I\times I$ matrix $\rho$ , let $P_b(\rho)$ be the real continuous functional calculus of the function assigning $0$ at $x=0$ and the total real power $x^b$ at $x\ne0$ . This defines

\frac{1}{\operatorname{Re}\operatorname{tr}P_a(\rho)}\,P_{a-1}(\rho)-I_I.

The reciprocal is taken in $\mathbb R$ and then regarded as a complex scalar; consequently, if its denominator is zero, the result is $-I_I$ . There are no restrictions on $a$ , and $\rho$ need not be Hermitian or a density matrix. The functional calculus returns zero when its self-adjointness requirement fails, and $I$ may be empty.

`QAlgorithms.Papers.Independent.Intakethird100.P41.cosecantPowerSum`

For any natural numbers $k,n$ , including zero, this defines

\sum_{j=1}^{\,n-1} \left(\frac{1}{2\sin(\pi j/n)}\right)^{2k},

where $n-1$ is natural-number subtraction, truncated at zero, and the sum is over the inclusive integer interval from $1$ to that value. Thus the sum is empty and equals $0$ when $n=0$ or $n=1$ . Reciprocals and division are total, with $0^{-1}=0$ . When $k=0$ , every summand is $1$ , including under the convention $0^0=1$ , so the value is the natural number $n-1$ , interpreted as a real number.

`QAlgorithms.Papers.Independent.Intakethird100.P41.densityPerturbation`

For any finite index type $I$ , any two complex matrices $\rho_0,\rho_1$ indexed by $I\times I$ , and any real $t$ , this defines

\rho(t)=\rho_0+t\rho_1,

with $t$ regarded as a complex scalar. Neither matrix is required to be Hermitian, positive, or normalized. The definition also applies when $I$ is empty.

`QAlgorithms.Papers.Independent.Intakethird100.P41.mutualRenyiNats`

For any finite types $A,B$ with decidable equality, any real $a$ , and any complex matrix $\rho$ indexed by $A\times B$ , this defines

R_a(\rho_A)+R_a(\rho_B)-R_a(\rho), \qquad (\rho_A)_{u,v}=\sum_{b\in B}\rho_{(u,b),(v,b)},\qquad (\rho_B)_{u,v}=\sum_{a\in A}\rho_{(a,u),(a,v)}.

For each matrix $X$ , $R_a(X)$ means: reindex $X$ using the specified finite enumeration, then take the natural logarithm of the real trace of its nonzero-spectrum indicator if $a=0$ ; take $-\operatorname{Re}\operatorname{tr}[(x\mapsto x\log x)(X)]$ if $a=1$ ; and otherwise take $\log(\operatorname{Re}\operatorname{tr}[(x\mapsto x^a)(X)])/(1-a)$ . These matrix functions use the total real continuous functional calculus, which returns zero when its self-adjointness requirement fails. No positivity, normalization, or Hermiticity assumption is imposed on $\rho$ . Either index type may be empty, and the total logarithm convention $\log0=0$ applies.

`QAlgorithms.Papers.Independent.Intakethird100.P41.occupiedPower`

For any finite index type $I$ with decidable equality, any real exponent $a$ , and any complex $I\times I$ matrix $\rho$ , this defines the matrix obtained by the real continuous functional calculus from

f_a(x)= \begin{cases} 0,&x=0,\\ x^a,&x\ne0, \end{cases}

where $x^a$ is the total real-power function. For Hermitian $\rho$ , this applies $f_a$ to its eigenvalues; in particular, zero eigenvalues are assigned $0$ , even when $a=0$ or $a<0$ . No Hermiticity or density assumption is imposed on $\rho$ ; the total functional calculus returns the zero matrix when its self-adjointness requirement fails. Empty $I$ is allowed.

`QAlgorithms.Papers.Independent.Intakethird100.P41.regulatedRenyiNats`

For any finite index type $I$ with decidable equality, any real $a$ , and any complex $I\times I$ matrix $\rho$ , first reindex $\rho$ by the specified enumeration $I\cong\{0,\ldots,|I|-1\}$ , obtaining $\widehat\rho$ . This defines

R_a(\rho)= \begin{cases} \displaystyle \log\!\left(\operatorname{Re}\operatorname{tr} \mathbf1_{\{x\ne0\}}(\widehat\rho)\right),&a=0,\\[2mm] \displaystyle-\operatorname{Re}\operatorname{tr} \bigl[(x\mapsto x\log x)(\widehat\rho)\bigr],&a=1,\\[2mm] \displaystyle\frac{\log\!\left(\operatorname{Re}\operatorname{tr} \bigl[(x\mapsto x^a)(\widehat\rho)\bigr]\right)}{1-a},&a\ne0,1. \end{cases}

The matrix functions here use the real continuous functional calculus; the formula is the supplied base- $2$ definition multiplied by $\log 2$ . No density or Hermiticity assumption is imposed. Logarithms and real powers are total functions, including $\log0=0$ and $0^0=1$ ; in the $a=0$ branch, zero eigenvalues are explicitly assigned $0$ . The functional calculus returns zero when its self-adjointness requirement fails. Empty $I$ is included.

`QAlgorithms.Papers.Independent.Intakethird100.P41.residueCoefficient`

For any natural numbers $k,n$ , this defines the real number

(-1)^{k+1}[z^{2k}] \left((1+z)^{\,k-1} \left(\sum_{m=0}^{\infty}\frac{\binom n{m+1}}{n}\,z^m\right)^{-1}\right).

All series operations and coefficient extraction are formal, and $k-1$ is natural-number subtraction truncated at zero. Division is real division with division by zero equal to $0$ . For $n>0$ , the series inside the inverse has constant coefficient $1$ , so its inverse is its formal multiplicative inverse. For $n=0$ , that series and its total inverse are both zero, giving value $0$ . For $k=0$ and $n>0$ , the value is $-1$ .

`QAlgorithms.Papers.Independent.Intakethird100.P41.scalarPairContinuation`

For every natural number $k$ , including $0$ , and every real number $t$ , define $C_k(t)$ as follows. With $x$ a polynomial indeterminate and $z$ a formal power series indeterminate, put

B_x(z)=\sum_{m=0}^{\infty} \frac{\prod_{j=1}^{m}(x-j)}{(m+1)!}\,z^m, \qquad P_k(x)=(-1)^{k+1}[z^{2k}] \left((1+z)^{k-1}B_x(z)^{-1}\right),

where $[z^{2k}]$ extracts a coefficient, the empty product is $1$ , and the inverse is the formal power series inverse, whose constant coefficient is $1$ . Then

C_k(t)=\frac{P_k(t)}{2t^{\,2k-1}}.

Both natural-number subtractions $k-1$ and $2k-1$ are truncated at $0$ . The definition includes negative and zero $t$ ; division by zero has value $0$ . Thus $C_k(0)=0$ for $k\ge1$ , while $P_0=-1$ and $C_0(t)=-\tfrac12$ for every real $t$ .

`QAlgorithms.Papers.Independent.Intakethird100.P41.sineSumPolynomial`

For every natural number $k$ , this defines the real polynomial

(-1)^{k+1}[z^{2k}] \left((1+z)^{\,k-1}D(x,z)^{-1}\right), \qquad D(x,z)=\sum_{m=0}^{\infty} \frac{\prod_{j=1}^{m}(x-j)}{(m+1)!}\,z^m.

Here $x$ is the polynomial variable, $z$ is the formal-series variable, and $[z^{2k}]$ extracts the indicated coefficient as a polynomial in $x$ . The inverse is the formal inverse specified using the constant-coefficient unit $1$ ; indeed $D(x,0)=1$ . The exponent $k-1$ uses natural-number subtraction, so it is $0$ when $k=0$ ; in that case the resulting polynomial is $-1$ . No analytic convergence is required.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph