Lemma 6: conditional Ahlswede–Csiszar sum identity (attributed prior result)

Open

QAlgorithms.Papers.Independent.Intakethird100.P76.conditional_sum_identity

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

prove2quantum

Let $K,\Phi,Y^n,Z^n$ be arbitrary finite random variables on one normalized finite probability space. All information is in bits. Then

I(K;Y^n\mid\Phi)-I(K;Z^n\mid\Phi)=\sum_{i=1}^n\bigl[I(K;Y_i\mid Y^{i-1},Z_{i+1}^n,\Phi)-I(K;Z_i\mid Y^{i-1},Z_{i+1}^n,\Phi)\bigr].

The case $n=0$ has empty sum and zero on both sides. The Lean masks store exactly the prefix before $i$ and suffix after $i$ , with fixed none entries elsewhere.

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.11, Lemma 6, explicitly attributed there to Ahlswede--Csiszar
[3, Lemma 4.1]. Arbitrary finite random variables on one normalized sample law.
The Option masks encode exactly Y before i and Z after i; all other entries
are fixed None and carry no information. For n=0 both sides are zero. -/
theorem conditional_sum_identity {O K P A B : Type*}
    [Fintype O] [Fintype K] [Fintype P] [Fintype A] [Fintype B]
    (p : O → ℝ) (hp : IsLaw p) (k : O → K) (phi : O → P)
    (n : ℕ) (y : O → Fin n → A) (z : O → Fin n → B) :
    condInfo p k y phi - condInfo p k z phi =
      ∑ i : Fin n,
        (condInfo p k (fun o => y o i)
          (fun o => ((fun j : Fin n => if j < i then some (y o j) else none),
            (fun j : Fin n => if i < j then some (z o j) else none), phi o)) -
        condInfo p k (fun o => z o i)
          (fun o => ((fun j : Fin n => if j < i then some (y o j) else none),
            (fun j : Fin n => if i < j then some (z o j) else none), phi o))) := 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. 11, Lemma 6, explicitly citing [3, Lemma 4.1]

Read-back

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

Let $O,K,P,A,B$ be finite types, let $p:O\to\mathbb R$ satisfy $p(o)\geq0$ for every $o$ and $\sum_op(o)=1$ , let $k:O\to K$ and $\phi:O\to P$ , let $n\geq0$ be a natural number, and let $y:O\to A^n$ and $z:O\to B^n$ . For any observation $U$ on $O$ , define

H(U)=-\sum_{o\in O}p(o)\log_2\!\left(\sum_{t:\,U(t)=U(o)}p(t)\right),\qquad H(U\mid V)=H(U,V)-H(V),\qquad I(U;V\mid T)=H(U\mid T)-H(U\mid V,T),

using the total real logarithm, so $\log_2 0=0$ . For each $i\in\{0,\ldots,n-1\}$ , define the conditioning observation $T_i(o)$ to be the triple consisting of the length- $n$ array whose $j$ -th entry is $y(o)_j$ marked as present when $j<i$ and is absent otherwise, the length- $n$ array whose $j$ -th entry is $z(o)_j$ marked as present when $i<j$ and is absent otherwise, and $\phi(o)$ . Then

I(k;y\mid\phi)-I(k;z\mid\phi) =\sum_{i=0}^{n-1} \left[I(k;y_i\mid T_i)-I(k;z_i\mid T_i)\right].

Here $y$ and $z$ on the left are the entire tuple-valued observations, and the coordinate $i$ itself is excluded from both arrays in $T_i$ . The case $n=0$ is included: the sum is empty and equals $0$ , while both tuple observations are constant. The probability hypothesis cannot hold when $O$ 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