Appendix B / Eq.(78): changing the reference marginal in smoothing

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.change_reference_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 $\rho_{AB}$ be a normalized state and $0<\varepsilon<1$ . Define $\widetilde I_{\max}^{\varepsilon}(A:B)_\rho$ by optimizing $D_{\max}(\tau_{AB}\|\rho_A\otimes\sigma_B)$ over subnormalized $\tau$ at purified distance at most $\varepsilon$ and normalized $\sigma_B$ . Ordinary smoothing uses $\tau_A$ instead of $\rho_A$ . Then

\widetilde I_{\max}^{\varepsilon}(A:B)_\rho\le I_{\max}^{\varepsilon/2}(A:B)_\rho.

No constraint $\tau_A=\rho_A$ is imposed in the tilde quantity. Singular marginals are allowed.

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]

/-- Appendix B, Eq.(78), PDF p.19: tilde smoothing versus ordinary smoothing;
no invertibility assumption is added. -/
theorem change_reference_smoothing (rho : Mat (A × B)) (hrho : IsDensityMatrix rho)
    (e : ℝ) (h0 : 0 < e) (h1 : e < 1) :
    referenceSmoothInfo rho e ≤ smoothInfo rho (e/2) := 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. 19, Appendix B / Eq.(78): changing the reference marginal in 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 matrix $\rho\succeq0$ on $A\times B$ with $\operatorname{tr}\rho=1$ , and every real $0<e<1$ , let $X_A=\operatorname{Tr}_B X$ , let $D_{\max}(X\|Y)=\inf\{\ell\in\mathbb R:2^\ell Y-X\succeq0\}$ in the extended reals, and let $P$ be the distance

P(X,Y)=\sqrt{1-\left( \operatorname{Re}\operatorname{tr}\sqrt{\sqrt X\,Y\sqrt X} +\sqrt{(1-\operatorname{Re}\operatorname{tr}X)(1-\operatorname{Re}\operatorname{tr}Y)} \right)^2}.

Then

\inf_{\substack{\tau\succeq0,\ \operatorname{Re}\operatorname{tr}\tau\le1\\P(\rho,\tau)\le e}} \ \inf_{\sigma_B\succeq0,\ \operatorname{tr}\sigma_B=1} D_{\max}(\tau\|\rho_A\otimes\sigma_B) \ \le\ \inf_{\substack{\tau\succeq0,\ \operatorname{Re}\operatorname{tr}\tau\le1\\P(\rho,\tau)\le e/2}} \ \inf_{\sigma_B\succeq0,\ \operatorname{tr}\sigma_B=1} D_{\max}(\tau\|\tau_A\otimes\sigma_B).

The partial trace has entries $(X_A)_{a,a'}=\sum_bX_{(a,b),(a',b)}$ , and matrix square roots use continuous functional calculus. Neither side requires $\tau_A=\rho_A$ ; on the left, $\rho_A$ is used only in the reference matrix inside $D_{\max}$ . The smoothing sets allow zero subnormalized matrices by definition, but $P(\rho,0)=1$ excludes zero at these tolerances. Extended-real infima over empty sets equal $+\infty$ ; the density hypothesis is impossible if either finite register is empty.

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