Multioperator trace-exponential inequality

Open

QAlgorithms.Papers.Independent.Intakethird100.P91.traceExponentialInequality

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

prove2quantum

Let $d,L\ge1$ be integers and let $C_1,\ldots,C_L$ act on the common space $\mathbb C^d$ , with products in the displayed order. For $1\le r<\infty$ , write $\|X\|_r=(\operatorname{Tr}(X^*X)^{r/2})^{1/r}$ for the unnormalized Schatten norm. On a positive eigenvalue $\lambda$ , $C^z$ acts by $\exp(z\log\lambda)$ , and it acts by zero on the kernel. No commutation between different factors or trace normalization is assumed.

Assume every $C_i$ is positive definite, let $q\ge1$ be finite and real, and put $\beta_0(t)=\pi/(2[\cosh(\pi t)+1])$ . The matrix logarithms are the self-adjoint spectral natural logarithms and $\exp$ is the matrix exponential. Then

\log\operatorname{Tr}\exp\!\left(\sum_{j=1}^{L}\log C_j\right) \le\int_{\mathbb R}\beta_0(t) \log\left(\left\|C_1^{(1+it)/q}\cdots C_L^{(1+it)/q}\right\|_q^q\right)\,dt.

All displayed logarithms are finite; the weighted integrand is integrable. This is the trace-exponential consequence of multioperator interpolation in the positive definite setting.

Formalization Note The real part of the complex matrix trace is used on the left; for the exponential of the self-adjoint sum this trace is real and positive.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P91

Formal statement

noncomputable section

open scoped Matrix ComplexConjugate ComplexOrder ENNReal Matrix.Norms.L2Operator

namespace QAlgorithms.Papers.Independent.Intakethird100.P91

open QAlgorithms.Papers.Independent.Information100.P50 (schattenNorm)

open QAlgorithms.Papers.Independent.Dependency50.P21
  (extendedLog upperLogIntegral betaDensity betaZero interpolationExponent)

open QAlgorithms.Papers.Independent.Bridge50.P29
  (positiveComplexPower orderedProduct)

/-- Corollary 3, Eq.(22), arXiv:1610.01262v1, PDF p.4.
The C_i are positive DEFINITE as printed in this numbered corollary.
The left side is the log of the trace of the exponential of the SUM of
spectral natural logarithms. The right side uses beta_0 and the q-th
power inside the log. Positive definiteness makes all these logs finite;
no Lie--Trotter identity or integrability conclusion is assumed. -/
theorem traceExponentialInequality
    (d L : ℕ) (hd : 0 < d) (hL : 0 < L)
    (C : Fin L → Matrix (Fin d) (Fin d) ℂ)
    (hC : ∀ i, (C i).PosDef)
    (q : ℝ) (hq : 1 ≤ q) :
    extendedLog ((NormedSpace.exp (∑ i, cfc Real.log (C i))).trace.re) ≤
    upperLogIntegral (fun t =>
      (betaZero t : EReal) *
        extendedLog ((schattenNorm (ENNReal.ofReal q)
          (orderedProduct (fun i => positiveComplexPower (C i)
            ((1 + (t : ℂ) * Complex.I) / (q : ℂ))))) ^ q)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P91

end

Source

Monotonicity of

p

-norms of multiple operators via unitary swivels, arXiv:1610.01262v1, PDF p. 4, Corollary 3, Eq.(22)

Read-back

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

For every pair of positive natural numbers $d,L$ , every family $C=(C_i)_{i=0}^{L-1}$ of positive definite complex $d\times d$ matrices, and every real $q\ge1$ , the following extended-real inequality holds:

\ell\left(\operatorname{Re}\operatorname{Tr} \exp\left(\sum_{i=0}^{L-1}\log C_i\right)\right) \le \mathcal U\left( t\mapsto \frac{\pi}{2(\cosh(\pi t)+1)} \,\ell\left(\left[S_q\left( \prod_{i=0}^{L-1}C_i^{(1+it)/q}\right)\right]^q\right) \right).

The exponential is the matrix exponential, $\log C_i$ is functional calculus with the real logarithm, the product is in increasing index order, and $C_i^z$ replaces each eigenvalue $\lambda>0$ by $\exp(z\log\lambda)$ . The quantity $S_q(B)$ is

\left(\operatorname{Re}\operatorname{Tr} \left[\operatorname{cfc}\!\left(u\mapsto u^{q/2},B^*B\right)\right]\right)^{1/q}.

The function $\ell$ is $\log$ on positive real inputs and $-\infty$ on nonpositive inputs. For an extended-real-valued function $f$ , $\mathcal U(f)$ is the nonnegative Lebesgue integral of its positive part minus that of its negative part, using extended-real subtraction; no additional integrability hypothesis is stated. The assumptions exclude zero dimensions, empty families, and singular $C_i$ , and include $q=1$ .

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