Each AWGN fibre is absolutely continuous w.r.t. the (Gaussian) output law. gaussianReal x N ≪ volume ≪ gaussianReal 0 (P.toNNReal+N) = q, both full-support Gaussians. Used to discharge the joint absolute continuity p⊗ₘW ≪ p.prod q and the Bayes density split.

2-variable (joint) measurability of the ℝ≥0∞ Gaussian pdf. The closed-form Gaussian pdf is everywhere jointly measurable in (mean, point), whereas the measure-form rnDeriv fun z => (gaussianReal z.1 N).rnDeriv volume z.2 is not (it is only a.e.-determined). This brick supplies the everywhere joint measurability that the eq-set construction in llr_compProd_prod_split requires.

2-variable (joint) measurability of the ℝ-valued Gaussian pdf. Companion of measurable_gaussianPDF_uncurry; used to supply the joint AEStronglyMeasurable prerequisite when lifting the proxy log-density integrability to the compProd.

Second moment of a real Gaussian is integrable. (y − m)² is integrable against gaussianReal m' v' (any mean / variance), since id ∈ L²(gaussianReal) (memLp_id_gaussianReal). Needed to discharge the Gaussian log-density integrabilities (the log pdf is a constant plus a (y − m)² term).

Log Gaussian density is integrable against a Gaussian law. For v ≠ 0, fun y => Real.log (gaussianPDFReal m v y) is integrable against gaussianReal m' v'. The log pdf splits as c₀ + c₁·(y − m)², a constant plus a finite-second-moment term.

Log of the Gaussian rnDeriv (toReal) is integrable against the Gaussian law. For v ≠ 0, fun y => Real.log ((gaussianReal m v).rnDeriv volume y).toReal is integrable against gaussianReal m v. Bridges the literal Measure.rnDeriv form appearing in the hypotheses to gaussianPDFReal via the a.e. identity rnDeriv_gaussianReal, then integrable_log_gaussianPDFReal_gaussianReal.

Second moment about the mean of a real Gaussian (variance form). The mean of gaussianReal m N is m, so ∫ y, (y − m)² ∂(gaussianReal m N) = N by variance_fun_id_gaussianReal. Used to make the per-fibre L¹-norm integral of the joint log-density a constant in the input x, which discharges the third condition of Measure.integrable_compProd_iff.

Proxy-form joint integrability of the AWGN fibre log-density. The fibre log-density, in measurable-proxy form fun z => Real.log (gaussianPDF z.1 N z.2).toReal, is integrable against the joint p ⊗ₘ awgnChannel N. Built via Measure.integrable_compProd_iff: joint AEStronglyMeasurable from the brick measurable_gaussianPDFReal_uncurry, per-fibre integrability from integrable_log_gaussianPDFReal_gaussianReal, and per-fibre L¹-norm integrability via the constant-second-moment fact integral_sq_sub_self_gaussianReal (the log pdf is c₀ + c₁·(y−x)², whose norm-integral is bounded by |c₀| + |c₁|·N, constant in x).

AWGN instance of IsContChannelMIDecompHyp.

Applies the general body mutualInfoOfChannel_toReal_eq_diffEntropy_sub at the AWGN instance p := gaussianReal 0 P.toNNReal, W := awgnChannel N h_meas. From the inputs P, N, hN, hPN, h_meas, h_out alone, all of the following are supplied:

• the fibre / output absolute continuities hW_ac, hq_ac (Gaussian facts);
• the joint absolute continuity p⊗ₘW ≪ p.prod q (absolutelyContinuous_compProd_right_iff + fibre-vs-output ac);
• the Bayes density split h_llr_split — from the general llr_compProd_prod_split, which rests on the linchpin rnDeriv_compProd_fibre (the fibre form of the compProd rnDeriv);
• the fibre log-density integrability and the fibre joint measurability — via the measurable PDF proxy g := fun z => gaussianPDF z.1 N z.2.

Why the measurable PDF proxy. The measure-form parameterized rnDeriv fun z => (gaussianReal z.1 N).rnDeriv volume z.2 has no everywhere joint measurability (rnDeriv is a.e.-determined; rnDeriv_gaussianReal is =ᵐ[volume], not everywhere). Instead, the fibre density term is carried by the closed-form proxy g, which is everywhere jointly measurable (measurable_gaussianPDF_uncurry). The proxy↔rnDeriv bridge is the per-fibre a.e. agreement hg_ae x : (W x).rnDeriv vol =ᵐ[W x] g(x,·) (from rnDeriv_gaussianReal lifted via gaussianReal_absolutelyContinuous), consumed only inside integrals by llr_compProd_prod_split and integral_log_proxy_fibre — never via a joint a.e. MeasurableSet, which would be circular. The proxy-form joint integrability is integrable_log_proxy_fibre_compProd. The two output-side log-density integrabilities follow from the Gaussian density facts: h_int_out_joint (the integrand depends only on z.2, so it is g ∘ snd with (p ⊗ₘ W).snd = outputDistribution = q) reduces to h_int_out_marg, which is integrable_log_rnDeriv_gaussianReal at q = gaussianReal 0 (P + N).

IsAwgnMIDecomp wrapper.

Composes isContChannelMIDecompHyp_awgn with the combinator awgn_midecomp_of_cont_chain. The MI-decomp predicate IsAwgnMIDecomp follows from the inputs P, N, hN, hPN, h_meas, h_out alone — via the linchpin rnDeriv_compProd_fibre, the general llr_compProd_prod_split, and the measurable PDF proxy g := gaussianPDF (see isContChannelMIDecompHyp_awgn). The Bayes density split, the joint absolute continuity, both fibre/output absolute continuities, the fibre log-density integrability and the two output-side log-density integrabilities are all supplied. Everything else in the MI chain rule (KL→integral, Fubini split, both differential-entropy identifications, output marginal) comes from the general body.

Closed-form Gaussian MI from h_out.

Same as awgn_mi_gaussian_closed_form_of_primitives but with the h_decomp argument supplied internally: IsAwgnMIDecomp comes from isAwgnMIDecomp_of_densitySplit, leaving h_out as the only standing hypothesis.