Tensorization of withDensity through Measure.pi (G-2, absent from Mathlib): the finite product of per-coordinate weighted measures (μ i).withDensity (f i) equals the product measure Measure.pi μ weighted by the coordinatewise product density x ↦ ∏ i, f i (x i). Proved via Measure.pi_eq (agreement on measurable boxes) + the box factorization lintegral_pi_prod_eq_prod.

Per-letter change-of-measure facts for the AWGN joint J₁ = law(X, X+Z) / product Q₁ = μX ⊗ μY (nondegenerate P', N ≠ 0): the mutual absolute continuity J₁ ≪ Q₁, Q₁ ≪ J₁, and the pointwise density relation (Q₁.rnDeriv J₁ p).toReal = exp(−φ p) a.e. [J₁] (where φ = log dJ₁/dQ₁). The f_X factor in the density ratio cancels, so the ratio is a ratio of two strictly-positive-and- finite Gaussian densities, giving the exponential relation; mutual AC follows from the everywhere-positive-and-finite densities w.r.t. volume.prod volume.

Degenerate per-letter KL vanishes (P' = 0 ∨ N = 0): in either degenerate case the per-letter KL (klDiv J₁ Q₁).toReal = 0. When P' = 0 the input collapses to Dirac 0, the shear is the identity on {0} × ℝ, so J₁ = Q₁ (klDiv_self). When N = 0 (with P' ≠ 0) the joint J₁ concentrates on the diagonal {(x, x)}, which is Q₁-null (positive-variance Gaussian product, atomless), so ¬ J₁ ≪ Q₁ ⇒ klDiv = ⊤ ⇒ toReal = 0.

bridge ① per-letter closed form (genuine, sorryAx-free): per-letter joint J₁ = law(X, X+Z) and product of marginals Q₁ = μX ⊗ μY have KL equal to the AWGN per-letter capacity (1/2) log(1 + P/N) (nondegenerate P > 0, N ≠ 0). Routed through the conditional-KL integral (klDiv_compProd_const_toReal_integral) + the 1-D Gaussian KL closed form (klDiv_gaussianReal_gaussianReal_eq), integrating the per-fibre quadratic against the mean-0 variance-P' input — deliberately avoiding mutualInfoOfChannel / MIClosedForm (import cycle KLCapacityAndAEP → MIClosedForm → ContChannelMIDecomp → KLCapacityAndAEP).

The signature carries the genuine preconditions 0 < P / (N:ℝ) ≠ 0 (the union-bound consumer derives both before invoking); no circularity / bundling / degenerate-def.

@audit:ok

bridge ① n-fold identity (genuine, sorryAx-free): klDiv(J_n, Q_n).toReal = n · klDiv(J₁, Q₁).toReal, where J_n/Q_n are the verbatim n-letter joint/product measures from the continuousAepGaussian_holds signature. Via arrowProdEquivProdArrow reshape (klDiv_map_measurableEquiv) + klDiv_pi_eq_sum

• i.i.d. Finset.sum_const.

Unconditional measure identity (no P/N precondition — holds even in the degenerate cases, both sides equal); no circularity / bundling / degenerate-def.

@audit:ok

Continuous AEP for the n-dimensional Gaussian.

Given P : ℝ, N : ℝ≥0, a typicality slack δ > 0, and an error tolerance ε > 0 (independent parameters), there exists a threshold N₀ such that for every n ≥ N₀ there is a measurable typical set A ⊆ (Fin n → ℝ) × (Fin n → ℝ) satisfying:

• (i) joint codebook+noise mass ≥ 1 - ε, under the joint law of (X, Y) with X ∼ N(0,P) i.i.d. and Y = X + Z, Z ∼ N(0,N) i.i.d.;
• (ii) independent-pair upper bound (X' independent of Y): under the product of marginals, A has mass ≤ exp(−(klDivₙ − n·3δ)) = exp(−n(I − 3δ)), where klDivₙ = klDiv(joint, product) = n·I is the n-letter KL (per-letter MI I).

The slack δ controls the typical set's width; the error target ε controls the mass-failure level of (i). Decoupling them lets the consumer pick R + 3δ < I independently of ε, which makes the union bound's second term decay.

Implementation:

• (i) uses only the finite-n Chebyshev weak law (pi_empirical_mean_concentration / pi_empirical_mean_typical_mass). The typical set A is built from the per-letter joint info-density φ(x,y) = log dJ₁/dQ₁.
• (ii) is discharged by the tensorize pi_withDensity (built on the lintegral box-Fubini lintegral_pi_prod_eq_prod): with Q₁ ≪ J₁, pi Q₁ = (pi J₁).withDensity (∏ᵢ Q₁.rnDeriv J₁ (wᵢ)), and on B the product density (∏ᵢ Q₁.rnDeriv J₁ (wᵢ)).toReal = exp(−∑φ) ≤ exp(−n(I − δ)) (awgn_perLetter_changeOfMeasure_facts, J₁[φ] = (klDiv J₁ Q₁).toReal via toReal_klDiv_of_measure_eq); klDivₙ = n·I is klDiv_nFold_eq_nsmul.
• The degenerate case (klDiv Jn Qn).toReal = 0 for P.toNNReal = 0 ∨ N = 0 is handled via klDiv_nFold_eq_nsmul + awgn_perLetter_klDiv_degenerate: P'=0 gives J₁ = Q₁ (shear identity on {0}×ℝ, klDiv_self); N=0 ∧ P'≠0 puts J₁ on the diagonal {(x,x)} (Q₁-null since μX is atomless), so ¬J₁≪Q₁ and klDiv = ⊤, toReal = 0. The exponent n·3δ ≥ 0 makes the bound exp(n·3δ) ≥ 1 ≥ Qn univ. The degenerate A := Set.univ branch is an honest witness: bound (ii) is genuinely loose (RHS ≥ 1) when klDiv = 0, which is machine-proved rather than asserted. @audit:ok