Lemma 11 / Eqs.(84)–(86): permutation-covariant de Finetti smoothing

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.deFinetti_smoothing

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

prove2quantum

All systems have finite positive dimension and fixed computational bases. Matrix order is Loewner order and logarithms are base two.

Let $\mathcal N:A'\to B$ be CPTP, $n\ge1$ , and $0<\varepsilon<1$ , with $A$ a copy of $A'$ . Let $\omega_{(AA')^n}=\int\sigma_{AA'}^{\otimes n}\,d\sigma$ be the Haar pure-state moment, constructed as the normalized symmetric projector, and let $\Omega_{RA^nA'^n}$ be its canonical purification. Set $\tau=(\mathrm{id}_{RA^n}\otimes\mathcal N^{\otimes n})(\Omega)$ . Let $K_1$ consist of density matrices $\sigma_{RA^nB^n}$ with $P(\sigma,\tau)\le\varepsilon$ and $\sigma_{RA^n}=\Omega_{RA^n}$ . Let $K_2$ consist of outputs $(\mathrm{id}_{RA^n}\otimes\widetilde{\mathcal N})(\Omega)$ at distance at most $\varepsilon$ from $\tau$ , with $\widetilde{\mathcal N}$ a permutation-covariant CPTP channel. Then

\inf_{\sigma\in K_1}I_{\max}(RA^n:B^n)_\sigma=\inf_{\sigma\in K_2}I_{\max}(RA^n:B^n)_\sigma.

Covariance means $\widetilde{\mathcal N}\circ\pi_{A'^n}=\pi_{B^n}\circ\widetilde{\mathcal N}$ . This explicitly repairs the source's same-forward-permutation notation; the source proof requires inverse input conjugation. The round-one moderator independently checked this minimal inverse-permutation repair; fresh read-backs remain necessary after the other round-one edits.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P65

Formal statement

noncomputable section

open Filter QAlgorithms

open scoped BigOperators Matrix ComplexConjugate ComplexOrder Topology

namespace QAlgorithms.Papers.Independent.Intakethird100.P65

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Dependency50.P09 (transposeBob)

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

open QAlgorithms.Papers.Independent.Independent2.P01 (dampingKraus damping)

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

open QAlgorithms.Papers.Independent.Information100.P06 (Below)

open QAlgorithms.Papers.Independent.Information100.P34 (choi)

open QAlgorithms.Papers.Independent.Information100.P62 (Stochastic)

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

open QAlgorithms.Papers.Independent.Information100.P67 (IsSubnormalized purifiedDistance)

open QAlgorithms.Papers.Independent.Information100.P69 (replacer permute)

open QAlgorithms.Papers.Independent.Information100.P71 (diamond channelPower channelRelative)

open QAlgorithms.Papers.Independent.Support50.P39 (quantumMutualInformation)

variable {A B C D R : Type} [Fintype A] [DecidableEq A]
  [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C]
  [Fintype D] [DecidableEq D] [Fintype R] [DecidableEq R]

variable [Nonempty A] [Nonempty B] [Nonempty C] [Nonempty D] [Nonempty R]

/-- Lemma 11, Eqs.(84)--(86), PDF p.20. The full R A^n reference is fixed.
SOURCE NOTATION REPAIR: Perm is interpreted as covariance (inverse input
conjugation), as required by tensor-power invariance in the printed proof;
no arbitrary-superchannel monotonicity is assumed. The independent round-one
moderator checked that this only repairs the inverse in the permutation action. -/
theorem deFinetti_smoothing (N : Superop A B) (hN : IsChannel N)
    (n : ℕ) (hn : 0 < n) (e : ℝ) (h0 : 0 < e) (h1 : e < 1) :
    infoOnSet (deFinettiK1 N n e) = infoOnSet (deFinettiK2 N n e) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P65

end

Source

Quantum Channel Simulation and the Channel's Smooth Max-Information, arXiv:1807.05354v2, PDF p. 20, Lemma 11 / Eqs.(84)–(86): permutation-covariant de Finetti smoothing

Read-back

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

For finite types $A,B$ with decidable equality, every channel $N:\operatorname{Mat}(A)\to\operatorname{Mat}(B)$ , every positive integer $n$ , and every real $0<e<1$ , put $d=|A|$ and define a matrix $\Omega_n$ on $(A\times A)^n$ by

\Omega_n(x,y)= \frac{\sum_{\pi\in\operatorname{Sym}(n)}\mathbf1_{\{x=y\circ\pi\}}} {n!\binom{d^2+n-1}{n}}.

The subtraction in the binomial coefficient is natural-number subtraction, truncated at zero. Define a vector $v$ on $\mathcal R_n\times A^n$ , where $\mathcal R_n=(A\times A)^n\times A^n$ , by $v((z,u),a)=(\sqrt{\Omega_n})_{z,\,(u_i,a_i)_i}$ , let $\Xi_n=vv^\dagger$ , and let $\omega_N=(\mathrm{id}_{\mathcal R_n}\otimes N^{\otimes n})(\Xi_n)$ . Let $K_1$ consist of density matrices $\sigma$ on $\mathcal R_n\times B^n$ satisfying $P(\sigma,\omega_N)\le e$ and $\operatorname{Tr}_{B^n}\sigma=\operatorname{Tr}_{A^n}\Xi_n$ . Let $K_2$ consist of matrices $(\mathrm{id}_{\mathcal R_n}\otimes T)(\Xi_n)$ , where $T:\operatorname{Mat}(A^n)\to\operatorname{Mat}(B^n)$ is a channel satisfying $T(\Pi_\pi X)=\Pi_\pi(TX)$ for every permutation $\pi$ and every matrix $X$ , with $(\Pi_\pi X)(x,y)=X(x\circ\pi,y\circ\pi)$ , and whose resulting matrix has distance at most $e$ from $\omega_N$ . Then

\inf_{\sigma\in K_1}I_{\max}(\sigma)=\inf_{\sigma\in K_2}I_{\max}(\sigma), \quad I_{\max}(X)=\inf_{\tau\succeq0,\ \operatorname{tr}\tau=1} \inf\{\ell\in\mathbb R:2^\ell(X_{\mathcal R_n}\otimes\tau)-X\succeq0\},

where $X_{\mathcal R_n}=\operatorname{Tr}_{B^n}X$ and all these infima are extended-real infima. A density matrix is positive semidefinite with trace $1$ ; channels are finite Kraus maps with $\sum_jK_j^\dagger K_j=I$ , and tensor powers are defined by products of their matrix-unit entries. The distance is $P(X,Y)=\sqrt{1-(F_{\mathrm r}(X,Y)+\sqrt{(1-\operatorname{Re}\operatorname{tr}X)(1-\operatorname{Re}\operatorname{tr}Y)})^2}$ , where $F_{\mathrm r}(X,Y)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X}$ . Matrix square roots use continuous functional calculus, division by zero is $0$ , and empty feasible sets have infimum $+\infty$ . No nonemptiness condition on $A,B$ is displayed. The conclusion equates the infimum values, without asserting equality of $K_1$ and $K_2$ or attainment.

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