Classical entropy power inequality for infinite-variance sums — capstone #

The named theorem entropyPowerExt_add_ge_infinite_variance (the same signature as the original finite-variance wall, with an explicit h_infvar infinite-variance hypothesis) is proved here using the conditioning-truncation route headline entropyPowerExt_add_ge_infinite_variance_truncation.

Implementation notes #

The theorem splits on whether the differential entropy of the sum is finite (hent_sum):

• if it is finite, the truncation-route headline applies directly (h_infvar is unused);
• otherwise the sum density r := (P.map (X + Y)).rnDeriv volume |>.toReal has non-integrable negMulLog. Its negative part B := ∫⁻ ofReal (-(negMulLog r)) is finite by the probability-measure negative-part lemma, while Integrable g volume ↔ A < ⊤ ∧ B < ⊤ (with A := ∫⁻ ofReal (negMulLog r)) forces A = ⊤, so differentialEntropyExt ν = (A : EReal) - (B : EReal) = ⊤, hence entropyPowerExt ν = ⊤ and the inequality holds by le_top.

The h_infvar hypothesis is kept only for signature compatibility; it is not load-bearing (unused in the finite case, and a weakening hypothesis). hX_ent / hY_ent are per-component finite-differential-entropy regularity preconditions. To avoid an import cycle, this file is placed downstream of the truncation route and imports only that route.