InformationTheory.Shannon.BlockwiseChannel.Definition

Imports 10

Blockwise channel + capacity definitions #

A BlockwiseChannel α β is a sequence of kernels W_n : Kernel (Fin n → α) (Fin n → β) (one per block length). This file holds the core definitions: the blockwise channel type, the i.i.d. block extension Channel.toBlock, the memoryless extension ofMemoryless, and the per-block / asymptotic capacity quantities capacityN / capacity_lim.

Main definitions #

BlockwiseChannel α β := (n : ℕ) → Kernel (Fin n → α) (Fin n → β)
Channel.toBlock W n — direct Measure.pi product kernel W^{⊗n}.
BlockwiseChannel.ofMemoryless W := fun n => W.toBlock n — memoryless extension.
BlockwiseChannel.capacityN W n : ℝ≥0∞ — per-block capacity (sSup MI over probability inputs).
BlockwiseChannel.capacity_lim W : ℝ — asymptotic per-letter capacity.

Design notes:

BlockwiseChannel is the function form (n : ℕ) → Kernel _ _. No marginal consistency axiom; sufficient for the memoryless extension.
Channel.toBlock is defined directly via Measure.pi: this makes the compProd ↔ pi bridge (toBlock_compProd_pi_factor, in BlockwiseChannel.MemorylessCapacity) almost definitional via measurePreserving_arrowProdEquivProdArrow, instead of an inductive MeasurableEquiv.piFinSuccAbove construction whose bridge would require substantial self-written plumbing.

`BlockwiseChannel` definition #

def

InformationTheory.Shannon.ChannelCoding.BlockwiseChannel

source

(α : Type u_3) (β : Type u_4) [MeasurableSpace α] [MeasurableSpace β] :

Type (max u_3 u_4)

A blockwise channel is a sequence of kernels, one per block length n.

Equations

InformationTheory.Shannon.ChannelCoding.BlockwiseChannel α β = ((n : ℕ) → ProbabilityTheory.Kernel (Fin n → α) (Fin n → β))

Instances For

Used by

`Channel.toBlock W` : the i.i.d. block extension of `W` #

Defined directly as Kernel.mk (fun x => Measure.pi (fun i => W (x i))) with explicit measurability proof. This makes the compProd ↔ pi bridge below definitionally tractable via measurePreserving_arrowProdEquivProdArrow.

noncomputable def

InformationTheory.Shannon.ChannelCoding.Channel.toBlock

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (n : ℕ) :

ProbabilityTheory.Kernel (Fin n → α) (Fin n → β)

The block kernel W^{⊗n} of W, defined as Measure.pi of per-coordinate applications of W. Requires [IsMarkovKernel W] so each fibre measure is a probability measure (used in the measurability proof via the π-system route).

Equations