Lemma 9 / Eq.(73): appendix repetition of Lemma 7

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.smoothInfo_comparison_appendix

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 density matrix and $0<\varepsilon<1$ . Ordinary smooth max-information optimizes over subnormalized $\widetilde\rho$ at purified distance at most the tolerance and uses $\widetilde\rho_A$ in the reference. Hatted smoothing additionally fixes $\widetilde\rho_A=\rho_A$ . Then

\widehat I_{\max}^{\varepsilon}(A:B)_\rho\le I_{\max}^{\varepsilon/6}(A:B)_\rho+\log_2(1+72/\varepsilon^2).

Purified distance uses generalized root fidelity. This compares free and fixed-marginal smoothing without any rank assumption.

This is the separate numbered occurrence in Appendix B, Lemma 9.

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 9, Eq.(73), PDF pp.18--19: the numbered appendix occurrence of Lemma 7. -/
theorem smoothInfo_comparison_appendix (rho : Mat (A × B)) (hrho : IsDensityMatrix rho)
    (e : ℝ) (h0 : 0 < e) (h1 : e < 1) :
    fixedSmoothInfo rho e ≤ smoothInfo rho (e/6) + (Real.logb 2 (1 + 72/e^2) : EReal) := 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. 18, Lemma 9 / Eq.(73): appendix repetition of Lemma 7

Read-back

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

For finite types $A,B$ with decidable equality, every positive semidefinite complex matrix $\rho$ on $A\times B$ with $\operatorname{tr}\rho=1$ , and every real $0<e<1$ , write $X_A=\operatorname{Tr}_B X$ , so $(X_A)_{a,a'}=\sum_bX_{(a,b),(a',b)}$ , and define

I_{\max}(X)=\inf_{\sigma_B\succeq0,\ \operatorname{tr}\sigma_B=1} D_{\max}(X\|X_A\otimes\sigma_B),\qquad D_{\max}(X\|Y)=\inf\{\ell\in\mathbb R:2^\ell Y-X\succeq0\},

with these infima taken in the extended reals. For positive semidefinite matrices of real trace at most $1$ , put

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}.

The assertion is

\inf_{\substack{\tau\succeq0,\ \operatorname{Re}\operatorname{tr}\tau\le1\\ P(\rho,\tau)\le e,\ \tau_A=\rho_A}}I_{\max}(\tau) \ \le\ \inf_{\substack{\tau\succeq0,\ \operatorname{Re}\operatorname{tr}\tau\le1\\ P(\rho,\tau)\le e/6}}I_{\max}(\tau) +\log_2(1+72/e^2).

Matrix square roots here are defined by continuous functional calculus. The smoothing definitions allow $\tau=0$ , although its distance from the normalized $\rho$ is $1$ , so the displayed tolerances exclude it; the fixed marginal condition also forces $\operatorname{tr}\tau=1$ . Empty feasible sets have extended-real infimum $+\infty$ . No nonemptiness assumption on the register types is displayed, but a trace-one $\rho$ cannot exist if either 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