Definitions for Monotonicity of the Quantum Relative Entropy Under Positive Maps

Definition

QAlgorithms_Papers_Independent_Intakethird100_P46

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

prove2quantum

The objects the formalized statements of Monotonicity of the Quantum Relative Entropy Under Positive Maps (arXiv:1512.06117) are stated in. Each was checked against the paper by a blind read-back and a moderator.

TraceLinearOperationBetween: PDF p.2, Notation: a complex-linear map from the full trace-class space T(H) to T(K). Its ambient values off trace class impose no restriction.
traceClassImage: PDF p.2: restrict the output of a trace-class operation to its actual domain.
PositiveTracePreservingBetween: PDF p.2, Notation and Theorem 1: positivity and trace preservation are required on every positive trace-class input, not only on the displayed pair.
PositiveTraceNonincreasingBetween: PDF pp.2–3, Notation and Theorem 1': positivity and trace nonincrease on the entire positive trace-class cone, between possibly different spaces.
literalTraceClassRelativeEntropy: PDF pp.1–2, (1) and Notation: literal unnormalized relative entropy in nats. On positive trace-class pairs, the accepted corrected extended divergence is D(rho||sigma)+tr(sigma-rho). Subtract ONLY this finite real trace correction. The ENNReal-to-EReal embedding retains infinity; finite negative D is allowed. No two potentially infinite entropy terms are subtracted.
PositiveMatrixTraceNonincreasing: PDF p.3, (4)–(5): positive finite-dimensional maps with trace nonincrease on every PSD matrix. Complex linearity is in the map type.
finiteLiteralRelativeEntropy: PDF pp.1–3, (1): finite-dimensional literal Umegaki entropy in nats, including support failure. This direct formula also accepts subnormalized outputs.
traceDecreaseMap: PDF p.3, counterexample: discard off-diagonal entries and halve the first entry.
counterexampleRho: PDF p.3, counterexample: the first normalized input state.
counterexampleSigma: PDF p.3, counterexample: the second normalized input state.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Papers_Independent_Dependency50_P13
import Definitions.Def_QAlgorithms_Papers_Independent_Bridge50_P49
import Definitions.Def_QAlgorithms_Defs_MatrixMapPositivity

/-!
Müller-Hermes–Reeb, arXiv:1512.06117v3, PDF pp.1–7.
All new definitions are local to this paper. Arbitrary countable Hilbert bases
represent separable complex Hilbert spaces; they need not diagonalize either
operator. Nuclear trace class and the corrected extended divergence are accepted
Dependency50.P13 definitions. Only the finite trace correction is removed here.
Theorem 3 (PDF p.4) is recorded as accepted-library reuse, without a duplicate.
Compilation and independent moderation are pending the batch handoff.
-/

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

namespace QAlgorithms.Papers.Independent.Intakethird100.P46

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms
open QAlgorithms.Papers.Independent.Dependency50.P13
  (IsTraceClass TraceClass IsPositive operatorTrace)
open QAlgorithms.Papers.Independent.Dependency50.P35 (Dominates)
open QAlgorithms.Papers.Independent.Bridge50.P49 (beigiSandwichedDivergence)

variable {H K : Type*}
  [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
  [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]

/-- PDF p.2, Notation: a complex-linear map from the full trace-class space
T(H) to T(K). Its ambient values off trace class impose no restriction. -/
def TraceLinearOperationBetween
    (Phi : (H →L[ℂ] H) → (K →L[ℂ] K)) : Prop :=
  (∀ A, IsTraceClass A → IsTraceClass (Phi A)) ∧
  (∀ A B, IsTraceClass A → IsTraceClass B → Phi (A + B) = Phi A + Phi B) ∧
  (∀ (z : ℂ) A, IsTraceClass A → Phi (z • A) = z • Phi A)

example : TraceLinearOperationBetween (id : (H →L[ℂ] H) → (H →L[ℂ] H)) := by
  exact ⟨fun A hA => hA, fun A B hA hB => rfl, fun z A hA => rfl⟩

/-- PDF p.2: restrict the output of a trace-class operation to its actual domain. -/
def traceClassImage (Phi : (H →L[ℂ] H) → (K →L[ℂ] K))
    (hPhi : TraceLinearOperationBetween Phi) (A : TraceClass H) : TraceClass K :=
  ⟨Phi A.val, hPhi.1 A.val A.property⟩

example (Phi : (H →L[ℂ] H) → (K →L[ℂ] K))
    (hPhi : TraceLinearOperationBetween Phi) (A : TraceClass H) :
    (traceClassImage Phi hPhi A).val = Phi A.val := rfl

/-- PDF p.2, Notation and Theorem 1: positivity and trace preservation are
required on every positive trace-class input, not only on the displayed pair. -/
def PositiveTracePreservingBetween {I J : Type*}
    (b : HilbertBasis I ℂ H) (c : HilbertBasis J ℂ K)
    (Phi : (H →L[ℂ] H) → (K →L[ℂ] K)) : Prop :=
  TraceLinearOperationBetween Phi ∧ ∀ A, IsTraceClass A → IsPositive A →
    IsPositive (Phi A) ∧ operatorTrace c (Phi A) = operatorTrace b A

example {I : Type*} (b : HilbertBasis I ℂ H) :
    PositiveTracePreservingBetween b b (id : (H →L[ℂ] H) → (H →L[ℂ] H)) := by
  exact ⟨⟨fun A hA => hA, fun A B hA hB => rfl, fun z A hA => rfl⟩,
    fun A hA hp => ⟨hp, rfl⟩⟩

/-- PDF pp.2–3, Notation and Theorem 1': positivity and trace nonincrease
on the entire positive trace-class cone, between possibly different spaces. -/
def PositiveTraceNonincreasingBetween {I J : Type*}
    (b : HilbertBasis I ℂ H) (c : HilbertBasis J ℂ K)
    (Phi : (H →L[ℂ] H) → (K →L[ℂ] K)) : Prop :=
  TraceLinearOperationBetween Phi ∧ ∀ A, IsTraceClass A → IsPositive A →
    IsPositive (Phi A) ∧ (operatorTrace c (Phi A)).re ≤ (operatorTrace b A).re

example {I : Type*} (b : HilbertBasis I ℂ H) :
    PositiveTraceNonincreasingBetween b b (id : (H →L[ℂ] H) → (H →L[ℂ] H)) := by
  exact ⟨⟨fun A hA => hA, fun A B hA hB => rfl, fun z A hA => rfl⟩,
    fun A hA hp => ⟨hp, le_rfl⟩⟩

/-- PDF pp.1–2, (1) and Notation: literal unnormalized relative entropy in nats.
On positive trace-class pairs, the accepted corrected extended divergence is
D(rho||sigma)+tr(sigma-rho). Subtract ONLY this finite real trace correction.
The ENNReal-to-EReal embedding retains infinity; finite negative D is allowed.
No two potentially infinite entropy terms are subtracted. -/
def literalTraceClassRelativeEntropy {I : Type*} (b : HilbertBasis I ℂ H)
    (rho sigma : TraceClass H) : EReal :=
  (QAlgorithms.Papers.Independent.Dependency50.P13.relativeEntropy rho sigma : EReal) -
    (((operatorTrace b sigma.val).re - (operatorTrace b rho.val).re : ℝ) : EReal)

example {I : Type*} (b : HilbertBasis I ℂ H) (rho sigma : TraceClass H)
    (h : operatorTrace b sigma.val = operatorTrace b rho.val) :
    literalTraceClassRelativeEntropy b rho sigma =
      (QAlgorithms.Papers.Independent.Dependency50.P13.relativeEntropy rho sigma : EReal) := by
  simp [literalTraceClassRelativeEntropy, h]

/-- PDF p.3, (4)–(5): positive finite-dimensional maps with trace nonincrease
on every PSD matrix. Complex linearity is in the map type. -/
def PositiveMatrixTraceNonincreasing {d e : ℕ}
    (Phi : Matrix (Fin d) (Fin d) ℂ →ₗ[ℂ] Matrix (Fin e) (Fin e) ℂ) : Prop :=
  ∀ A, A.PosSemidef → (Phi A).PosSemidef ∧ (Phi A).trace.re ≤ A.trace.re

example (d : ℕ) : PositiveMatrixTraceNonincreasing
    (LinearMap.id : Matrix (Fin d) (Fin d) ℂ →ₗ[ℂ] Matrix (Fin d) (Fin d) ℂ) := by
  intro A hA
  exact ⟨hA, le_rfl⟩

/-- PDF pp.1–3, (1): finite-dimensional literal Umegaki entropy in nats,
including support failure. This direct formula also accepts subnormalized outputs. -/
def finiteLiteralRelativeEntropy {I : Type} [Fintype I] [DecidableEq I]
    (rho sigma : Matrix I I ℂ) : EReal :=
  if Dominates sigma rho then
    (((cfc (fun x : ℝ => x * Real.log x) rho -
      rho * cfc Real.log sigma).trace.re : ℝ) : EReal)
  else ⊤

example {I : Type} [Fintype I] [DecidableEq I]
    (rho sigma : Matrix I I ℂ) (h : ¬ Dominates sigma rho) :
    finiteLiteralRelativeEntropy rho sigma = ⊤ := by
  simp [finiteLiteralRelativeEntropy, h]

/-- PDF p.3, counterexample: discard off-diagonal entries and halve the first entry. -/
def traceDecreaseMap : Matrix (Fin 2) (Fin 2) ℂ →ₗ[ℂ] Matrix (Fin 2) (Fin 2) ℂ where
  toFun X := !![X 0 0 / 2, 0; 0, X 1 1]
  map_add' X Y := by
    ext i j
    fin_cases i <;> fin_cases j <;> simp [add_div]
  map_smul' z X := by
    ext i j
    fin_cases i <;> fin_cases j <;> simp [smul_eq_mul, mul_div_assoc]

example (X : Matrix (Fin 2) (Fin 2) ℂ) : traceDecreaseMap X 0 0 = X 0 0 / 2 := rfl

/-- PDF p.3, counterexample: the first normalized input state. -/
def counterexampleRho : Matrix (Fin 2) (Fin 2) ℂ := !![(1 / 3 : ℂ), 0; 0, 2 / 3]

/-- PDF p.3, counterexample: the second normalized input state. -/
def counterexampleSigma : Matrix (Fin 2) (Fin 2) ℂ := !![(2 / 3 : ℂ), 0; 0, 1 / 3]

example : counterexampleRho 0 0 = (1 / 3 : ℂ) := rfl

example : counterexampleSigma 1 1 = (1 / 3 : ℂ) := rfl

end QAlgorithms.Papers.Independent.Intakethird100.P46

Source

Monotonicity of the Quantum Relative Entropy Under Positive Maps, arXiv:1512.06117v3, https://arxiv.org/abs/1512.06117v3

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P46.PositiveMatrixTraceNonincreasing`

For natural numbers $d,e$ , including zero, and a complex-linear map $\Phi:M_d(\mathbb C)\to M_e(\mathbb C)$ , this predicate says that every positive semidefinite matrix $A$ has positive semidefinite image and satisfies

\operatorname{Re}\operatorname{Tr}\Phi(A)\le\operatorname{Re}\operatorname{Tr}A.

There is no trace-one or nonzero-input restriction.

`QAlgorithms.Papers.Independent.Intakethird100.P46.PositiveTraceNonincreasingBetween`

For complex Hilbert spaces $H,K$ , arbitrary index types $I,J$ , Hilbert bases $b=(b_i)_{i\in I}$ and $c=(c_j)_{j\in J}$ , and a function $\Phi$ between bounded complex-linear operators on these spaces, this predicate requires trace-class preservation, additivity and complex homogeneity on trace-class inputs, and, for every positive trace-class $A$ , positivity of $\Phi(A)$ together with

\operatorname{Re}\sum_{j\in J}\langle c_j,\Phi(A)c_j\rangle \le \operatorname{Re}\sum_{i\in I}\langle b_i,Ab_i\rangle.

Trace class means admitting $Tx=\sum_{r\in\mathbb N}\langle v_r,x\rangle u_r$ with $\sum_r\|u_r\|\|v_r\|$ summable; positivity means self-adjointness and nonnegative real quadratic forms. The traces use total infinite sums. Zero inputs are included, no normalization is required, and the basis index types need not be countable.

`QAlgorithms.Papers.Independent.Intakethird100.P46.PositiveTracePreservingBetween`

For complex Hilbert spaces $H,K$ , arbitrary index types $I,J$ , Hilbert bases $b=(b_i)_{i\in I}$ of $H$ and $c=(c_j)_{j\in J}$ of $K$ , and a function $\Phi$ between their bounded complex-linear operators, this predicate requires that $\Phi$ preserve trace-class operators, be additive and complex homogeneous on trace-class inputs, and, for every positive trace-class operator $A$ , have positive output and satisfy

\sum_{j\in J}\langle c_j,\Phi(A)c_j\rangle = \sum_{i\in I}\langle b_i,Ab_i\rangle.

Here trace class means admitting a representation $Tx=\sum_{r\in\mathbb N}\langle v_r,x\rangle u_r$ with $\sum_r\|u_r\|\|v_r\|$ summable; positivity means $T^*=T$ and $\operatorname{Re}\langle x,Tx\rangle\ge0$ for every $x$ . The displayed traces are the defined total infinite sums, and their equality is an equality in $\mathbb C$ . No normalization or nonzero-input condition is required, and $I,J$ are not assumed countable.

`QAlgorithms.Papers.Independent.Intakethird100.P46.TraceLinearOperationBetween`

For complex Hilbert spaces $H$ and $K$ , and an arbitrary function $\Phi$ from bounded complex-linear operators on $H$ to bounded complex-linear operators on $K$ , this predicate requires that $\Phi$ maps trace-class operators to trace-class operators, satisfies $\Phi(A+B)=\Phi(A)+\Phi(B)$ whenever $A$ and $B$ are trace class, and satisfies $\Phi(zA)=z\Phi(A)$ for every $z\in\mathbb C$ and trace-class $A$ . Here an operator $T$ is trace class precisely when there exist sequences $(u_r)_{r\in\mathbb N}$ and $(v_r)_{r\in\mathbb N}$ in its Hilbert space such that $\sum_r\|u_r\|\|v_r\|$ is summable and $Tx=\sum_r\langle v_r,x\rangle u_r$ for every $x$ . The predicate imposes no conditions on $\Phi$ at operators outside this class.

`QAlgorithms.Papers.Independent.Intakethird100.P46.counterexampleRho`

This defines the $2\times2$ complex matrix

\begin{pmatrix} \frac13&0\\ 0&\frac23 \end{pmatrix}.

`QAlgorithms.Papers.Independent.Intakethird100.P46.counterexampleSigma`

This defines the $2\times2$ complex matrix

\begin{pmatrix} \frac23&0\\ 0&\frac13 \end{pmatrix}.

`QAlgorithms.Papers.Independent.Intakethird100.P46.finiteLiteralRelativeEntropy`

For any finite type $I$ equipped with decidable equality, and arbitrary complex matrices $\rho,\sigma$ indexed by $I$ , this defines

L(\rho,\sigma)= \begin{cases} \operatorname{Re}\operatorname{Tr}\bigl(f(\rho)-\rho\log(\sigma)\bigr), &\ker\sigma\subseteq\ker\rho,\\ +\infty,&\text{otherwise}, \end{cases} \qquad f(x)=x\log x,

as an extended-real number, using continuous functional calculus for both matrix functions. The kernels are those of matrix multiplication on $\mathbb C^I$ . No positivity, self-adjointness, normalization, or nonzero assumption is imposed; the finite branch is not truncated to be nonnegative. The real logarithm is total, with $\log0=0$ . The empty index type is allowed and gives value $0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P46.literalTraceClassRelativeEntropy`

For a complex Hilbert space $H$ , an arbitrary index type $I$ , a Hilbert basis $b=(b_i)_{i\in I}$ , and trace-class operators $\rho,\sigma$ on $H$ , this defines the extended-real number

L_b(\rho,\sigma) = R(\rho,\sigma) -\left(\operatorname{Re}\sum_i\langle b_i,\sigma b_i\rangle -\operatorname{Re}\sum_i\langle b_i,\rho b_i\rangle\right).

Here trace-class membership means admitting a representation $Tx=\sum_{r\in\mathbb N}\langle v_r,x\rangle u_r$ with summable $\|u_r\|\|v_r\|$ , and $R(\rho,\sigma)$ is the supremum, in $[0,\infty]$ , over every $n\in\mathbb N$ and every orthonormal family $v_0,\ldots,v_{n-1}$ in $H$ , of the following quantity. Set $X_{ij}=\langle v_i,\rho v_j\rangle$ and $Y_{ij}=\langle v_i,\sigma v_j\rangle$ ; the quantity is $+\infty$ if $\ker Y\nsubseteq\ker X$ , and otherwise is

\max\!\left\{0,\operatorname{Re}\operatorname{Tr} \bigl(f(X)-X\log(Y)-X+Y\bigr)\right\}, \qquad f(x)=x\log x,

with matrix functions interpreted by the continuous functional calculus. The supremum is embedded into the extended reals before subtracting the finite real trace difference. Neither positivity nor normalization of $\rho,\sigma$ is assumed; the supremum includes $n=0$ , and real logarithms and infinite sums have their total-function meanings.

`QAlgorithms.Papers.Independent.Intakethird100.P46.traceClassImage`

For complex Hilbert spaces $H,K$ , a function $\Phi$ between their bounded complex-linear operators, a hypothesis that $\Phi$ preserves trace-class operators and is additive and complex homogeneous on them, and a trace-class operator $A$ on $H$ , this definition returns the trace-class operator on $K$ whose underlying operator is $\Phi(A)$ . An operator $T$ is trace class here when it admits sequences $u_r,v_r$ with $\sum_r\|u_r\|\|v_r\|$ summable and $Tx=\sum_r\langle v_r,x\rangle u_r$ for every $x$ ; the supplied hypothesis provides this property for $\Phi(A)$ .

`QAlgorithms.Papers.Independent.Intakethird100.P46.traceDecreaseMap`

This defines the complex-linear map on $2\times2$ complex matrices given, for every input $X$ , by

X\longmapsto \begin{pmatrix} X_{00}/2&0\\ 0&X_{11} \end{pmatrix}.

Its linear-map structure includes additivity and homogeneity for every complex scalar; no restriction is placed on the input matrix.

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