Schatten three-lines interpolation with arbitrary endpoint exponents

Open

QAlgorithms.Papers.Independent.Intakethird100.P91.schattenThreeLines

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

prove2quantum

Let $d\ge1$ and $S=\{z\in\mathbb C:0\le\operatorname{Re}z\le1\}$ . Let $G:S\to M_d(\mathbb C)$ be bounded, holomorphic in the interior, and continuous up to the boundary. Choose $0<\theta<1$ and arbitrary $p_0,p_1\in[1,\infty]$ , with no ordering requirement. Define $1/p_\theta=(1-\theta)/p_0+\theta/p_1$ , using $1/\infty=0$ , and set $M_k=\sup_{t\in\mathbb R}\|G(k+it)\|_{p_k}$ for $k=0,1$ . Finite Schatten norms are unnormalized and the norm at infinity is the spectral operator norm. Then

\|G(\theta)\|_{p_\theta}\le M_0^{1-\theta}M_1^\theta.

Both suprema are over nonempty bounded sets. This is the finite matrix version of the recalled three-lines result, following the entrywise convention of the source's footnote 2.

Formalization Note The Lean map is defined on all complex numbers, with hypotheses and evaluations restricted to the strip. Interior holomorphy and continuity up to its boundary are expressed by continuity on the closed strip; no constraint is imposed outside it.

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)

/-- Lemma 4, Eqs.(25)--(27), arXiv:1610.01262v1, PDF p.4.
Finite matrix interpretation follows footnote 2. G is arbitrary outside
the closed strip. The computed endpoint suprema are nonempty and finite
by strip boundedness and finite dimension. No order between p0 and p1 is
assumed; either or both may be infinity, including equal endpoints. -/
theorem schattenThreeLines
    (d : ℕ) (hd : 0 < d) (G : ℂ → Matrix (Fin d) (Fin d) ℂ)
    (hbounded : Bornology.IsBounded (G '' {z : ℂ | 0 ≤ z.re ∧ z.re ≤ 1}))
    (hholomorphic : DifferentiableOn ℂ G {z : ℂ | 0 < z.re ∧ z.re < 1})
    (hcontinuous : ContinuousOn G {z : ℂ | 0 ≤ z.re ∧ z.re ≤ 1})
    (theta : ℝ) (htheta : 0 < theta ∧ theta < 1)
    (p0 p1 : ℝ≥0∞) (hp0 : 1 ≤ p0) (hp1 : 1 ≤ p1) :
    schattenNorm (interpolationExponent theta p0 p1) (G (theta : ℂ)) ≤
      (boundarySup G p0 0) ^ (1 - theta) * (boundarySup G p1 1) ^ theta := 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, Lemma 4, Eqs.(25)–(27), footnote 2

Read-back

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

For every positive natural number $d$ , every function $G:\mathbb C\to M_d(\mathbb C)$ whose image of the closed strip $0\le\operatorname{Re}z\le1$ is bounded, which is continuous on that closed strip and complex differentiable on its interior, every real $0<\theta<1$ , and all extended nonnegative real exponents $p_0,p_1\in[1,\infty]$ , one has

S_{p_\theta}(G(\theta)) \le \left(\sup_{t\in\mathbb R}S_{p_0}(G(it))\right)^{1-\theta} \left(\sup_{t\in\mathbb R}S_{p_1}(G(1+it))\right)^\theta, \qquad \frac1{p_\theta}=\frac{1-\theta}{p_0}+\frac{\theta}{p_1},

with $1/\infty=0$ and the reciprocal of $0$ in $[0,\infty]$ equal to $\infty$ . Here $S_\infty(B)=\|B\|_{\mathrm{op}}$ , while, for finite $s\ge1$ ,

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

Each boundary supremum is the real supremum of the indicated set of values, and the powers on the right are real powers. Either or both endpoint exponents may be $\infty$ , with $p_\theta=\infty$ when both are $\infty$ ; no ordering between $p_0$ and $p_1$ is assumed, and neither $G$ nor its boundary values are required to be nonzero.

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