The jointly typical set is symmetric in its two blocks: a pair (x, y) is jointly typical for (Xs, Ys) exactly when the swapped pair (y, x) is jointly typical for (Ys, Xs). Both the per-letter log-likelihood and the joint entropy are invariant under the swap, so the three bands defining membership are exchanged rather than changed.

Uniform bound on the conditional slices of the jointly typical set taken along the first block: whatever the second word y, the i.i.d. law of the first sequence gives the set of words jointly typical with y mass at most exp(-n (I(X; Y) - 3ε)), where I(X; Y) is read as H(X) + H(Y) - H(X, Y).

The mirror image of measureReal_jointlyTypicalFiber_le, slicing along the second block: the same exponential bound holds for the mass the i.i.d. law of the second sequence gives to the words jointly typical with a prescribed first word x. The covering estimate needs both families, since the second-moment argument controls the two directions of the pair count separately.

A pair of codebooks read as the single padded family of codewords carried by the canonical ambient of the second-moment estimate: the i-th codeword of the first codebook is padded by a constant in the second alphabet and vice versa.

The sharpened mutual covering estimate, read on a product of two independent codebook ensembles.

The Lipschitz factor by which the type radius of a jointly strongly typical pair has to be amplified to reach the weak bands of the two blocks and of their joint sequence. It is the single constant governing both directions the covering estimate needs: the exponential lower bound on the mass of the strongly typical set, and the slice bound obtained by reading that set inside a weakly typical set of the widened radius.

@audit:ok

Mutual covering for a pair of independent i.i.d. codebook ensembles. Writing I = H(X) + H(Y) - H(X, Y) for the dependence between the two sequences, if the two subcodebook rates R₁', R₂' add up to more than I and ε is small enough compared with both the slack R₁' + R₂' - I and the individual rates, then the probability that no pair of codewords is jointly typical drops below any prescribed η.

Mutual covering at a jointly strongly typical pair. The strongly typical set is smaller than the weakly typical one, so this bound implies the weak reading of ε-widened radius; the price is that the covering rate conditions are stated at the radius amplified by coveringBandConst, which is what converts the strong radius into the weak bands governing both the mass of the set and its conditional slices.

@audit:ok

Mutual covering for Marton's auxiliary codebooks at a prescribed typicality parameter. The parameter ε is a hypothesis rather than an output, so that a consumer may choose one ε meeting the smallness conditions here together with those of the decoding analysis; marton_mutual_covering is the form in which ε is chosen, uniformly in the failure level η.

@audit:ok

Marton's mutual covering lemma. Two subcodebooks are drawn independently, the first from the V₁-marginal of the auxiliary law and the second from its V₂-marginal, at positive rates R₁' and R₂' whose sum exceeds the dependence I(V₁; V₂) between the auxiliary variables. Then for every prescribed bound ε₀ there is a typicality parameter ε < ε₀ for which the probability that no pair of codewords is jointly typical falls below any prescribed failure level η at every large enough blocklength. The single ε works for all η, so the failure probability tends to zero as the blocklength grows.

The upper bound ε < ε₀ is what gives the conclusion content. A typicality radius wide enough to swallow the whole space empties the failure event, so a statement asserting only 0 < ε would be satisfied by a vacuous witness independently of the rates.

The hypotheses hpV, hK, hW are the full-support regularity preconditions shared by every typicality bound in this development; they are what rules out a deterministic input map x = f(v₁, v₂) and forces the general-kernel formulation.

@audit:ok

Mutual covering with independent auxiliary variables, where the covering threshold I(V₁; V₂) vanishes and every pair of positive rates therefore qualifies. The typicality parameter is again produced below any prescribed bound ε₀, uniformly in the failure level. This is the degenerate regime of Marton's inner bound, and it certifies that the hypotheses of marton_mutual_covering are jointly satisfiable.

@audit:ok

The Lipschitz factor relating the type radius of a jointly strongly typical auxiliary pair to the weak bands of the two auxiliary blocks and of their joint sequence. It is the covering counterpart of martonBandConst, which governs the transmitted (V₁, X) pair instead.

@audit:ok

Mutual covering for Marton's auxiliary codebooks at a prescribed typicality parameter, with the covering set read as the jointly strongly typical one. This is the form the encoder's selection rule consumes: a strongly typical selected pair is what pins the empirical type of the transmitted words, which the receiver-1 conditional AEP needs.

@audit:ok

Marton's mutual covering lemma at the strongly typical set. Two subcodebooks are drawn independently, the first from the V₁-marginal of the auxiliary law and the second from its V₂-marginal, at positive rates R₁' and R₂' whose sum exceeds the dependence I(V₁; V₂) between the auxiliary variables. Then for every prescribed bound ε₀ there is a typicality parameter ε < ε₀ for which the probability that no pair of codewords is jointly strongly typical falls below any prescribed failure level η at every large enough blocklength. The single ε works for all η, so the failure probability tends to zero as the blocklength grows.

This is strictly stronger than marton_mutual_covering: the strongly typical set is contained in the weakly typical one of the radius widened by martonCoveringBandConst, so the event bounded here contains the weak one.

The upper bound ε < ε₀ is what gives the conclusion content. A typicality radius wide enough to swallow the whole space empties the failure event, so a statement asserting only 0 < ε would be satisfied by a vacuous witness independently of the rates.

The hypotheses hpV, hK, hW are the full-support regularity preconditions shared by every typicality bound in this development; they are what rules out a deterministic input map x = f(v₁, v₂) and forces the general-kernel formulation.

@audit:ok

Strongly typical mutual covering with independent auxiliary variables, where the covering threshold I(V₁; V₂) vanishes and every pair of positive rates therefore qualifies. The typicality parameter is again produced below any prescribed bound ε₀, uniformly in the failure level. This is the degenerate regime of Marton's inner bound, and it certifies that the hypotheses of marton_strong_mutual_covering are jointly satisfiable.

@audit:ok