A discrete memoryless channel (DMC) is just a (Markov) kernel α → Measure β. Markov-ness is requested as a separate type-class hypothesis on the user side, so the definition itself stays the bare Kernel.

Channel joint distribution under input law p: p ⊗ₘ W is the joint distribution of (X, Y) when X ∼ p and Y | X ∼ W X. Lives in Measure (α × β).

For a Markov kernel W and probability input p, the joint p ⊗ₘ W is a probability measure.

The output distribution of the channel under input p: q := p ⊗ₘ W projected to β, i.e. the second marginal. Used for the channel-output marginal q(y) = ∑ₓ p(x) W(y|x).

The mutual information of (X, Y) ∼ p ⊗ₘ W. Defined as klDiv (p ⊗ₘ W) (p ⊗ q) where q := outputDistribution p W. Equivalent to the standard mutualInfo of any random variable pair drawn from p ⊗ₘ W.

mutualInfoOfChannel equals MI of the joint coordinates. Unfolds the klDiv-defined mutualInfoOfChannel p W into the canonical mutualInfo (jointDistribution p W) Prod.fst Prod.snd. Used as the bridge from the channel-side formulation to the joint-distribution-side three-term identity.

Entropy ↔ mutual-information bridge for the channel. The channel mutual information equals the three-term form H(X) + H(Y) − H(X, Y) on the joint distribution p ⊗ₘ W, where H is the discrete Shannon entropy and H(X, Y) := entropy (p ⊗ₘ W) id is the joint entropy on α × β.

Composing this with entropy_eq_of_identDistrib lets the achievability consumer rewrite the joint-AEP exponent H(jointSeq Xs Ys 0) − H(Xs 0) − H(Ys 0) = −(mutualInfoOfChannel p W).toReal once the i.i.d. ambient μ := Measure.infinitePi (jointDistribution p W) is plumbed in (so that μ.map (Xs 0) = p, etc.).

A block code of length n with M messages over input alphabet α and output alphabet β: a deterministic encoder Fin M → (Fin n → α) and decoder (Fin n → β) → Fin M.

We bundle no measurability fields: on finite (or MeasurableSingletonClass) alphabets all functions are automatically measurable, so requiring fields would only force the caller to discharge measurable_of_finite redundantly.

The decoding region for message m: {y : Fin n → β | decoder y = m}.

Decoding regions are measurable on a MeasurableSingletonClass output alphabet (every set is then measurable).

The complement of the decoding region for m ("error event" for m given the output y): {y | decoder y ≠ m}.

Pointwise error probability when message m is sent through the channel W applied symbol-wise to encoder m. We model the channel output distribution given x : Fin n → α as Measure.pi (i ↦ W (x i)) — the canonical "memoryless extension" of W to length n blocks.

Average error probability under a uniform message: (1/M) ∑ m, errorProbAt c W m. For M = 0 we set this to 0 (the sum is empty).

The average error probability is bounded above by 1 (each errorProbAt ≤ 1 for a Markov kernel; summing over M terms and dividing by M keeps the bound).

Joint sequence over the product alphabet α × β.

The jointly typical set A_ε^n ⊆ (Fin n → α) × (Fin n → β): pairs (x, y) whose empirical entropies of X, Y, and (X, Y) are all within ε of the true entropies.

Implementation: the X-typical condition uses the marginal sequence Xs (via InformationTheory.Shannon.typicalSet μ Xs n ε), the Y-typical condition uses Ys, and the joint-typical condition uses the joint sequence Zs := jointSequence Xs Ys over the product alphabet α × β. We package this as the preimage of the three single-axis typical sets under the natural reshape (Fin n → α × β) ≃ (Fin n → α) × (Fin n → β).

The jointly typical set is measurable (finite product alphabet).

The jointly typical set is finite (it lives in a finite ambient space).

Bound (b): size of the jointly typical set. The size is bounded by the size of the joint single-axis typical set, at most exp(n · (H(X, Y) + ε)).

This bounds |A_ε^n| by the cardinality of the joint typical set, which is a strictly weaker (larger) bound than 2^{n(H(X,Y)+ε)} but suffices for the channel coding argument.

Bound (a): joint AEP probability. The probability that the block-joint pair (X^n, Y^n) lies in the jointly typical set tends to 1.

Bound (c): independent-pair probability. The probability under the product measure μX^n × μY^n (where μX^n := μ.map (jointRV Xs n) and similarly for Y) that (X̃, Y) lies in the jointly typical set is bounded by exp(-n(I - 3ε)) (in the log form: exp(n · (H(X,Y) - H(X) - H(Y) + 3ε))).

Mutual independence (iIndepFun) along each of the X and Y axes is required to factorise the block laws μ.map (jointRV Xs n) = Measure.pi (μ.map (Xs ·)). The joint axis identification (hidentZ) is not required for this bound (it is required only by the random-codebook average downstream of this lemma).