The uniform probability law (card X)⁻¹ • count on a nonempty finite type.

Abstract Markov-chain factorization M → g M → Y for an ambient ν ⊗ₘ κ in which the message-to-output kernel κ factors through a deterministic encoder g : M → Z and a codeword kernel Wcode : Z → Y (i.e. κ m = Wcode (g m)). This is the general shape behind the message-to-codeword-to-output chain of a multi-user converse; it needs no product/pi structure, only the factorization hκ. @audit:ok

Re-randomizing a single coordinate of a product of probability measures leaves the Measure.pi-integral unchanged. Used to peel the i-th output letter off the block channel ∏ⱼ W (xⱼ) in the memoryless-channel derivation. @audit:ok

Marginalization of a product of probability measures at a single coordinate. @audit:ok

Per-letter conditional independence for a product-channel ambient: if the message-to-output kernel factors as the per-letter product κ m = ∏ⱼ W (x m j), then at every letter i the output ω.2 i is conditionally independent of F given the input letter x ω.1 i, for any measurable F that does not read output coordinate i. Not reading that coordinate is what hFupd says — re-randomizing it leaves F unchanged — so F may read the message, hence every input letter, together with all the other output letters. @audit:ok

A product-channel ambient is a memoryless channel: if the message-to-output kernel factors as the per-letter product κ m = ∏ⱼ W (x m j) of a channel W applied to a deterministic codeword x m, then ν ⊗ₘ κ is a memoryless channel with per-letter inputs x ω.1 i and per-letter outputs ω.2 i. This is isMarkovChain_of_compProd_pi read at the conditioner that collects every input and output letter other than the i-th. @audit:ok

@audit:ok

@audit:ok

Per-letter joint pushforward of a product-channel compProd: for an ambient ν ⊗ₘ κ whose message-to-output kernel factors as the per-letter product κ m = ∏ⱼ W (x m j), the joint law of the i-th input-output pair (x ω.1 i, ω.2 i) is the channel joint (ν.map fun m ↦ x m i) ⊗ₘ W. Stated separately from isMarkovChain_of_compProd_pi, which establishes the same identity internally, because it is what identifies a per-letter information quantity of the ambient with the corresponding channel quantity.

The blockwise product u ↦ ∏ⱼ Q (u j) of a kernel Q out of a finite alphabet.

Mathlib has no Kernel.pi; over a countable alphabet with measurable singletons the family of product measures is a kernel for free, which is what Kernel.ofFunOfCountable supplies here.

Mutual information is invariant under a shared pushforward of both random variables: I(f; g) = I(f ∘ T; g ∘ T) when the pair law on μ.map T matches the pair law of the composed variables on μ.

condDistrib is stable under a shared pushforward of the conditioning and conditioned variables: condDistrib f h (μ.map T) =ᵐ condDistrib (f ∘ T) (h ∘ T) μ on the conditioning marginal (μ.map T).map h.

Conditional mutual information is invariant under a shared pushforward of all three random variables: I(f; g | h) = I(f ∘ T; g ∘ T | h ∘ T).

condMutualInfo_map_comp phrased against any measure ρ propositionally equal to μ.map T. The equation hypothesis is substituted (transporting its IsFiniteMeasure instance), which sidesteps the ill-typed motive of rewriting the measure argument of condMutualInfo directly.

If ⌈exp x⌉₊ ≤ M then x ≤ log M, converting a message count into a rate bound. From exp x ≤ ⌈exp x⌉₊ ≤ M, taking logs (both sides positive) gives x = log (exp x) ≤ log M.