§III, unnumbered source/channel rate decomposition (15)–(17)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.rate_decomposition

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

prove2quantum

Let $S,X,Y,Z$ be finite nonempty alphabets and let $W(x,y,z\mid s)$ be a normalized discrete memoryless broadcast channel. All entropies and information quantities are in bits. For an input law $p$ , information quantities below use exactly the induced law $p(s)W(x,y,z\mid s)$ .

For every normalized input distribution define $R_{\rm ch}=I(S;Y)-I(S;Z)$ and $R_{\rm src}=I(X;Y\mid S)-I(X;Z\mid S)$ . Then

I(X,S;Y)-I(X,S;Z)=R_{\rm ch}+R_{\rm src}.

Neither summand is assumed nonnegative, and degradedness is unnecessary.

The identity separates the channel and residual-source contributions.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P76

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P76

noncomputable section

open scoped BigOperators

open Filter Set

attribute [local instance] Classical.propDecidable

-- Exact pinned primitives, inspected at their definitions before reuse.

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Frontier30.P12 (IsStochastic)

variable {S X Y Z : Type} [Fintype S] [Fintype X] [Fintype Y] [Fintype Z]
  [Nonempty S] [Nonempty X] [Nonempty Y] [Nonempty Z]

variable {n u w : ℕ}

/-- PDF p.5, (15)--(17): no degradedness or sign restrictions. -/
theorem rate_decomposition (W : DMBC S X Y Z) (p : S → ℝ) (hp : IsLaw p) :
    advantage W p = channelRate W p + residualSourceRate W p := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P76

Source

The Sender-Excited Secret Key Agreement Model: Capacity, Reliability and Secrecy Exponents, arXiv:1107.4148v4, PDF p. 5, §III, unnumbered source/channel rate decomposition (15)–(17)

Read-back

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

For finite nonempty alphabets $S,X,Y,Z$ , any conditional probability distributions $W_s(x,y,z)$ , and any probability law $p:S\to\mathbb R$ , meaning $p(s)\ge0$ and $\sum_sp(s)=1$ , form the joint distribution $p(s)W_s(x,y,z)$ . The declaration asserts the following equality of real numbers, with every information quantity measured in bits:

I((X,S);Y)-I((X,S);Z) = I(S;Y)-I(S;Z) +I(X;Y\mid S)-I(X;Z\mid S).

Here $I(A;B)=H(A)+H(B)-H(A,B)$ and $I(A;B\mid C)=H(A,C)-H(C)-H(A,B,C)+H(B,C)$ , using the entropy of each indicated observation under that joint distribution. No cost condition or degradation hypothesis is assumed.

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