General DMC capacity (limit form) — publish layer #

This file is a thin publish layer on top of BlockwiseChannel/. It re-exports the limit-form capacity definition and four publish-surface theorems under a dedicated GeneralDMC namespace so that downstream modules (AWGN, MAC, BC, RelayCutset, …) can refer to GeneralDMC.capacity_lim directly without depending on BlockwiseChannel plumbing names.

For the memoryless case, every publish theorem is fully discharged via BlockwiseChannel.capacity_lim_eq_capacity_of_memoryless. For the fully general case (Han–Verdú spectral form / informationally stable channels) the publish theorems are exposed in hypothesis-form: the limit-existence / monotonicity hypothesis is taken as an explicit argument and consumed pass-through. The Han–Verdú spectral form itself is out of scope.

Main publish surface #

• GeneralDMC.capacity_lim — namespace abbrev for BlockwiseChannel.capacity_lim.
• GeneralDMC.capacity_lim_tendsto_of_memoryless — for ofMemoryless W, the per-letter capacity sequence converges to capacity W (memoryless concrete limit form).
• GeneralDMC.capacity_lim_exists_of_memoryless — limit-existence corollary in ∃ ℓ, Tendsto … shape (memoryless concrete limit form).
• GeneralDMC.capacity_lim_exists_of_subadditive — Fekete-based general limit-existence pass-through: given a real-valued subadditive surrogate that bounds the per-letter capacity, the limit exists.
• GeneralDMC.capacity_lim_eq_capacity_of_memoryless — alias of the BlockwiseChannel main theorem (the main publish target).
• GeneralDMC.capacity_lim_nonneg_of_memoryless — nonnegativity in the memoryless case (direct from the equality + capacity_nonneg).
• GeneralDMC.capacity_lim_monotone_in_n_of_memoryless — the per-letter sequence (capacityN _ n).toReal / n is monotone in n for memoryless channels (in fact eventually constant).
• GeneralDMC.capacity_lim_pass_through_of_eventually_const — monotonicity pass-through: if the per-letter sequence is eventually equal to some constant c, then capacity_lim = c.

Design #

This file is intentionally signature-stable: it does not redefine BlockwiseChannel, capacityN, or capacity_lim, and adds no new mathematical content beyond statement-level pass-through. The four publish surfaces (capacity_lim_exists, capacity_lim_nonneg, capacity_lim_monotone_in_n, capacity_lim_eq_capacity_of_memoryless) are split into a concrete memoryless flavour (discharged 0-sorry from BlockwiseChannel) and a general hypothesis-form flavour (limit-existence / monotonicity taken as an explicit argument).

References #

• InformationTheory/Shannon/BlockwiseChannel/Definition.lean

Namespace abbreviations #

We expose BlockwiseChannel and capacity_lim under the GeneralDMC namespace as plain abbreviations, so downstream code can write GeneralDMC.capacity_lim W without open-ing BlockwiseChannel.

Memoryless concrete flavour #

Pass-through of BlockwiseChannel.capacity_lim_eq_capacity_of_memoryless plus its three immediate corollaries (existence, nonnegativity, monotonicity).

General hypothesis-form flavour #

For non-memoryless channels, limit existence and monotonicity are taken as explicit hypotheses. These versions are intentionally minimal pass-through wrappers around Subadditive.tendsto_lim and Filter.Tendsto.limUnder_eq — no new mathematical content; the goal is to publish a stable downstream-facing API.