InformationTheory.Shannon.ParallelGaussian.Converse.Regularity

instance

InformationTheory.Shannon.ParallelGaussian.parallelOutput_marginal_isProbabilityMeasure

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (i : Fin n) :

MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)))

Coordinate marginals of the correlated output law are probability measures.

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelOutput_marginal_eq_conv

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (i : Fin n) :

MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)) = (MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) p).conv (ProbabilityTheory.gaussianReal 0 (N i))

Parallel-output marginal as 1-D AWGN convolution. The i-th coordinate marginal of the correlated output law is the input marginal smoothed by the noise: μY.map (· i) = (p.map (· i)) ∗ gaussianReal 0 (N i).

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelOutput_marginal_eq_awgn_output

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (i : Fin n) :

MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)) = ChannelCoding.outputDistribution (MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) p) (AWGN.awgnChannel (N i) ⋯)

Parallel-output marginal as 1-D AWGN output law. The i-marginal of the correlated output equals the 1-D AWGN output law outputDistribution (p.map (· i)) (awgnChannel (N i)), letting the single-coordinate AWGN lemmas apply verbatim.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelMarginal_mem_awgnPowerConstraintSet

source

{n : ℕ} (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (P : ℝ) (hp : p ∈ parallelGaussianPowerConstraintSet P) (i : Fin n) :

MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) p ∈ AWGN.awgnPowerConstraintSet P

i-marginal inherits the 1-D AWGN power constraint. From the total constraint ∑ⱼ ∫⁻ (xⱼ)² ∂p ≤ P, the input marginal satisfies p.map (· i) ∈ awgnPowerConstraintSet P.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelOutput_absolutelyContinuous_volume

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) :

(ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)).AbsolutelyContinuous MeasureTheory.volume

Output law absolute continuity μY ≪ volume. The output is the fibre mixture μY s = ∫⁻ x, (W x) s ∂p, and each fibre is ≪ volume, so the mixture is too.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelOutput_marginal_absolutelyContinuous_volume

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) (i : Fin n) :

(MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas))).AbsolutelyContinuous MeasureTheory.volume

Each coordinate marginal is absolutely continuous: μY.map (· i) ≪ volume.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.volume_absolutelyContinuous_parallelOutput_marginal

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) (i : Fin n) :

MeasureTheory.volume.AbsolutelyContinuous (MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)))

Reverse full-support AC of each output coordinate marginal: volume ≪ μY.map (· i).

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.volume_absolutelyContinuous_parallelOutput

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) :

MeasureTheory.volume.AbsolutelyContinuous (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas))

Reverse full-support AC of the correlated output law: volume ≪ μY. From μY s = 0 the nonnegative x ↦ (W x) s vanishes p-a.e., so volume s = 0 by the reverse Gaussian-product AC volume ≪ W x.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelOutput_absolutelyContinuous_pi_marginals

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) :

(ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)).AbsolutelyContinuous (MeasureTheory.Measure.pi fun (i : Fin n) => MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)))

Joint vs. product-of-marginals absolute continuity for the output law: μY ≪ Measure.pi (fun i => μY.map (· i)), via μY ≪ volume ≪ Measure.pi (marginals).

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.parallelOutput_marginal_logDensity_integrable

source

{n : ℕ} (N : Fin n → NNReal) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (p : MeasureTheory.Measure (Fin n → ℝ)) [MeasureTheory.IsProbabilityMeasure p] (P : ℝ) (hP : 0 ≤ P) (i : Fin n) (hN : ↑(N i) ≠ 0) (hp : p ∈ parallelGaussianPowerConstraintSet P) :

MeasureTheory.Integrable (fun (z : Fin n → ℝ) => Real.log ((MeasureTheory.Measure.map (fun (z : Fin n → ℝ) => z i) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas))).rnDeriv MeasureTheory.volume (z i)).toReal) (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas))

Marginal log-density integrability over the joint output law. The integrand depends only on the i-th coordinate, so it pushes to the marginal μY.map (· i) (a 1-D AWGN output).

@audit:ok

Used by