Prove2Me

Lemma 7 / Eq.(47): comparison of smooth max-informations

Open
QAlgorithms.Papers.Independent.Intakethird100.P65.smoothInfo_comparison

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 ρAB\rho_{AB} be a normalized density matrix and 0<ε<10<\varepsilon<1. Ordinary smooth max-information optimizes over subnormalized ρ~\widetilde\rho at purified distance at most the tolerance and uses ρ~A\widetilde\rho_A in the reference. Hatted smoothing additionally fixes ρ~A=ρA\widetilde\rho_A=\rho_A. Then

I^max⁡ε(A:B)ρ≤Imax⁡ε/6(A:B)ρ+log⁡2(1+72/ε2).\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.

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 7, Eq.(47), PDF p.11: hatted epsilon versus ordinary epsilon/6. -/
theorem smoothInfo_comparison (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. 11, Lemma 7 / Eq.(47): comparison of smooth max-informations
Read-back

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

For finite index types A,BA,B, with decidable equality, let ρ\rho be a positive semidefinite matrix on A×BA\times B with trace 11, and let 0<e<10<e<1. Define F(R,S)=Re⁡tr⁡R SRF(R,S)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt R\,S\sqrt R} and

P(R,S)=1−(F(R,S)+(1−Re⁡tr⁡R)(1−Re⁡tr⁡S))2.P(R,S)= \sqrt{1-\left(F(R,S)+ \sqrt{(1-\operatorname{Re}\operatorname{tr}R) (1-\operatorname{Re}\operatorname{tr}S)}\right)^2}.

The square roots of matrices are those given by continuous functional calculus. Let Be(ρ)\mathcal B_e(\rho) consist of matrices τ≥0\tau\ge0 with Re⁡tr⁡τ≤1\operatorname{Re}\operatorname{tr}\tau\le1 and P(ρ,τ)≤eP(\rho,\tau)\le e; this permits τ=0\tau=0 whenever it meets the distance condition. Define, using extended-real infima,

Dmax⁡(R∥S)=inf⁡{λ∈R:2λS−R≥0},Imax⁡(τ)=inf⁡σ≥0tr⁡σ=1Dmax⁡(τ∥(Tr⁡Bτ)⊗σ).D_{\max}(R\|S)=\inf\{\lambda\in\mathbb R:2^\lambda S-R\ge0\},\qquad I_{\max}(\tau)= \inf_{\substack{\sigma\ge0\\\operatorname{tr}\sigma=1}} D_{\max}(\tau\|(\operatorname{Tr}_B\tau)\otimes\sigma).

Then

inf⁡τ∈Be(ρ)Tr⁡Bτ=Tr⁡BρImax⁡(τ) ≤ inf⁡τ∈Be/6(ρ)Imax⁡(τ)+log⁡2(1+72e2).\inf_{\substack{\tau\in\mathcal B_e(\rho)\\ \operatorname{Tr}_B\tau=\operatorname{Tr}_B\rho}} I_{\max}(\tau) \ \le\ \inf_{\tau\in\mathcal B_{e/6}(\rho)}I_{\max}(\tau) +\log_2\left(1+\frac{72}{e^2}\right).

The partial trace has entries (Tr⁡Bτ)a,a′=∑bτ(a,b),(a′,b)(\operatorname{Tr}_B\tau)_{a,a'}=\sum_b\tau_{(a,b),(a',b)}; no attainment of either infimum is asserted.

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