Linear mutual Renyi response and quadratic mutual information at a product state

Open

QAlgorithms.Papers.Independent.Intakethird100.P41.mutualRenyi_firstOrder

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

prove2quantum

Let $A$ and $B$ be arbitrary finite regulated Hilbert factors, let $\widehat\rho_A$ and $\widehat\rho_B$ be positive trace-one density matrices, and set $\rho_0=\widehat\rho_A\otimes\widehat\rho_B$ . Let $\rho(t)=\rho_0+t\rho_1$ be normalized and positive with unchanged occupied support for sufficiently small real $t$ of either sign, where $\rho_1$ is Hermitian, has trace zero, and has image in the occupied support of $\rho_0$ . Define the actual marginals by $\rho_A(t)=\operatorname{Tr}_B\rho(t)$ and $\rho_B(t)=\operatorname{Tr}_A\rho(t)$ , and put $I_\alpha(t)=S_\alpha(\rho_A(t))+S_\alpha(\rho_B(t))-S_\alpha(\rho(t))$ . For fixed $\alpha>0$ , $\alpha\ne1$ , define

D_X=\frac{\widehat\rho_X^{\alpha-1}}{\operatorname{Tr}\widehat\rho_X^\alpha}-\mathbf1_X\quad(X=A,B).

Then

I_\alpha(t)=t\frac{\alpha}{\alpha-1}\operatorname{Tr}\!\left[\rho_1(D_A\otimes D_B)\right]+O(t^2), \qquad I_1(t)=O(t^2).

All logarithms are natural, powers are on occupied support, and the error estimates are two-sided at zero for fixed data. This distinguishes the possible linear Renyi response from the quadratic onset of mutual information. No universal nonzero quadratic coefficient is asserted.

Formalization Note Both marginals are computed using the frozen partial-trace definitions at each parameter. The theorem concerns the regulated finite-rank interpretation, not an unqualified infinite-dimensional extension.

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 pp.7-8, (2.11)-(2.13): MRI has the displayed linear response about a product
state and MI has a quadratic remainder. Marginals are computed by partial trace at each
parameter, not held fixed. This states the regulated finite-rank interpretation; it makes
no assertion that the quadratic coefficient is nonzero for every perturbation. -/
theorem mutualRenyi_firstOrder {A B : Type*} [Fintype A] [Fintype B]
    [DecidableEq A] [DecidableEq B]
    (rhoA : Matrix A A ℂ) (rhoB : Matrix B B ℂ)
    (hA : QAlgorithms.IsDensityMatrix rhoA) (hB : QAlgorithms.IsDensityMatrix rhoB)
    (rho1 : Matrix (A × B) (A × B) ℂ)
    (hpert : IsSupportPreservingPerturbation (Matrix.kronecker rhoA rhoB) rho1)
    (a : ℝ) (ha : 0 < a) (ha1 : a ≠ 1) :
    Asymptotics.IsBigO (𝓝 (0 : ℝ))
      (fun t : ℝ => mutualRenyiNats a
        (densityPerturbation (Matrix.kronecker rhoA rhoB) rho1 t) -
        t * (a / (a - 1) *
          (rho1 * Matrix.kronecker (centeredPower a rhoA)
            (centeredPower a rhoB)).trace.re))
      (fun t : ℝ => t ^ 2) ∧
    Asymptotics.IsBigO (𝓝 (0 : ℝ))
      (fun t : ℝ => mutualRenyiNats 1
        (densityPerturbation (Matrix.kronecker rhoA rhoB) rho1 t))
      (fun t : ℝ => t ^ 2) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P41

Source

Entanglement Renyi entropies in holographic theories, arXiv:1006.0047v3, PDF p. 8, §2.2, (2.11)–(2.13)

Read-back

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

For every pair of finite index types $A,B$ with decidable equality, let $\rho_A,\rho_B$ be positive semidefinite matrices of trace $1$ on their respective types, and let $\rho_1$ be a complex matrix on $A\times B$ . Put $\rho_0=\rho_A\otimes\rho_B$ , and assume that $\rho_1$ is Hermitian of trace $0$ , $\ker\rho_0\subseteq\ker\rho_1$ , and $\rho(t)=\rho_0+t\rho_1$ is positive semidefinite of trace $1$ with kernel $\ker\rho_0$ for every sufficiently small real $t$ . For any real $a>0$ , $a\ne1$ , define $P_b(X)$ by continuous functional calculus using $0\mapsto0$ and $x\ne0\mapsto x^b$ , and put

C_a(X)=\frac{P_{a-1}(X)}{\operatorname{Re}\operatorname{tr}P_a(X)}-I.

Define $R_b(X)$ , after the specified finite reindexing, as $\log(\operatorname{Re}\operatorname{tr}\mathbf1_{\{x\ne0\}}(X))$ for $b=0$ , as $-\operatorname{Re}\operatorname{tr}[(x\mapsto x\log x)(X)]$ for $b=1$ , and otherwise as $\log(\operatorname{Re}\operatorname{tr}(x\mapsto x^b)(X))/(1-b)$ . Write $J_b(X)=R_b(\operatorname{tr}_B X)+R_b(\operatorname{tr}_A X)-R_b(X)$ , where $(\operatorname{tr}_B X)_{u,v}=\sum_bX_{(u,b),(v,b)}$ and $(\operatorname{tr}_A X)_{u,v}=\sum_aX_{(a,u),(a,v)}$ . Then

J_a(\rho(t)) -t\,\frac{a}{a-1}\operatorname{Re}\operatorname{tr} \bigl(\rho_1[C_a(\rho_A)\otimes C_a(\rho_B)]\bigr) =O(t^2), \qquad J_1(\rho(t))=O(t^2)

as real $t\to0$ . Each estimate bounds the absolute value by a constant times $|t|^2$ on a two-sided neighborhood of $0$ . Logarithms and reciprocals use their total conventions at zero. Singular density matrices are permitted; an empty $A$ or $B$ makes the corresponding trace- $1$ 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