Gaussian pdf sup upper bound gaussianPDFReal m v y ≤ (√(2πv))⁻¹. The exponential factor rexp (-(y-m)²/(2v)) is ≤ 1 (nonpositive exponent), so the pdf is bounded above by its normalization constant.

For any SFinite input p, the AWGN output is the convolution with the noise law: outputDistribution p (awgnChannel N h_meas) = p ∗ gaussianReal 0 N. Via outputDistribution = (p⊗ₘW).snd = W ∘ₘ p (snd_compProd) and the in-tree translation-kernel ↔ convolution bridge bind_eq_conv_of_translation_kernel.

The capacity log-algebra step: (1/2)log(2πe(P+N)) − (1/2)log(2πeN) = (1/2)log(1+P/N).

Second moment of a shifted real Gaussian: ∫ z, (z − c)² ∂𝒩(0,N) = N + c².

(y − m)² is integrable against the mixture output law p ∗ 𝒩(0,N) (for any m), given that the input second moment is integrable.

hp_2mom_int : Integrable (fun x ↦ x²) p is a regularity precondition: the bare constraint ∫ x² ∂p ≤ P does not imply integrability (a non-integrable x² gives the degenerate ∫ x² ∂p = 0 ≤ P).

Second moment of the mixture output: ∫ y² ∂(p ∗ 𝒩(0,N)) = ∫ x² ∂p + N. Via integral_conv (the output is (p.prod 𝒩).map (·+·)) and the fiber identity ∫ z, (x + z)² ∂𝒩(0,N) = x² + N.

The mixture output law q = p ∗ 𝒩(0,N) has variance at most P + N: Var(Y) ≤ E[Y²] = E[X²] + N ≤ P + N. With m := ∫ y ∂q the true mean, ∫ (y − m)² ∂q = Var(Y) ≤ P + N.

hp_2mom_int is a regularity precondition (see output_sq_sub_integrable).

Each AWGN fiber is absolutely continuous w.r.t. the (mixture) output law: ∀ x, awgnChannel N h_meas x ≪ outputDistribution p (awgnChannel N h_meas). The output q = p ∗ 𝒩(0,N) is full-support since 𝒩(0,N) ≪ volume, so each 𝒩(x,N) ≪ q. The in-tree awgnChannel_apply_absolutelyContinuous_output is Gaussian-input-only and not reusable here.

Proxy-form joint integrability of the AWGN fiber log-density for an arbitrary probability-measure input p: fun z ↦ Real.log (gaussianPDF z.1 N z.2).toReal is integrable against the joint p ⊗ₘ awgnChannel N. The integrand decomposes everywhere as c₀ + c₁·(z.2 − z.1)², and the (z.2 − z.1)² term is integrable against the joint via Measure.integrable_compProd_iff (per-fiber integrability + constant L¹-norm N). The proof uses only that p is a probability measure, so it is the general-p counterpart of the Gaussian-input-only ContChannelMIDecomp.integrable_log_proxy_fibre_compProd.

The mixture output density f_q(y) := ∫⁻ x, gaussianPDF x N y ∂p (the value of the convolution density at y). The output law q = p ∗ 𝒩(0,N) equals volume.withDensity outputMixtureDensity.

The mixture density is jointly measurable in y.

Measurability of the Gaussian pdf in the mean parameter (fixed argument y): Measurable (fun x ↦ gaussianPDF x N y). Isolated as its own declaration because the (uncurry).comp term, if elaborated with an expected type pushed in, makes isDefEq unfold gaussianPDF/gaussianPDFReal and hit a heartbeat timeout; the have h := …; exact h shape elaborates comp freely and matches cheaply. Consumers call this lemma (term reuse).

The mixture output q = p ∗ 𝒩(0,N) is volume.withDensity (fun y ↦ ∫⁻ x, gaussianPDF x N y ∂p). Holds for any input p (possibly discrete) since the noise is absolutely continuous, via lintegral_conv (Tonelli) and the translation 𝒩(x,N) = volume.withDensity (gaussianPDF x N).

The Gaussian density is kept behind the opaque local g := fun z ↦ gaussianPDF z.1 N z.2 to stop isDefEq/whnf from unfolding gaussianReal/gaussianPDFReal during the Fubini swap (which otherwise hits a heartbeat timeout). @audit:ok

The output rnDeriv is a.e. the mixture density.

The mixture density is bounded above by (√(2πN))⁻¹: each Gaussian component is ≤ (√(2πN))⁻¹ (gaussianPDFReal_le_sup), and p is a probability measure, so the average inherits the bound.

The mixture density admits a Gaussian lower bound f_q(y) ≥ c·exp(−a·y²) with c, a > 0, equivalently a quadratic upper bound on −log f_q: there exist a, b : ℝ with −log (f_q y).toReal ≤ a · y² + b for all y. Chebyshev concentrates ≥ 1/2 of the mass of p on {|x| ≤ R} (from the finite second moment), and on that set gaussianPDF x N y has a Gaussian-tail lower bound quadratic in y. @audit:ok

Quadratic bound on |log f_q|: there exist c₀, c₁ : ℝ with |log (f_q y).toReal| ≤ c₀ + c₁ · y² for all y. Combines the constant upper bound outputMixtureDensity_le_sup with the quadratic lower bound output_logDensity_lower_bound.

The continuous mixture output q = p ∗ 𝒩(0,N) has integrable log-density: negMulLog ((q.rnDeriv vol ·).toReal) is volume-integrable. The output density is bounded above by (√(2πN))⁻¹ and −log f_q is bounded by a quadratic, so |negMulLog f_q(y)| = |f_q(y) · log f_q(y)| ≤ f_q(y)·(c₀ + c₁·y²), integrable against volume since ∫ f_q(y)·(c₀+c₁y²) dvol = ∫ (c₀+c₁y²) dq < ∞ (finite second moment of q).

The input p is constrained by membership in awgnPowerConstraintSet P (lintegral second moment ≤ P), which carries the genuine integrability of x² via awgnPowerConstraintSet_mem_iff_integrable. This rules out the heavy-tailed inputs (Cauchy etc.) that would break the statement. @audit:ok

Joint form of outputDistribution_logDensity_integrable: log ((q.rnDeriv vol ·).toReal) ∘ snd is integrable against the joint p ⊗ₘ W. Lift along the snd-marginal: q = (p ⊗ₘ W).map Prod.snd, and |log f_q| ≤ c₀ + c₁·y² is integrable against q (finite second moment), so the snd-pullback is integrable against p ⊗ₘ W, via integrable_map_measure and outputMixtureDensity_log_abs_le. @audit:ok

Final converse conclusion (supplies the h_max_ent of awgnCapacity_eq). For any input law p ∈ awgnPowerConstraintSet P (lintegral second moment ≤ P), (mutualInfoOfChannel p (awgnChannel N)).toReal ≤ (1/2) log(1 + P/N).

Assembled from the chain rule (mutualInfoOfChannel_toReal_eq_diffEntropy_sub), the fiber entropy constant, the Gaussian max-entropy bound (differentialEntropy_le_gaussian_of_variance_le), Var(Y) ≤ P + N, and the capacity log-algebra.

The constraint is membership in awgnPowerConstraintSet P (lintegral form), which carries the genuine integrability of x² (awgnPowerConstraintSet_mem_iff_integrable), ruling out the heavy-tailed inputs (Cauchy etc.) that make a Bochner-only signature false. The output log-density integrability hypotheses (h_int_out / h_ent_int) are supplied by outputDistribution_logDensity_integrable[_joint]. @audit:ok

AWGN capacity closed form (Cover-Thomas).

awgnCapacity P N = (1/2) log(1 + P/N). This supersedes awgnCapacity_eq (AWGN/Basic.lean): there the converse max-entropy bound h_max_ent was an explicit hypothesis; here it is discharged by awgn_per_input_mi_le_log. The achievability bridge (awgn_mi_gaussian_closed_form_of_out), the MI decomposition (isAwgnMIDecomp_of_densitySplit) and the bind/conv output-Gaussian fact are all wired upstream. @audit:ok