Appendix A: Epstein trace function maps upper half-plane to itself

Open

QAlgorithms.Papers.Independent.Intakethird100.P51.epsteinPick

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

prove2quantum

Let $A>0$ and let $K,B$ be self-adjoint matrices on a nonzero finite complex system. For $\operatorname{Im}z>0$ , define

g(z)=\operatorname{Tr}\exp\bigl(K+\operatorname{Log}(zA+B)\bigr),

where $\operatorname{Log}$ is the principal holomorphic matrix logarithm obtained by the contour-resolvent formula. Then $g$ is analytic on the upper half-plane and

\operatorname{Im}g(z)>0\qquad(\operatorname{Im}z>0).

An admissible positively oriented contour exists for each pencil value. This is Epstein’s Pick-function step; $B$ need not be positive.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P51

Formal statement

noncomputable section

open scoped Matrix ComplexOrder ComplexConjugate Matrix.Norms.L2Operator

open MeasureTheory

namespace QAlgorithms.Papers.Independent.Intakethird100.P51

attribute [local instance] Classical.propDecidable Classical.decEq

-- Exact interfaces from the frozen accepted library; no local redeclarations.

open QAlgorithms.Papers.Independent.Information100.P63 (Mat)

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

open QAlgorithms.Papers.Independent.Information100.P27 (average)

open QAlgorithms.Papers.Independent.Dependency50.P21 (relativeEntropy marginalAB channelAdjoint)

open QAlgorithms.Papers.Independent.Dependency50.P35 (marginalAC)

open QAlgorithms.Papers.Independent.Gap48.P19 (shannonNats)

open QAlgorithms.Papers.Independent.Gap48.P33 (measurementInformation)

section Statements

variable {A B C D J K O : Type}

variable [Fintype A] [Fintype B] [Fintype C] [Fintype D] [Fintype J] [Fintype K] [Fintype O]

variable [DecidableEq A] [DecidableEq B] [DecidableEq C] [DecidableEq D]

variable [DecidableEq J] [DecidableEq K] [DecidableEq O]

/-- Appendix A, equations (62)–(63), PDF p.24: Epstein's analytic Pick function.
The nonnormal pencil uses the principal contour logarithm, not Hermitian cfc. -/
theorem epsteinPick [Nonempty A] (R K B : Mat A) (hR : R.PosDef) (hK : K.IsHermitian) (hB : B.IsHermitian) :
    AnalyticOnNhd ℂ (epsteinTrace K R B) {z : ℂ | 0 < z.im} ∧
      ∀ z : ℂ, 0 < z.im →
        (∃ cr : ℂ × ℝ, UpperLogContour (z • R + B) cr.1 cr.2) ∧
        0 < (epsteinTrace K R B z).im := by sorry

end Statements

end QAlgorithms.Papers.Independent.Intakethird100.P51

end

Source

Inequalities for Quantum Entropy: A Review with Conditions for Equality, arXiv:quant-ph/0205064v2, PDF p. 24, Appendix A: Epstein trace function maps upper half-plane to itself

Read-back

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

For every finite nonempty index type $A$ , with decidable equality, and all complex matrices $R,K,B$ on $A$ such that $R$ is positive definite and $K,B$ are Hermitian, define

F(z)=\operatorname{tr}\exp\!\left(K+\mathcal L(zR+B)\right).

Here $\mathcal L(M)$ is defined as follows: if there exist $c\in\mathbb C$ and $r\in\mathbb R$ with $0<r<\operatorname{Im}c$ and $\operatorname{spec}_{\mathbb C}(M)\subseteq\{\zeta:|\zeta-c|<r\}$ , choose one such pair and set

\mathcal L(M)=\frac{1}{2\pi i} \oint_{|\zeta-c|=r}\log(\zeta)(\zeta I_A-M)^{-1}\,d\zeta;

if no such pair exists, set $\mathcal L(M)=0$ . The logarithm in this contour integral is the principal complex logarithm, and the exponential defining $F$ is the matrix exponential. The function $F$ is complex analytic in a neighborhood of every point of the open upper half-plane. Moreover, for every $z\in\mathbb C$ with $\operatorname{Im}z>0$ , a pair $c,r$ satisfying the stated contour conditions for $zR+B$ exists, and $\operatorname{Im}F(z)>0$ .

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