Classical entropy power inequality for absolutely continuous, infinite-variance sums #

The classical entropy power inequality Nₑ(X + Y) ≥ Nₑ(X) + Nₑ(Y) for an independent sum of two absolutely continuous random variables with finite differential entropy, without assuming finite variance. It is obtained from the finite-variance entropy power inequality entropyPowerExt_add_ge_of_finite_variance by applying it to the conditioning truncation X_n := X | {|X| ≤ n ∧ |Y| ≤ n} and passing to the limit n → ∞.

Main statements #

• entropyPowerExt_add_ge_infinite_variance_truncation — the law-level inequality Nₑ(P.map (X + Y)) ≥ Nₑ(P.map X) + Nₑ(P.map Y) for the conditioning-truncation route.

Implementation notes #

For each n the conditioned measure P_n := P[· | {|X| ≤ n ∧ |Y| ≤ n}] (joint conditioning on both components) has compact support, hence finite second moments and finite differential entropy; it preserves absolute continuity (cond_absolutelyContinuous plus monotonicity of Measure.map under absolute continuity) and independence (conditioning on the rectangular event X⁻¹[-n, n] ∩ Y⁻¹[-n, n] preserves IndepFun X Y). So the finite-variance inequality applies at each n, giving Nₑ(P_n.map (X + Y)) ≥ Nₑ(P_n.map X) + Nₑ(P_n.map Y).

The final assembly is a limsup chain that does not depend on moments: the per-n inequality, the upper semicontinuity bound Nₑ(P.map (X + Y)) ≥ limsupₙ Nₑ(P_n.map (X + Y)) (Gibbs plus a cross-entropy dominated convergence argument), and the right-hand convergences Nₑ(P_n.map X) → Nₑ(P.map X), Nₑ(P_n.map Y) → Nₑ(P.map Y) compose into Nₑ(P.map (X + Y)) ≥ limsupₙ Nₑ(P_n.map (X + Y)) ≥ limₙ (Nₑ(P_n.map X) + Nₑ(P_n.map Y)).

Design choices:

• the truncation index is n : ℕ with truncation set {|X| ≤ n ∧ |Y| ≤ n}, monotone in n, so monotone / dominated convergence along the atTop filter is direct;
• the conditioning API is ProbabilityTheory.cond P s = (P s)⁻¹ • P.restrict s, whose absolute continuity is cond_absolutelyContinuous. A naive indicator truncation 1_{|X| ≤ n} · X would create an atom in the law and break absolute continuity, so conditioning is used instead;
• the black box works with the random-variable form P.map (fun ω => X ω + Y ω); convolution is implicit in P_n.map (X + Y) and Measure.conv is never expanded explicitly;
• independence is preserved because joint conditioning is on a rectangular event.