InformationTheory.Shannon.ParallelGaussian.Converse.Core

Imports 9

Product-measure absolute continuity #

theorem

InformationTheory.Shannon.ParallelGaussian.pi_absolutelyContinuous

{n : ℕ} (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (h : ∀ (i : Fin n), (μ i).AbsolutelyContinuous MeasureTheory.volume) :

(MeasureTheory.Measure.pi μ).AbsolutelyContinuous MeasureTheory.volume

Measure.pi preserves absolute continuity w.r.t. volume. If every factor μ i ≪ volume (each a probability measure), then Measure.pi μ ≪ volume.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.pi_absolutelyContinuous_reverse

source

{n : ℕ} (ν : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (ν i)] (h_ac : ∀ (i : Fin n), (ν i).AbsolutelyContinuous MeasureTheory.volume) (h_rev : ∀ (i : Fin n), MeasureTheory.volume.AbsolutelyContinuous (ν i)) :

MeasureTheory.volume.AbsolutelyContinuous (MeasureTheory.Measure.pi ν)

Reverse Measure.pi absolute continuity from componentwise mutual AC. If every factor is mutually absolutely continuous with volume (ν i ≪ volume and volume ≪ ν i), then volume ≪ Measure.pi ν.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.volume_absolutelyContinuous_pi_gaussian

source

{n : ℕ} (x : Fin n → ℝ) (N : Fin n → NNReal) (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) :

MeasureTheory.volume.AbsolutelyContinuous (MeasureTheory.Measure.pi fun (i : Fin n) => ProbabilityTheory.gaussianReal (x i) (N i))

Reverse full-support AC for a Gaussian product fibre. volume ≪ Measure.pi (gaussianReal (x i) (N i)) whenever every N i ≠ 0, since the product of everywhere-positive Gaussian densities gives the reverse AC.

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.jointDifferentialEntropyPi_pi_eq_sum

source

{n : ℕ} (μ : Fin n → MeasureTheory.Measure ℝ) [∀ (i : Fin n), MeasureTheory.IsProbabilityMeasure (μ i)] (h_ac : ∀ (i : Fin n), (μ i).AbsolutelyContinuous MeasureTheory.volume) (h_int : ∀ (i : Fin n), MeasureTheory.Integrable (fun (y : ℝ) => Real.log ((μ i).rnDeriv MeasureTheory.volume y).toReal) (μ i)) :

jointDifferentialEntropyPi (MeasureTheory.Measure.pi μ) = ∑ i : Fin n, differentialEntropy (μ i)

Product → sum differential entropy identity. For a product of probability measures μ i ≪ volume on ℝ, the joint differential entropy of Measure.pi μ is the coordinate sum of the 1-D entropies, jointDifferentialEntropyPi (Measure.pi μ) = ∑ i, differentialEntropy (μ i). The per-component log-density integrability h_int is a regularity precondition (satisfied by Gaussians).

@audit:ok

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.gaussianReal_logRnDeriv_integrable

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. For v ≠ 0, log ((gaussianReal m v).rnDeriv volume y).toReal is integrable against gaussianReal m v; it is the affine-in-(y-m)² function -(1/2)log(2πv) - (y-m)²/(2v).

@audit:ok

Used by

Channel↔RV MI decomposition, generic lift #

The single-coordinate decomposition is hardwired to Measure ℝ / differentialEntropy. The same chain is re-derived over a generic measurable space β with a SigmaFinite reference measure vol, producing the entropy in raw ∫ log(rnDeriv) ∂ form, then specialized to β = Fin n → ℝ, vol = volume.

theorem

InformationTheory.Shannon.ParallelGaussian.parallel_mutualInfoOfChannel_toReal_eq_diffEntropyPi_sub

source

(ChannelCoding.mutualInfoOfChannel p (parallelGaussianChannel N h_meas h_parallel_meas)).toReal = jointDifferentialEntropyPi (ChannelCoding.outputDistribution p (parallelGaussianChannel N h_meas h_parallel_meas)) - ∫ (x : Fin n → ℝ), jointDifferentialEntropyPi ((parallelGaussianChannel N h_meas h_parallel_meas) x) ∂p

Channel↔RV MI decomposition, Fin n → ℝ lift. Specializes the generic chain rule to β = Fin n → ℝ, vol = volume, producing the entropy in jointDifferentialEntropyPi form. The absolute-continuity / log-density-integrability hypotheses are regularity preconditions.

@audit:ok

Used by

Correlated-output regularity preconditions #

The decomposition and the subadditivity step both consume regularity preconditions of the correlated output law μY := outputDistribution p (parallelGaussianChannel N …): absolute continuity of the joint and of every coordinate marginal w.r.t. Lebesgue measure, the joint-vs-product absolute continuity, and the log-density integrabilities. These follow from Gaussian smoothing (each fibre is a full-support product, so the output is volume-equivalent), supplied here for an arbitrary correlated input as named lemmas.

theorem

InformationTheory.Shannon.ParallelGaussian.parallelChannel_fibre_absolutelyContinuous_volume

source

{n : ℕ} (N : Fin n → NNReal) (hN : ∀ (i : Fin n), ↑(N i) ≠ 0) (h_meas : IsParallelAwgnChannelMeasurable N) (h_parallel_meas : IsParallelGaussianKernelMeasurable N) (x : Fin n → ℝ) :

((parallelGaussianChannel N h_meas h_parallel_meas) x).AbsolutelyContinuous MeasureTheory.volume

Each fibre is absolutely continuous w.r.t. volume. Each component gaussianReal (x i) (N i) ≪ volume, so the product fibre is ≪ volume.

@audit:ok

Used by

noncomputable def

InformationTheory.Shannon.ParallelGaussian.piGaussProxy

source

{n : ℕ} (N : Fin n → NNReal) (z : (Fin n → ℝ) × (Fin n → ℝ)) :

ENNReal

Gaussian-PDF-product proxy density z ↦ ∏ᵢ gaussianPDF (z.1 i) (N i) (z.2 i) for the Fin n → ℝ fibre, named so the decomposition lift receives a single atomic g argument rather than a ∏ gaussianPDF lambda that the unifier repeatedly expands.

@audit:ok

Equations

InformationTheory.Shannon.ParallelGaussian.piGaussProxy N z = ∏ i : Fin n, ProbabilityTheory.gaussianPDF (z.1 i) (N i) (z.2 i)

Instances For

Used by

theorem

InformationTheory.Shannon.ParallelGaussian.piGaussProxy_measurable

source

{n : ℕ} (N : Fin n → NNReal) :

Measurable (piGaussProxy N)

Used by