AWGN channel-coding converse — mutual-information finiteness and chain #

Builds the mutual-information layer of the AWGN channel-coding converse (Cover–Thomas): the canonical joint law of (W, Yⁿ), Fano's inequality dispatch, the block-mixture output density used to bound I(W; Yⁿ), the finiteness of I(W; Yⁿ) and I(Xⁿ; Yⁿ) via the discrete-input compProd chain rule, the data-processing inequality, and the mutual-information chain rule I(Xⁿ; Yⁿ) ≤ ∑ᵢ I(Xᵢ; Yᵢ).

Main definitions #

• awgnConverseJoint — the canonical joint law of (W, Yⁿ) under a uniform message W and the memoryless AWGN channel, as the mixture (1/M) ∑ₘ δ_m ⊗ ∏ᵢ AWGN_{encoder m i}.
• perLetterYLaw — the per-coordinate output marginal of Yᵢ, a mixture of Gaussians.
• perLetterMI / jointMIWYn / jointMIXnYn — the per-letter and joint mutual informations I(Xᵢ; Yᵢ), I(W; Yⁿ), I(Xⁿ; Yⁿ) on the canonical joint.

Main statements #

• awgn_converse_single_shot_call — Fano dispatch yielding log M ≤ I(W; Yⁿ) + binEntropy(Pe) + Pe · log(M − 1).
• awgn_dpi — I(W; Yⁿ) ≤ I(Xⁿ; Yⁿ) from the Markov chain W → Xⁿ → Yⁿ.
• awgn_chain_rule — I(Xⁿ; Yⁿ) ≤ ∑ᵢ I(Xᵢ; Yᵢ) for the memoryless channel.
• awgnConverseJoint_mutualInfo_ne_top_via_chain — I(W; Yⁿ) ≠ ∞ ∧ I(Xⁿ; Yⁿ) ≠ ∞.

Implementation notes #

• The mutual informations are stated through the single canonical joint awgnConverseJoint so that data-processing and chain-rule lemmas apply directly. Finiteness of I(W; Yⁿ) and I(Xⁿ; Yⁿ) is obtained from klDiv_ne_top (absolute continuity plus integrable log-likelihood ratio), constructed directly to avoid the circularity of a Real-form chain rule, since W is discrete and Xⁿ is finite-valued.

Local quantities: joint law, output marginals, mutual informations #

Sub-bound lemmas #

The three analytic sub-bounds (per-letter log-density integrability, the continuous mutual-information chain rule, and the Markov-chain factorization) live as lemmas in InformationTheory/Shannon/AWGN/ConverseMIChainRule.lean and are invoked here as ordinary lemma calls.

Fano dispatch #

awgn_converse_single_shot_call invokes shannon_converse_single_shot with X := Fin M, Y := Fin n → ℝ, decoder := c.decoder, μ := awgnConverseJoint c h_meas, assembling Fano's inequality, the data-processing postprocessing step, the entropy chain, and H(W uniform) = log M.

Block-mixture output density #

The n-dimensional output density needed for finiteness of I(W; Yⁿ) and I(Xⁿ; Yⁿ). The block output blockYLaw is a mixture of n-dimensional product Gaussians over the finitely many codewords, so |log density| is dominated by a quadratic envelope centred at component m via a supremum upper bound together with a same-component lower bound (blockDensity ≥ M⁻¹ · (density of component m)).

Finiteness of I(W; Yⁿ) via the discrete-input compProd chain rule #

Since W = Fin M is discrete, the joint is (M⁻¹ • count) ⊗ₘ K with K m the n-dimensional block component, and the product of marginals is (M⁻¹ • count) ⊗ₘ const blockY. Finiteness follows from klDiv_ne_top (absolute continuity plus integrable log-likelihood ratio), reduced per-fibre to the output log-density integrability of each component (integrable_log_blockYLaw_on_component) and the Gaussian fibre log-density integrability.

Data-processing and chain rule #

The data-processing side derives I(W; Yⁿ) ≤ I(Xⁿ; Yⁿ) from mutualInfo_le_of_markov, with the Markov factorization supplied by awgnConverseMarkov_holds (AWGN/ConverseMIChainRule/Markov.lean). The chain-rule side connects to awgnContinuousMIChainRule_holds (AWGN/ConverseMIChainRule/PerLetterMI.lean) by definitional equality.