Relative Petz Renyi entanglement is non-entangling monotone

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.relativeRenyi_monotone

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

prove2quantum

All Hilbert spaces are finite-dimensional complex spaces with fixed product bases and positive local dimensions. States are positive semidefinite operators of trace one; pure kets have norm one. A non-entangling map is completely positive and preserves the full separable positive cone. A channel is also trace preserving. Let $\rho$ be any bipartite density matrix, let $\Lambda$ be a non-entangling channel, and let $0\le\alpha\le2$ . Define $E_{R,\alpha}$ as the infimum of base-two Petz divergence over all separable density matrices. Then

E_{R,\alpha}(\Lambda(\rho))\le E_{R,\alpha}(\rho).

This includes the mixed-state result and both endpoints.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P19

Formal statement

noncomputable section

open QAlgorithms QAlgorithms.Entanglement Filter

open scoped Matrix ComplexOrder ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P19

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P19 (Bip)

open QAlgorithms.Papers.Independent.Information100.P69 (CP)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower SupportIncluded)

open QAlgorithms.Papers.Independent.Dependency50.P19 (epr)

/-- PDF p.10: Petz relative-Renyi entanglement monotonicity for mixed inputs
and every order in [0,2], including the Umegaki branch. -/
theorem relativeRenyi_monotone {a b c d : ℕ}
    (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d)
    (alpha : ℝ) (h0 : 0 ≤ alpha) (h2 : alpha ≤ 2)
    (rho : Bip a b) (hrho : IsDensityMatrix rho)
    (L : Superop (Fin a × Fin b) (Fin c × Fin d)) (hL : IsChannel L) (hne : NE L) :
    relativeRenyi alpha (L rho) ≤ relativeRenyi alpha rho := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 10, relative-renyi-monotonicity

Read-back

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

For positive natural numbers $a,b,c,d$ , a real order $0\le\alpha\le2$ , and a positive semidefinite trace- $1$ matrix $\rho$ on $\mathbb C^a\otimes\mathbb C^b$ , let $L$ be a channel to $\mathbb C^c\otimes\mathbb C^d$ that preserves separable positive operators. Explicitly, $L(X)=\sum_jK_jXK_j^\dagger$ for a finite family satisfying $\sum_jK_j^\dagger K_j=I$ , and it maps every finite sum of nonnegative multiples of tensor products of density matrices to another such sum; empty sums are included. For a positive semidefinite matrix $X$ , define $X^{[t]}$ by functional calculus using $x^{[t]}=0$ at $x=0$ and $x^{[t]}=x^t$ otherwise, including $0^{[0]}=0$ . For density matrices $R,S$ , define the extended nonnegative quantity

D_\alpha(R\|S)= \begin{cases} \dfrac{\max\{0,\operatorname{Re}\operatorname{Tr}(R\log R-R\log S)\}}{\log2}, &\alpha=1,\ \ker S\subseteq\ker R,\\ +\infty,&\alpha=1,\ \ker S\nsubseteq\ker R,\\ +\infty,&\alpha>1,\ \ker S\nsubseteq\ker R,\\ \max\!\left\{0,\dfrac{\log_2 z}{\alpha-1}\right\}, &\alpha\ne1,\ \text{the preceding support obstruction is absent},\ z>0,\\ +\infty,&\alpha\ne1,\ \text{the preceding support obstruction is absent},\ z\le0, \end{cases} \qquad z=\operatorname{Re}\operatorname{Tr}\bigl(R^{[\alpha]}S^{[1-\alpha]}\bigr),

where logarithms of matrices use functional calculus with the total real logarithm, whose value at zero is zero. Let $E_\alpha(R)$ be the infimum of $D_\alpha(R\|S)$ over all density matrices $S$ expressible as finite nonnegative weighted sums of products of density matrices. Then

E_\alpha(L(\rho))\le E_\alpha(\rho)

in $[0,+\infty]$ . Both endpoint orders $0,2$ and the separate order- $1$ definition are included.

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