InformationTheory.Shannon.AWGN.ConverseMIChainRule.BlockMI

Imports 12

Memoryless MI chain rule: block MI decomposition #

Memoryless MI chain rule #

The chain rule I(X^n;Y^n) ≤ ∑ᵢ I(X_i;Y_i) is the textbook argument I(W;Y^n) = h(Y^n) − n·h(noise) ≤ ∑ h(Y_i) − n·h(noise) = ∑ I(X_i;Y_i), combined with the deterministic data-processing inequality I(X^n;Y^n) ≤ I(W;Y^n) (since X^n = encoder ∘ W is a measurable post-processing of W, via mutualInfo_le_of_postprocess — no Markov-chain machinery needed). The I(W;Y^n) decomposition uses the discrete-input block kernel blockKernelInline : Channel (Fin M) (Fin n → ℝ) whose measurability is free (measurable_of_countable, input Fin M), so the parallel-Gaussian kernel-measurability gap (X-input route) is sidestepped. Pieces:

the generic n-D continuous-channel MI decomposition ChannelCoding.mutualInfoOfChannel_toReal_eq_log_density_sub (the gateway atom, output type β := Fin n → ℝ, reference volume; genuine, no wall), giving I(W;Y^n).toReal = h(Y^n) − n·h(noise);
the n-D subadditivity Shannon.jointDifferentialEntropyPi_le_sum (genuine);
the per-letter 1-D decomposition mutualInfoOfChannel_toReal_eq_diffEntropy_sub (genuine), giving I(X_i;Y_i).toReal = h(Y_i) − h(noise).

The block regularity machinery mirrors the per-letter Wall-4 closure above and the ConverseMutualInfoFiniteness.lean block infrastructure.

instance

InformationTheory.Shannon.AWGN.blockKernelInline_isMarkov

source

{P : ℝ} {N : NNReal} {M n : ℕ} (c : AwgnCode M n P) :

ProbabilityTheory.IsMarkovKernel (InformationTheory.Shannon.AWGN.blockKernelInline✝ N c)

Used by

instance

InformationTheory.Shannon.AWGN.msgLawInline_isProb

source

(M : ℕ) [NeZero M] :

MeasureTheory.IsProbabilityMeasure (InformationTheory.Shannon.AWGN.msgLawInline✝ M)

Used by

noncomputable def

InformationTheory.Shannon.AWGN.blockYLawInline

source

{P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {M n : ℕ} (c : AwgnCode M n P) :

MeasureTheory.Measure (Fin n → ℝ)

Block output law Y^n = (converseJointInline).map snd (= mixture of product Gaussians). This is outputDistribution msgLawInline blockKernelInline.

Equations

InformationTheory.Shannon.AWGN.blockYLawInline h_meas c = MeasureTheory.Measure.map Prod.snd (InformationTheory.Shannon.AWGN.converseJointInline h_meas c)

Instances For

Used by

theorem

InformationTheory.Shannon.AWGN.blockYLawInline_eq_mixture

source

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

blockYLawInline h_meas c = (↑(Fintype.card (Fin M)))⁻¹ • ∑ m : Fin M, MeasureTheory.Measure.pi fun (i : Fin n) => ProbabilityTheory.gaussianReal (c.encoder m i) N

blockYLawInline = M⁻¹ • ∑ₘ pi (gaussianReal (encoder m i) N) (closed mixture form).

Used by

theorem

InformationTheory.Shannon.AWGN.blockYLawInline_ac_volume

source

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

(blockYLawInline h_meas c).AbsolutelyContinuous MeasureTheory.volume

Used by

instance

InformationTheory.Shannon.AWGN.blockYLawInline_isProb

source

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

MeasureTheory.IsProbabilityMeasure (blockYLawInline h_meas c)

Used by

theorem

InformationTheory.Shannon.AWGN.integrable_log_blockYLawInline_on_component

source

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

MeasureTheory.Integrable (fun (y : Fin n → ℝ) => Real.log ((blockYLawInline h_meas c).rnDeriv MeasureTheory.volume y).toReal) (MeasureTheory.Measure.pi fun (i : Fin n) => ProbabilityTheory.gaussianReal (c.encoder m i) N)

Per-component output log-density integrability (n-dim) against the m-th product-Gaussian fibre pi (gaussianReal (encoder m i) N). Mirror of ConverseMutualInfoFiniteness.integrable_log_blockYLaw_on_component.

Used by

theorem

InformationTheory.Shannon.AWGN.gaussianReal_logRnDeriv_integrable_inline

source

(m : ℝ) {v : NNReal} (hv : v ≠ 0) :

MeasureTheory.Integrable (fun (y : ℝ) => Real.log ((ProbabilityTheory.gaussianReal m v).rnDeriv MeasureTheory.volume y).toReal) (ProbabilityTheory.gaussianReal m v)

Per-Gaussian log-density integrability (mirror of ParallelGaussian.gaussianReal_logRnDeriv_integrable, inaccessible downstream).

Used by

theorem

InformationTheory.Shannon.AWGN.mutualInfo_encoder_le_fst

source

{P : ℝ} {N : NNReal} (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 ≤ mutualInfo (converseJointInline h_meas c) Prod.fst Prod.snd

Deterministic DPI: I(X^n;Y^n) ≤ I(W;Y^n) (X^n = encoder ∘ fst is a post-processing of W = fst).

Used by

theorem

InformationTheory.Shannon.AWGN.mutualInfo_fst_snd_ne_top

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) Prod.fst Prod.snd ≠ ⊤

I(W;Y^n) ≠ ∞ (finiteness, so .toReal is monotone).

Used by

theorem

InformationTheory.Shannon.AWGN.blockMI_decomp

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) Prod.fst Prod.snd).toReal = jointDifferentialEntropyPi (blockYLawInline h_meas c) - ↑n * differentialEntropy (ProbabilityTheory.gaussianReal 0 N)

Block MI decomposition: I(W;Y^n).toReal = h(Y^n) − n·h(noise).

Used by