Definitions for Monotonicity of $p$ -norms of multiple operators via unitary swivels

Definition

QAlgorithms_Papers_Independent_Intakethird100_P91

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

prove2quantum

The objects the formalized statements of Monotonicity of $p$ -norms of multiple operators via unitary swivels (arXiv:1610.01262) are stated in. Each was checked against the paper by a blind read-back and a moderator.

IsSwivelTuple: The full-space unitary swivels of Theorem 1, PDF p.3. Each V_i commutes with its own C_i; there is no commutation requirement between distinct C_i. Both unitary identities are explicit, including on the kernel of C_i.
swivelValues: The set of objective values in Eq.(5), PDF p.3, including the outer real power r. Its greatest element, asserted in swivelMonotonicity, is the printed maximum. No empty/unbounded real-supremum convention is used.
boundarySup: The computed endpoint supremum M_k in Lemma 4, Eq.(26), PDF p.4. Theorem hypotheses make this real range nonempty and bounded above. Outside those hypotheses, an unbounded range has Mathlib's default sSup=0.

Definition code

import Mathlib
import Definitions.Def_QAlgorithms_Papers_Independent_Bridge50_P29

/-!
Wilde, arXiv:1610.01262v1, PDF pp.3--5. Finite complex matrices implement
footnote 2 on p.4. Only pinned accepted-library interfaces are imported.
Lemma 5 and Remark 6 are exact reuses recorded in items.json; the singular
trace-exponential preview on p.2 is deferred in HARD.md and GAPS.json.
Compilation is pending the batch handoff.
-/

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)

/-- The full-space unitary swivels of Theorem 1, PDF p.3. Each V_i commutes
with its own C_i; there is no commutation requirement between distinct C_i.
Both unitary identities are explicit, including on the kernel of C_i. -/
def IsSwivelTuple {d L : ℕ} (C V : Fin L → Matrix (Fin d) (Fin d) ℂ) : Prop :=
  ∀ i, (V i)ᴴ * V i = 1 ∧ V i * (V i)ᴴ = 1 ∧ C i * V i = V i * C i

/-- The set of objective values in Eq.(5), PDF p.3, including the outer
real power r. Its greatest element, asserted in swivelMonotonicity, is the
printed maximum. No empty/unbounded real-supremum convention is used. -/
def swivelValues {d L : ℕ} (C : Fin L → Matrix (Fin d) (Fin d) ℂ) (r : ℝ) : Set ℝ :=
  {x | ∃ V : Fin L → Matrix (Fin d) (Fin d) ℂ,
    IsSwivelTuple C V ∧
    x = (schattenNorm (ENNReal.ofReal r)
      (orderedProduct (fun i => positiveComplexPower (C i) (1 / (r : ℂ)) * V i))) ^ r}

/-- The computed endpoint supremum M_k in Lemma 4, Eq.(26), PDF p.4.
Theorem hypotheses make this real range nonempty and bounded above.
Outside those hypotheses, an unbounded range has Mathlib's default sSup=0. -/
def boundarySup {d : ℕ} (G : ℂ → Matrix (Fin d) (Fin d) ℂ)
    (p : ℝ≥0∞) (k : ℝ) : ℝ :=
  sSup (Set.range (fun t : ℝ => schattenNorm p (G ((k : ℂ) + (t : ℂ) * Complex.I))))

example {d L : ℕ} (C : Fin L → Matrix (Fin d) (Fin d) ℂ) :
    IsSwivelTuple C (fun _ => 1) := by
  intro i
  simp

example {d L : ℕ} (C : Fin L → Matrix (Fin d) (Fin d) ℂ) (r : ℝ) :
    (swivelValues C r).Nonempty := by
  refine ⟨_, (fun _ => 1), ?_, rfl⟩
  intro i
  simp

example {d : ℕ} (A : Matrix (Fin d) (Fin d) ℂ) (p : ℝ≥0∞) (k : ℝ) :
    boundarySup (fun _ => A) p k = schattenNorm p A := by
  simp [boundarySup]

end QAlgorithms.Papers.Independent.Intakethird100.P91

Source

Monotonicity of

p

-norms of multiple operators via unitary swivels, arXiv:1610.01262v1, https://arxiv.org/abs/1610.01262v1

Read-back

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

`QAlgorithms.Papers.Independent.Intakethird100.P91.IsSwivelTuple`

For arbitrary natural numbers $d,L$ , and families $C=(C_i)_{i=0}^{L-1}$ and $V=(V_i)_{i=0}^{L-1}$ of complex $d\times d$ matrices, this predicate means that, for every $i$ ,

V_i^*V_i=I_d,\qquad V_iV_i^*=I_d,\qquad C_iV_i=V_iC_i,

where $V_i^*$ is the conjugate transpose. Thus every $V_i$ is unitary and commutes with the corresponding $C_i$ ; no condition is imposed between different indices, and no positivity or Hermitian assumption is imposed on $C_i$ . Both $d=0$ and $L=0$ are allowed; when $L=0$ , the predicate is vacuously true.

`QAlgorithms.Papers.Independent.Intakethird100.P91.boundarySup`

For any natural number $d$ , any function $G:\mathbb C\to M_d(\mathbb C)$ , any extended nonnegative real $p\in[0,\infty]$ , and any real $k$ , this defines the real number

\sup_{t\in\mathbb R}S_p\bigl(G(k+it)\bigr),

where $S_\infty(B)=\|B\|_{\mathrm{op}}$ , and, for finite $p$ ,

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

Here $\operatorname{cfc}$ is functional calculus, and division and real powers are total, so $S_0(B)=1$ . No continuity, analyticity, or boundedness assumption on $G$ is part of this definition, and $d=0$ is allowed. The supremum is taken in $\mathbb R$ , rather than in the extended reals; if its set of values is unbounded above, the total real supremum used here is $0$ .

`QAlgorithms.Papers.Independent.Intakethird100.P91.swivelValues`

For arbitrary natural numbers $d,L$ , a family $C=(C_i)_{i=0}^{L-1}$ of complex $d\times d$ matrices, and a real number $r$ , this defines the set of all real numbers

\left\{\,\left[S_{\max(r,0)} \left(\prod_{i=0}^{L-1}\bigl(P_{1/r}(C_i)V_i\bigr)\right)\right]^r: V_i^*V_i=V_iV_i^*=I_d,\ C_iV_i=V_iC_i\ \text{for every }i\,\right\}.

The product is taken in increasing index order, with the empty product equal to $I_d$ , and $1/r$ in the subscript of $P$ is complex division. Here, for a Hermitian matrix $A=U\operatorname{diag}(\lambda_j)U^*$ , $P_z(A)$ is $U\operatorname{diag}(h_z(\lambda_j))U^*$ , where $h_z(0)=0$ and $h_z(x)=\exp(z\log x)$ for $x\ne0$ , using the total real logarithm; for a non-Hermitian $A$ , $P_z(A)=0$ . For a finite nonnegative parameter $s$ ,

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

where $\operatorname{cfc}$ denotes functional calculus and the powers are total real powers. There is no assumption that $r>0$ or that any $C_i$ is positive. In particular, division by zero uses $1/0=0$ , and $S_0(B)=1$ ; consequently the defined set is $\{1\}$ whenever $r\le0$ . Zero dimensions and empty families are included.

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

Definitions for Monotonicity of ppp-norms of multiple operators via unitary swivels

QAlgorithms.Papers.Independent.Intakethird100.P91.IsSwivelTuple

QAlgorithms.Papers.Independent.Intakethird100.P91.boundarySup

QAlgorithms.Papers.Independent.Intakethird100.P91.swivelValues

Definitions for Monotonicity of $p$ -norms of multiple operators via unitary swivels

`QAlgorithms.Papers.Independent.Intakethird100.P91.IsSwivelTuple`

`QAlgorithms.Papers.Independent.Intakethird100.P91.boundarySup`

`QAlgorithms.Papers.Independent.Intakethird100.P91.swivelValues`