Unbounded Renyi entropy increase below one half

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.renyi_unboundedIncrease

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. For each $0\le\alpha<1/2$ and each real $M>0$ , there are finite bipartite pure states $\psi,\varphi$ and a non-entangling channel $\Lambda$ such that

\Lambda(\psi)=\varphi,\qquad E_\alpha(\varphi)-E_\alpha(\psi)>M.

All entropies are in bits; the dimensions may depend on $\alpha$ and $M$ .

This states the introductory claim in its stronger unbounded form.

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.3, strengthened introductory claim: arbitrarily large entropy
increases below one half. Dimensions may depend on alpha and the desired increase. -/
theorem renyi_unboundedIncrease (alpha : ℝ) (h0 : 0 ≤ alpha) (hhalf : alpha < 1 / 2)
    (M : ℝ) (hM : 0 < M) :
    ∃ a b c d : ℕ, 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d ∧
      ∃ psi : UnitBipartiteKet a b, ∃ phi : UnitBipartiteKet c d,
      ∃ L : Superop (Fin a × Fin b) (Fin c × Fin d),
        IsChannel L ∧ NE L ∧ L psi.rho = phi.rho ∧
        M < schmidtRenyi (ENNReal.ofReal alpha) phi.ket - schmidtRenyi (ENNReal.ofReal alpha) psi.ket := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 3, unbounded-renyi-increase

Read-back

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

For every real $0\le\alpha<\tfrac12$ and every real $M>0$ , there exist positive natural numbers $a,b,c,d$ , unit vectors $\psi\in\mathbb C^a\otimes\mathbb C^b$ and $\phi\in\mathbb C^c\otimes\mathbb C^d$ , and a channel $L$ between their matrix spaces such that $L$ preserves separable positive operators and

L(|\psi\rangle\langle\psi|)=|\phi\rangle\langle\phi|, \qquad M<H_\alpha(\phi)-H_\alpha(\psi).

Here a channel has a finite Kraus representation $L(X)=\sum_jK_jXK_j^\dagger$ with $\sum_jK_j^\dagger K_j=I$ , and preservation of separable positive operators means preservation of finite nonnegative weighted sums of tensor products of positive semidefinite trace- $1$ matrices, including the empty sum. For a unit vector $v\in\mathbb C^u\otimes\mathbb C^v$ , let $\lambda_i$ , $0\le i<u$ , be the eigenvalues of its first marginal $\operatorname{Tr}_2|v\rangle\langle v|$ , listed in decreasing order and retaining zeros, and define

H_\alpha(v)= \begin{cases} \log_2\#\{i:\lambda_i>0\},&\alpha=0,\\[2pt] \dfrac{\log_2\left(\sum_i\lambda_i^\alpha\right)}{1-\alpha}, &0<\alpha<\tfrac12. \end{cases}

Thus order zero is included and uses the number of strictly positive marginal eigenvalues.

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