First-order entropy response on a regulated finite occupied support

Open

QAlgorithms.Papers.Independent.Intakethird100.P41.entropy_firstOrder

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

prove2quantum

Let $\rho(t)=\rho_0+t\rho_1$ be a density operator on an arbitrary finite occupied-support realization of a regulated system. Assume $\rho_0\ge0$ , $\operatorname{Tr}\rho_0=1$ , $\rho_1$ is Hermitian, $\operatorname{Tr}\rho_1=0$ , and $\operatorname{im}\rho_1\subseteq\operatorname{im}\rho_0$ . For all sufficiently small real $t$ of either sign, assume $\rho(t)$ remains positive and has the same occupied support as $\rho_0$ . For every fixed real $\alpha>0$ , $\alpha\ne1$ , the Renyi entropy $S_\alpha(\rho)=\log\operatorname{Tr}(\rho^\alpha)/(1-\alpha)$ and von Neumann entropy $S(\rho)=-\operatorname{Tr}(\rho\log\rho)$ , both in nats, satisfy

S_\alpha(\rho(t))=S_\alpha(\rho_0)+t\frac{\alpha}{1-\alpha}\frac{\operatorname{Tr}(\rho_1\rho_0^{\alpha-1})}{\operatorname{Tr}(\rho_0^\alpha)}+O(t^2), \qquad S(\rho(t))=S(\rho_0)-t\operatorname{Tr}(\rho_1\log\rho_0)+O(t^2).

Powers and logarithms are taken on the occupied support. Each remainder is two-sided as $t\to0$ , with constants allowed to depend on the fixed state, perturbation and order. These responses compare ordinary and Renyi entropy under a support-preserving perturbation.

Formalization Note The index type is arbitrary and finite, rather than a prescribed matrix dimension. This is the plan's regulated finite-rank interpretation; it does not assert an infinite-rank trace-class differentiability theorem.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P41

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P41

open Filter

open QAlgorithms.Papers.Independent.Information100.P56 (entropy)

open scoped Topology

/-- PDF p.7, (2.9)-(2.10): both first-order entropy responses, with quadratic
remainders, for the regulated finite-rank interpretation. The dimension is arbitrary,
zero eigenvalues are allowed, and no commutation hypothesis is imposed on rho0 and rho1.
The infinite-rank interpretation requires additional trace/differentiability domains. -/
theorem entropy_firstOrder {I : Type*} [Fintype I] [DecidableEq I]
    (rho0 rho1 : Matrix I I ℂ) (hpert : IsSupportPreservingPerturbation rho0 rho1)
    (a : ℝ) (ha : 0 < a) (ha1 : a ≠ 1) :
    Asymptotics.IsBigO (𝓝 (0 : ℝ))
      (fun t : ℝ => regulatedRenyiNats a (densityPerturbation rho0 rho1 t) -
        regulatedRenyiNats a rho0 - t * (a / (1 - a) *
          (rho1 * occupiedPower (a - 1) rho0).trace.re /
            (occupiedPower a rho0).trace.re))
      (fun t : ℝ => t ^ 2) ∧
    Asymptotics.IsBigO (𝓝 (0 : ℝ))
      (fun t : ℝ => entropy (densityPerturbation rho0 rho1 t) -
        entropy rho0 + t * (rho1 * cfc Real.log rho0).trace.re)
      (fun t : ℝ => t ^ 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P41

Source

Entanglement Renyi entropies in holographic theories, arXiv:1006.0047v3, PDF p. 7, §2.2, (2.8)–(2.10)

Read-back

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

For every finite index type $I$ with decidable equality, complex $I\times I$ matrices $\rho_0,\rho_1$ , and real $a>0$ with $a\ne1$ , assume that $\rho_0$ is positive semidefinite of trace $1$ , $\rho_1$ is Hermitian of trace $0$ , $\ker\rho_0\subseteq\ker\rho_1$ , and every sufficiently small real $t$ makes $\rho(t)=\rho_0+t\rho_1$ positive semidefinite of trace $1$ with exactly the same kernel as $\rho_0$ . Let $P_b(X)$ apply the function $0\mapsto0$ , $x\ne0\mapsto x^b$ , by real continuous functional calculus; let $R_a(X)=\log(\operatorname{Re}\operatorname{tr}(x\mapsto x^a)(X))/(1-a)$ , with the specified finite reindexing understood; and let $S(X)=-\operatorname{Re}\operatorname{tr}[(x\mapsto x\log x)(X)]$ . Then both estimates hold as real $t\to0$ :

R_a(\rho(t))-R_a(\rho_0) -t\,\frac{a}{1-a}\, \frac{\operatorname{Re}\operatorname{tr}(\rho_1P_{a-1}(\rho_0))} {\operatorname{Re}\operatorname{tr}P_a(\rho_0)} =O(t^2),

S(\rho(t))-S(\rho_0) +t\,\operatorname{Re}\operatorname{tr}\bigl(\rho_1\log(\rho_0)\bigr) =O(t^2).

Here $\log(\rho_0)$ uses the real continuous functional calculus with the total convention $\log0=0$ . Each $O(t^2)$ assertion means that the absolute value of the displayed expression is bounded by a constant times $|t|^2$ throughout some neighborhood of $0$ , including negative $t$ . Singular $\rho_0$ is allowed; empty $I$ makes the density hypothesis impossible.

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