InformationTheory.Shannon.AWGN.ConverseMIChainRule.PerLetterMI

source

Imports 13

Per-letter MI decomposition and continuous MI chain rule #

instance

InformationTheory.Shannon.AWGN.perLetterInputLaw_isProb

source

{P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} [NeZero M] (c : AwgnCode M n P) (i : Fin n) :

MeasureTheory.IsProbabilityMeasure (InformationTheory.Shannon.AWGN.perLetterInputLaw✝ h_meas c i)

Used by

theorem

InformationTheory.Shannon.AWGN.awgnContinuousMIChainRule_holds

source

{P : ℝ} {N : NNReal} (hN : N ≠ 0) (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} [NeZero M] (c : AwgnCode M n P) :

(mutualInfo (converseJointInline h_meas c) (fun (ω : Fin M × (Fin n → ℝ)) => c.encoder ω.1) Prod.snd).toReal ≤ ∑ i : Fin n, (mutualInfo (converseJointInline h_meas c) (fun (ω : Fin M × (Fin n → ℝ)) => c.encoder ω.1 i) fun (ω : Fin M × (Fin n → ℝ)) => ω.2 i).toReal

Memoryless AWGN continuous MI chain rule.

I(X^n; Y^n) ≤ ∑ᵢ I(X_i; Y_i) on the inlined joint. The route: I(X^n;Y^n) ≤ I(W;Y^n) (deterministic DPI) = h(Y^n) − n·h(noise) ≤ ∑ h(Y_i) − n·h(noise) = ∑ I(X_i;Y_i), combining mutualInfo_encoder_le_fst, blockMI_decomp, jointDifferentialEntropyPi_blockYLawInline_le_sum, and perLetterMI_decomp. Consumer-side unfold jointMIXnYn perLetterMI awgnConverseJoint gives defeq.

[NeZero M] (M ≥ 1, so the uniform message law is a probability measure) and hN : N ≠ 0 (full-support Gaussian fibres ⇒ blockYLaw absolutely continuous) are regularity preconditions, both supplied by the converse consumer. They are not load-bearing: the MI inequality is proved from the entropy chain, not encoded in the hypotheses (at the degenerate boundary N = 0 the Gaussian fibres collapse to Diracs, breaking only the density route, while the MI inequality itself stays true since it is KL≥0-backed). @audit:ok

Used by