InformationTheory.Shannon.EPI.InfiniteVariance.Truncation.Density

The sum density is the convolution of the marginal densities: (P.map (X + Y)).rnDeriv =ᵐ ofReal (convDensityAdd pX pY), where pX := (P.map X).rnDeriv volume |>.toReal and pY := (P.map Y).rnDeriv volume |>.toReal. This is the conditioning-free version of rnDeriv_map_condTrunc_sum_ae. @audit:ok

Positivity of the marginal mass: P (truncSet X Y n) ≠ 0 implies (P.map Z) {r | |r| ≤ n} ≠ 0 for Z = X or Z = Y, since independence factors P (truncSet) = P (X⁻¹ Sn) · P (Y⁻¹ Sn) and one factor equals (P.map Z) Sn. @audit:ok

Single-component dominating bound for the conditioned marginal density: for a fixed positive-mass n₀ and any n ≥ n₀, the conditioned density p_n := (condTrunc.map Z).rnDeriv volume |>.toReal is bounded by C_Z · pZ, where pZ := (P.map Z).rnDeriv volume |>.toReal and C_Z := ((P.map Z) {|r| ≤ n₀})⁻¹.toReal. Reducing to single-component conditioning gives p_n =ᵐ (m_n)⁻¹ · 1_Sn · pZ, and m_n⁻¹ ≤ m_{n₀}⁻¹ = C_Z by monotonicity. @audit:ok

Dominating bound p_n ∗ q_n ≤ C · (pX ∗ pY) (a.e. z, with C = C_X · C_Y): for a fixed positive-mass n₀ and all n ≥ n₀, each conditioned marginal density is bounded by a constant multiple of the corresponding P-marginal (condTrunc_marginal_density_le), and monotonicity of the convolution lifts this to the sum density. Per-z integrability of the convolution slice is supplied by integrable_prod_iff' plus Integrable.prod_right_ae, and the Y-bound is transported through the measure-preserving map x ↦ z - x. @audit:ok

Fixed-n version of the dominating bound: for a single positive-mass n, convDensityAdd pnX pnY ≤ C · convDensityAdd pX pY (a.e. z). Same argument as convDensity_condTrunc_le_const_mul specialized at n₀ := n, supplied directly without the atTop eventually wrapper so that callers requiring the bound at a fixed n avoid threshold dependence. @audit:ok

Pointwise convergence of the sum density under conditioning truncation: p_n ∗ q_n → pX ∗ pY (a.e. z). Each conditioned marginal converges a.e. (p_n → pX, q_n → qY), and the filter-form dominated convergence theorem with the dominating function C² · pX(x) · pY(z - x) gives p_n ∗ q_n (z) → pX ∗ pY (z) for a.e. z. @audit:ok

The cross-entropy sequence RHS_n := -∫ log (density of ν) ∂μ_n, where μ_n := (condTrunc P X Y n).map (X + Y) and ν := P.map (X + Y). It links the Gibbs upper bound and the dominated-convergence limit in the upper semicontinuity argument. @audit:ok

Per-n integrability of the cross-entropy integrand: log (density of ν) is integrable against μ_n, where ν := P.map (X + Y) and μ_n := (condTrunc P X Y n).map (X + Y). Pulling the integral back to volume and using the dominating bound p_n ∗ q_n ≤ C (pX ∗ pY) together with hent_sum bounds the integrand by C · |negMulLog ((ν.rnDeriv).toReal)|, which is integrable. This supplies the h_cross_int premise of the Gibbs bound. @audit:ok

Per-n Gibbs upper bound: ∀ᶠ n, h(μ_n) ≤ RHS_n, where RHS_n = crossEntropySeq P X Y n. The generalized Gibbs inequality differentialEntropy_le_cross_entropy is applied with μ = μ_n, ν = P.map (X + Y), supplying the per-n regularity facts (μ_n absolutely continuous, μ_n ≪ ν, finite entropy, and the cross-entropy integrability). @audit:ok

Convergence of the cross-entropy sequence: RHS_n → h(ν) with ν = P.map (X + Y). Pulling RHS_n back to volume as ∫ (-log (density of ν)) · (p_n ∗ q_n) dvolume, the pointwise convergence p_n ∗ q_n → pX ∗ pY together with the dominating function |log (density of ν)| · C² (pX ∗ pY) (integrable from hent_sum) gives, via dominated convergence, the limit -∫ (pX ∗ pY) log (pX ∗ pY) = h(ν). @audit:ok