The MI image whose sSup defines parallelGaussianCapacity.

The independent-Gaussian product input with per-coordinate power Q i.

The achiever's per-coordinate second moment: ∫ xᵢ² ∂(gaussianProductInput Q) = Q i.

Achiever feasibility: if ∑ᵢ Q i ≤ P then the product Gaussian input lies in parallelGaussianPowerConstraintSet P.

@audit:ok

The analytic regularity bundle the sup-sandwich consumes, parameterized by the achiever power split Q, mirroring the single-coordinate AWGN.awgnCapacity_eq residuals.

Lower bound (achiever). The independent Gaussian product input is feasible and achieves the per-coordinate sum, so the capacity is at least that sum.

Upper bound (max-entropy and water-filling). Every constrained input has MI bounded by the water-filling sum.

max_ent from subadditivity. With the channel MI written as h(Yⁿ) - condTerm (h_decomp), output-entropy subadditivity h(Yⁿ) ≤ ∑ h(Yᵢ) and the per-coordinate water-filling allocation bound h_perCoord give I ≤ ∑ᵢ (1/2) log(1 + P'ᵢ/Nᵢ).

At a KKT water level ν (h_kkt) the capacity equals the per-coordinate water-filling sum, i.e. IsParallelGaussianPerCoordReduction P N h_meas h_parallel_meas ν holds. The analytic regularity hypotheses are bundled in IsParallelGaussianPerCoordRegularity.

Parallel Gaussian channel capacity (water-filling). For parallel AWGN channels Y_i = X_i + Z_i, Z_i ∼ 𝒩(0, N_i) (i : Fin (n+1)) under the total power constraint ∑_i E[X_i²] ≤ P, the information capacity equals the water-filling sum

C = ∑_i (1/2) log(1 + max(0, ν - N_i) / N_i)

at the KKT water level ν. The hypotheses are the KKT budget condition h_kkt and the analytic regularity bundle h_reg; water-filling optimality is obtained internally from h_kkt rather than assumed.

The ℝ≥0∞ analogue of n-variate Fubini: for a product measure Measure.pi μ over Fin n, the integral of a product of single-coordinate functions equals the product of the per-coordinate integrals (the ℝ≥0∞ form of MeasureTheory.integral_fin_nat_prod_eq_prod).

@audit:ok

compProd-of-Measure.pi factorization. The channel joint gaussianProductInput Q ⊗ₘ parallelGaussianChannel N factors as the Measure.pi of the per-coordinate joints gaussianReal 0 (Qᵢ) ⊗ₘ awgnChannel Nᵢ, reshaped by arrowProdEquivProdArrow.

@audit:ok

Per-channel MI decomposition of the product achiever. The channel mutual information of the independent-Gaussian product input through the parallel Gaussian channel equals the sum of the per-coordinate single-channel mutual informations.

@audit:ok

AWGN single-channel mutual information is finite. The channel MI of the Gaussian input through a single AWGN channel is a finite ENNReal (≠ ⊤).

The N ≠ 0 hypothesis is required: for N = 0 the channel is deterministic (W x = dirac x), the joint lives on the diagonal graph (p.prod q-null for a continuous input P ≠ 0), and klDiv = ⊤ — the claim is false there.

Per-channel MI decomposition of the product achiever, in .toReal form. The per-coordinate finiteness needed for the .toReal/∑ exchange requires N i ≠ 0.

Per-coordinate AWGN MI closed form (all variances). For a single AWGN sub-channel, the Gaussian-input mutual information equals (1/2)·log(1 + Q/N), with no positivity hypothesis on the input variance Q. The Q = 0 branch (deterministic input gaussianReal 0 0 = dirac 0) gives MI = 0 = (1/2)·log 1 via klDiv_self.

The achiever MI value equals the per-coordinate water-filling sum. Inhabits the achiever_mi field of IsParallelGaussianPerCoordRegularity.

Deprecated alias for parallel_gaussian_capacity_formula.