EPI G2 Gaussian max-entropy bound for the convolution density #

The file provides the Gaussian max-entropy upper bound negMulLog_convDensityAdd_gaussian_entropy_upper (@audit:ok): for the convolution density f_t = convDensityAdd pX g_t = pX ∗ g_{u n} (pX an L¹ input density with finite second moment, g_t a centered Gaussian), the entropy integral ∫ negMulLog f_t is bounded above by (1/2) log(2πe·V) for any V ≥ (∫ x² pX) + t. This bound is consumed by the layer-2 two-sided sandwich to discharge the IsBoundedUnder premise of tendsto_of_le_liminf_of_limsup_le (differentialEntropy_convDensity_integral_tendsto).

The name (Vitali/UI) reflects this file's origin as the home of the Vitali UnifIntegrable route to the same endpoint-continuity result; that route is superseded by the Fatou-LSC / conditioning sandwich above, and only the Gaussian max-entropy framing below survives.

Framing helpers (probability-measure framing of f_t) #

f_t := convDensityAdd pX g_t is measurable and nonnegative; the smoothed-density measure μ_t := volume.withDensity (ofReal ∘ f_t) is a probability measure with differentialEntropy μ_t = ∫ negMulLog f_t, and f_t has finite first and second moments — the mean/variance/integrability data consumed by differentialEntropy_le_gaussian_of_variance_le in the max-entropy bound.