Theorem 1 — $C_{\epsilon,\delta}\le\max_{P_X}I(X\wedge Y|Z)$ for the wiretap channel with public feedback

Let $W:\mathcal X\to\mathcal Y\times\mathcal Z$ be a discrete memoryless wiretap channel on finite alphabets (not necessarily degraded), in which the legitimate receiver may send noiseless public feedback to the transmitter. For $0\le\epsilon,\delta$ with $\epsilon+\delta<1$, the $(\epsilon,\delta)$-wiretap capacity is bounded above as

where $I(X\wedge Y|Z)$ is the conditional mutual information (in bits) of $P_{XYZ}=P_XW$.

This is a strong converse: the bound holds for every fixed error probability $\epsilon$ and secrecy parameter $\delta$ with $\epsilon+\delta<1$, not only as $\epsilon,\delta\to0$. For a degraded wiretap channel it matches Wyner's achievable rate and so characterizes $C_{\epsilon,\delta}$ in that range.

Formalization Note $C_{\epsilon,\delta}$ is the extended-real supremum of achievable rates, over codes with randomized encoders and randomized feedback over an arbitrary feedback alphabet; the maximum over input distributions is an extended-real supremum (attained on the compact simplex).

Differences from the source:

• encoding: C_{ϵ,δ} = sup of achievable rates (0 if none) → sSup in EReal (⊥ if none); reason: both are ≤ the non-negative right-hand side; the inequality is unchanged
• encoding: max over P_X → ⨆ over FinDist X in EReal; reason: attained on the compact simplex; same value
• encoding: log base fixed by ⌊2^{nR}⌋, variation distance with factor ½ → Real.rpow 2, Nat.floor; tvDist in ℝ≥0∞ with factor 2⁻¹; reason: Lean convention; same quantities
• encoding: (possibly randomized) encoder and feedback mappings, time index t = 1, …, n, messages {1, …, N} → deterministic maps of independent local randomness Ux, Uy of arbitrary type (paper's own representation, proof of Lemma 7), arbitrary feedback alphabet, 0-based rounds, Fin N; reason: Lean convention; the same class of codes