Lemma 12 / Eq.(97): fixed-marginal mutual-information continuity

Open

QAlgorithms.Papers.Independent.Intakethird100.P65.fixedMarginal_continuity

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},\sigma_{AB}$ be normalized density matrices with $\rho_A=\sigma_A$ , and let $\varepsilon\ge0$ satisfy $\tfrac12\|\rho-\sigma\|_1\le\varepsilon$ . Then

|I(A:B)_\rho-I(A:B)_\sigma|\le2\varepsilon\log_2|A|+(1+\varepsilon)h_2\!\left(\frac{\varepsilon}{1+\varepsilon}\right).

Here $h_2$ is binary entropy in bits. The dimension is that of the fixed reference system $A$ , and singular states are permitted.

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 12, Eq.(97), PDF p.21: fixed A marginal, half trace distance,
log dimension of A, and epsilon/(1+epsilon). -/
theorem fixedMarginal_continuity (rho sigma : Mat (A × B))
    (hrho : IsDensityMatrix rho) (hsigma : IsDensityMatrix sigma)
    (hmarg : traceRight rho = traceRight sigma) (e : ℝ) (he : 0 ≤ e)
    (hdist : traceNorm (rho - sigma) / 2 ≤ e) :
    |quantumMutualInformation rho - quantumMutualInformation sigma| ≤
      2*e*Real.logb 2 (Fintype.card A) + (1+e)*binEntropy2 (e/(1+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. 21, Lemma 12 / Eq.(97): fixed-marginal mutual-information continuity

Read-back

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

For finite types $A,B$ with decidable equality, let $\rho,\sigma$ be positive semidefinite matrices on $A\times B$ , each of trace $1$ , whose $A$ -marginals agree: $\operatorname{Tr}_B\rho=\operatorname{Tr}_B\sigma$ . For every real $e\ge0$ satisfying $\tfrac12\|\rho-\sigma\|_1\le e$ , the assertion is

\left|I(\rho)-I(\sigma)\right| \le 2e\log_2|A|+(1+e)\,h_2\!\left(\frac{e}{1+e}\right).

Here $I(X)=S(\operatorname{Tr}_B X)+S(\operatorname{Tr}_A X)-S(X)$ , $S(X)=-\operatorname{Re}\operatorname{tr}f(X)$ with $f(x)=x\log_2x$ applied by continuous functional calculus, and $h_2(t)=\operatorname{binEntropy}(t)/\log2$ , where $\operatorname{binEntropy}(t)=-t\log t-(1-t)\log(1-t)$ uses the total real logarithm, including $\log0=0$ . The trace norm is $\|X\|_1=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , and each partial trace sums over the discarded diagonal index. The bound depends on $|A|$ ; there is no upper restriction on $e$ , and $e=0$ is included. If either register is empty, the density hypotheses are impossible.

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