InformationTheory.Shannon.ParallelGaussian.Converse.MixtureDensity

The joint mixture output density f_Y(z) := ∫⁻ x, ∏ᵢ gaussianPDF (x i) (N i) (z i) ∂p, the Fin n → ℝ analogue of the 1-D output mixture density.

Unfolded form of parallelOutputMixtureDensity.

@audit:ok

The joint mixture density is measurable in z.

@audit:ok

The correlated output μY equals volume.withDensity (parallelOutputMixtureDensity) (the noise fibre is a withDensity of the Gaussian-PDF product, with Tonelli moving the ∂p average outside).

@audit:ok

The output rnDeriv is a.e. equal to the joint mixture density.

@audit:ok

The joint mixture density is bounded above by ∏ᵢ (√(2π Nᵢ))⁻¹.

@audit:ok

Coordinate-box concentration. There is a box S = {x | ∀ i, |x i| ≤ Rᵢ} carrying ≥ 1/2 of the mass of p, via a per-coordinate Chebyshev bound and a union bound over Fin n.

@audit:ok

Quadratic -log upper bound on the mixture density: ∃ a b, 0 ≤ a ∧ ∀ z, -log (f_Y z).toReal ≤ a · ∑ᵢ (zᵢ)² + b. On the concentration box each coordinate Gaussian has a tail lower bound, giving f_Y(z) ≥ (1/2)·∏ᵢ Krᵢ(zᵢ), quadratic in each zᵢ.

@audit:ok

Quadratic bound on |log f_Y|: ∃ c₀ c₁, 0 ≤ c₁ ∧ ∀ z, |log (f_Y z).toReal| ≤ c₀ + c₁ ∑ᵢ (zᵢ)², combining the constant upper bound with the quadratic lower bound.

@audit:ok

Joint log-density integrability for the correlated output law: log ((μY.rnDeriv volume z).toReal) is integrable against μY.

@audit:ok

Fibre product-entropy identity. Each fibre is a coordinate product of Gaussians, so the conditional term is the constant ∑ᵢ (1/2)log(2πe Nᵢ).

@audit:ok

The output marginal mean mᵢ := ∫ y, y ∂(μY.map (· i)).

Marginal centered-second-moment (noise additivity). With m the marginal mean, ∫ (y − m)² ∂(μY.map (· i)) = (∫ (xᵢ − m)² ∂p) + Nᵢ, via the convolution identity for the marginal and the Gaussian fibre second moment.

@audit:ok

Output marginal mean equals input marginal mean: mᵢ = ∫ (xᵢ) ∂p (the noise mean is 0).

@audit:ok

Output marginal variance bound: Var(Yᵢ) ≤ E[Xᵢ²] + Nᵢ, from noise additivity Var(Yᵢ) = Var(Xᵢ) + Nᵢ and Var(Xᵢ) ≤ E[Xᵢ²].

@audit:ok

Output marginal variance lower bound: Var(Yᵢ) ≥ Nᵢ, since the independent noise of variance Nᵢ adds to the nonnegative input variance.

@audit:ok

Output marginal variance integrability. The centered square (yᵢ − mᵢ)² is integrable against the marginal.

@audit:ok

Output marginal entropy-integrand volume integrability (for differentialEntropy_le_gaussian_of_variance_le), via the 1-D AWGN output of the input marginal and its inherited power constraint.

@audit:ok

Fibre ≪ output: W x ≪ μY, via W x ≪ volume ≪ μY.

@audit:ok

Fibre rnDeriv as Gaussian-PDF-product proxy: (W x).rnDeriv volume =ᵐ[W x] fun y => ∏ᵢ gaussianPDF (x i) (N i) (y i).

@audit:ok

Fibre log-proxy integrability over the joint: log (∏ gaussianPDF) is integrable against p ⊗ₘ W. The log of the Gaussian-PDF product is the coordinate sum ∑ᵢ (cᵢ + c'ᵢ (yᵢ − xᵢ)²), each quadratic summand integrable.

@audit:ok

Channel↔RV MI decomposition value for the correlated input: I = jointDifferentialEntropyPi(μY) − ∫ jointDifferentialEntropyPi(W x) ∂p, a reduction to the decomposition lift parallel_mutualInfoOfChannel_toReal_eq_diffEntropyPi_sub with all preconditions supplied.

@audit:ok

Per-coordinate max-entropy converse split (correlated input), exposing the per-coordinate second-moment ellipsoid. For 0 ≤ P, every feasible input admits a split P' (with 0 ≤ P'ᵢ and P'ᵢ ≤ E[Xᵢ²] = ∫ (xᵢ)² ∂p) whose per-coordinate sum bounds the MI. Assembled from the MI decomposition, output-entropy subadditivity, per-coord Gaussian max-entropy, and the variance allocation P'ᵢ := Var(Yᵢ) − Nᵢ.

This strengthens parallel_per_input_mi_le_sum's ∑ P'ᵢ ≤ P to the per-coordinate ellipsoid P'ᵢ ≤ ∫ (xᵢ)² ∂p, which water-filling needs; the plain-sum version is the corollary parallel_per_input_mi_le_sum directly below. The 0 ≤ P precondition threads through the variance/integrability lemmas.

Plain-sum corollary of parallel_per_input_mi_le_sum_percoord: for 0 ≤ P, every feasible input admits a split P' (with 0 ≤ P'ᵢ, ∑ P'ᵢ ≤ P) whose per-coordinate sum bounds the MI. Follows from the per-coordinate ellipsoid P'ᵢ ≤ ∫ (xᵢ)² ∂p summed against the total power budget ∑ᵢ ∫ (xᵢ)² ∂p ≤ P.

The 0 ≤ P precondition is necessary: for P < 0 the constraint set is non-empty (it contains the Dirac at 0) yet ∑ P'ᵢ ≤ P < 0 with P'ᵢ ≥ 0 is unsatisfiable, so the statement would be false.

BddAbove (miImage P N …). Every MI value of a feasible input is bounded by the constant ∑ᵢ (1/2) log(1 + P/Nᵢ): the per-input split returns a feasible P' with P'ᵢ ≤ P coordinate-wise, and log monotonicity caps each term.