Memoryless blockwise capacity: the per-n equality #

For memoryless DMC (ofMemoryless W, with all W_n := ⊗_n W), the per-block capacity reduces to n · capacity W. This file establishes that per-n equality capacityN_ofMemoryless_eq via:

• the structural bridge toBlock_compProd_pi_factor (compProd ↔ pi),
• i.i.d. input MI multiplicativity mutualInfoOfChannel_pi_iid_eq_nsmul (the ≥ direction),
• the per-letter marginal bridge and Cover-Thomas chain (the ≤ direction).

Main statements #

• capacityN_ofMemoryless_eq — (ofMemoryless W).capacityN n matches n · capacity W (per-n equality).

The asymptotic limit form capacity_lim_eq_capacity_of_memoryless is in BlockwiseChannel.CapacityLimit.

Structural bridge toBlock_compProd_pi_factor #

With Channel.toBlock defined directly via Measure.pi, the bridge becomes nearly definitional: (Measure.pi p) ⊗ₘ (toBlock W n) lives on (Fin n → α) × (Fin n → β), and pushing it through the canonical equiv to Fin n → α × β recovers Measure.pi (fun i => p i ⊗ₘ W) via measurePreserving_arrowProdEquivProdArrow.symm.

Helper: arbitrary measure MI ≤ capacity #

i.i.d. input MI multiplicativity #

The key identity behind the ≥ direction: for an i.i.d. product input q := Measure.pi (fun _ : Fin n => p₀), the channel mutual information with the block kernel W^{⊗n} factors as n • I(p₀; W). Proven by pushing both joint and marginal-product through the canonical (Fin n → α × β) ≃ᵐ (Fin n → α) × (Fin n → β) and applying klDiv_pi_eq_sum.

≤ direction — per-letter marginal bridge #

The ≤ direction capacityN_ofMemoryless_le reduces per-block MI to a sum of per-letter MIs via the Cover-Thomas chain (subadditivity + memoryless splitting of conditional entropy). The chain reduces to two IsMarkovChain facts about μ := q ⊗ₘ (Channel.toBlock W n), each established via a condDistrib identification.

The ≥ direction (capacityN_ofMemoryless_ge) goes through via mutualInfoOfChannel_pi_iid_eq_nsmul, giving the i.i.d.-input achievability of n · capacity W. Combined with capacityN_ofMemoryless_le, the full equality capacityN_ofMemoryless_eq and limit form capacity_lim_eq_capacity_of_memoryless follow.

The per-letter marginal bridge (per_letter_marginal_eq_compProd) and per-letter MI identification (mutualInfo_per_letter_eq_marginal) below are the building blocks for the ≤ direction.