Logarithmic multioperator interpolation

Open

QAlgorithms.Papers.Independent.Intakethird100.P91.logarithmicInterpolation

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 semidefinite, and let $1\le q<p$ be finite real numbers. Define $\beta_\theta(t)=\sin(\pi\theta)/(2\theta[\cosh(\pi t)+\cos(\pi\theta)])$ for $0<\theta<1$ . Then

\log\left(\left\|C_1^{1/p}\cdots C_L^{1/p}\right\|_p^p\right) \le\int_{\mathbb R}\beta_{q/p}(t) \log\left(\left\|C_1^{(1+it)/q}\cdots C_L^{(1+it)/q}\right\|_q^q\right)\,dt.

Here $i=\sqrt{-1}$ , scalar logarithms are natural with $\log0=-\infty$ , and the integral is the signed extended Lebesgue integral. Its positive part is finite, while its negative part may be infinite. This bound gives explicit interpolation without optimizing over unitaries, and covers zero factors.

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)

/-- Theorem 2, Eq.(18), arXiv:1610.01262v1, PDF pp.3--4.
The outer powers p and q remain INSIDE their natural logarithms.
Zero eigenvalues have support-zero powers; extendedLog(0)=-infinity.
The signed extended integral retains an infinite negative part, with its
positive part finite by boundedness of these finite matrix products and
the beta probability density. There is no unitary optimization here. -/
theorem logarithmicInterpolation
    (d L : ℕ) (hd : 0 < d) (hL : 0 < L)
    (C : Fin L → Matrix (Fin d) (Fin d) ℂ)
    (hC : ∀ i, (C i).PosSemidef)
    (p q : ℝ) (hq : 1 ≤ q) (hqp : q < p) :
    extendedLog ((schattenNorm (ENNReal.ofReal p)
      (orderedProduct (fun i => positiveComplexPower (C i) (1 / (p : ℂ))))) ^ p) ≤
    upperLogIntegral (fun t =>
      (betaDensity (q / p) 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. 3, Theorem 2, Eq.(18), proof p.4

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 semidefinite complex $d\times d$ matrices, and all real $p,q$ satisfying $1\le q<p$ , the following inequality holds in the extended real numbers:

\ell\left(\left[S_p\left(\prod_{i=0}^{L-1}C_i^{1/p}\right)\right]^p\right) \le \mathcal U\left( t\mapsto b_{q/p}(t)\, \ell\left(\left[S_q\left(\prod_{i=0}^{L-1}C_i^{(1+it)/q}\right)\right]^q\right) \right).

Products are in increasing index order; for a positive semidefinite $A$ , $A^z$ replaces every positive eigenvalue $\lambda$ by $\exp(z\log\lambda)$ and every zero eigenvalue by $0$ . For $s>0$ ,

S_s(B)= \left(\operatorname{Re}\operatorname{Tr} \left[\operatorname{cfc}\!\left(u\mapsto u^{s/2},B^*B\right)\right]\right)^{1/s}, \qquad b_a(t)=\frac{\sin(\pi a)} {2a\bigl(\cosh(\pi t)+\cos(\pi a)\bigr)}.

Here $\ell(x)=\log x$ when $x>0$ , and $\ell(x)=-\infty$ when $x\le0$ ; for an extended-real-valued function $f$ , $\mathcal U(f)$ is defined as the nonnegative Lebesgue integral of its positive part minus the nonnegative Lebesgue integral of its negative part, with both integrals cast to the extended reals and subtraction performed there. No separate integrability or finiteness hypothesis is imposed on this expression. The hypotheses ensure $0<q/p<1$ , but permit singular or zero matrices $C_i$ , so the extended logarithms need not be finite.

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