The joint-typicality decoder (Cover–Thomas). Given a typical set A ⊆ (Fin n → ℝ) × (Fin n → ℝ) and a candidate codebook, it maps each received vector y to the smallest codeword index m with (codebook m, y) ∈ A; if no such m exists it returns the default ⟨0, …⟩ : Fin M (well-defined under [NeZero M]).

The set A is a parameter so that callers can plug in the AEP-supplied typical set directly.

The joint-typicality decoder is measurable for any measurable typical set A.

Joint measurability in (codebook, y) of jointTypicalDecoder.

Bundle c ↦ Measure.pi (fun i => awgnChannel N h_meas (c m i)) as a genuine kernel. Each fibre is a probability measure (so the kernel is Markov, hence s-finite), which lets us feed it to Kernel.measurable_kernel_prodMk_left.

The random-coding union bound (Cover–Thomas, with the typicality slack δ separated from the error target ε). With the codebook drawn from the two-stage Gaussian product law and the decoder fixed to the joint-typicality decoder against A, there is a threshold N₀ such that for every n ≥ N₀, every codebook size M ≤ ⌈exp(nR)⌉, and every measurable typical set A satisfying the two AEP bounds at slack δ, the average per-message error probability is ≤ 2ε:

• hA_mass — the joint codebook+noise law puts mass ≥ 1−ε on A.
• hA_indep — the independent-pair product law puts mass ≤ exp(−(klDiv_n − 3nδ)) on A.

The slack assumption hslack : R + 3δ < (1/2) log(1 + P/N) is what makes the alias term decay: with the typicality margin g = I − R − 3δ > 0 and klDiv_n = n·I, the alias mass is bounded by exp(−ng)·(…) → 0, hence ≤ ε past N₀. The preconditions hP : 0 < P and hN : (N:ℝ) ≠ 0 exclude the degenerate corner 1 + P/N < 0, where P.toNNReal = 0 collapses klDiv to 0 and the alias term no longer decays; under 0 < P and 0 < N we have 1 + P/N > 1 > 0. They are regularity preconditions, not a bundled proof core. @audit:ok

The random-coding union bound closed against the AEP-supplied typical set. Under the random Gaussian codebook and AWGN channel, the average per-message error probability (using jointTypicalDecoder against the AEP-supplied typical set) is ≤ 2ε for all M ≤ ⌈exp(n R)⌉ once n is large enough, given the typicality margin R + 3δ < (1/2) log(1 + P/N) with δ separate from ε.

A modular composition of continuousAepGaussian_holds + awgn_random_coding_union_bound; hP/hN are passed through to the union bound at the call site. @audit:ok