InformationTheory.Shannon.AWGN.ConverseMIChainRule.Markov
Deterministic-encoder Markov factorization #
Markov factorization #
InformationTheory.Shannon.AWGN.awgnConverseMarkov_holds
source{P : ℝ}
{N : NNReal}
(h_meas : IsAwgnChannelMeasurable N)
{M n : ℕ}
[NeZero M]
(c : AwgnCode M n P)
:
IsMarkovChain (converseJointInline h_meas c) Prod.fst (fun (ω : Fin M × (Fin n → ℝ)) => c.encoder ω.1) Prod.snd
Markov chain W → encoder ∘ W → Y^n factorization.
IsMarkovChain (converseJointInline h_meas c) Prod.fst (encoder ∘ fst) Prod.snd, the
joint factorization.
The argument starts from the identity μ = (μ.map fst) ⊗ₘ (W.comap encoder) (with μ the
message-space marginal and W := Channel.toBlock (awgnChannel N) n the noise block kernel),
established on the mixture-of-diracs via ext_of_lintegral (h_marginalA). From it,
condDistrib Yo Zc μ =ᵐ W (condDistrib_ae_eq_of_measure_eq_compProd); then condDistrib Xs Zc μ
is absorbed via compProd_map_condDistrib, and the triple-joint factorization is verified by
ext_of_lintegral + the h_marginalA reduction (precedent:
BlockwiseChannel.isMarkovChain_per_letter_input).
@audit:ok