InformationTheory.Shannon.EPI.InfiniteVariance.Truncation.Construction

The truncation set truncSet X Y n := {ω | |X ω| ≤ n ∧ |Y ω| ≤ n}, a rectangular event truncating both components simultaneously. It is monotone increasing in n : ℕ and exhausts the whole space.

The conditioning measure condTrunc P X Y n := P[· | truncSet X Y n]. For large n the mass P (truncSet X Y n) is positive, so this is a probability measure.

Independence is preserved by joint conditioning: IndepFun X Y P implies IndepFun X Y (condTrunc P X Y n), since the conditioning event X⁻¹[-n, n] ∩ Y⁻¹[-n, n] is rectangular.

Absolute continuity is preserved by conditioning truncation: (P.map X) ≪ volume implies ((condTrunc P X Y n).map X) ≪ volume, composing cond_absolutelyContinuous with monotonicity of Measure.map.

Pushing the jointly-conditioned measure condTrunc P X Y n forward along a component Z (Z = X or Z = Y) reduces to single-component conditioning: (condTrunc P X Y n).map Z = cond (P.map Z) {r | |r| ≤ n}. The partner mass P (Y⁻¹ Sn) from the independence factoring P (truncSet) = P (X⁻¹ Sn) · P (Y⁻¹ Sn) cancels. @audit:ok

The Radon–Nikodym derivative of a measure conditioned on a positive-mass set s is the indicator-restricted density scaled by the normalizing constant: (cond μ s).rnDeriv volume =ᵐ (μ s)⁻¹ · 1_s · μ.rnDeriv volume. @audit:ok

Per-n finite second moment Integrable ((Z ·)²) (condTrunc P X Y n). Since condTrunc is supported on truncSet, the component Z = X or Z = Y is bounded by n, so its second moment is bounded.

Per-n finite differential entropy of a component: Integrable (negMulLog (rnDeriv ·)) volume for (condTrunc P X Y n).map Z. The entropy integrability of the conditioned marginal condTrunc.map Z = cond (P.map Z) Sn is derived from that of P.map Z (the precondition hZ_ent) via the conditional density formula. This re-supplies the hX_ent / hY_ent arguments of the finite-variance black box. @audit:ok

The absolutely continuous measure (condTrunc P X Y n).map Z is recovered as volume.withDensity (ofReal ∘ r) from the real density r := (rnDeriv ·).toReal, via withDensity_rnDeriv_eq together with ofReal ∘ toReal = id on the a.e.-finite rnDeriv. @audit:ok

The conditioned sum density is the convolution of the conditioned marginal densities: the rnDeriv of the law of X + Y under condTrunc P X Y n equals convDensityAdd p_n q_n a.e., where p_n := (condTrunc.map X).rnDeriv volume |>.toReal and q_n := (condTrunc.map Y).rnDeriv volume |>.toReal. Obtained by applying indepSum_density_ae with condTrunc P X Y n in place of P (independence from indepFun_condTrunc, absolute continuity from map_condTrunc_absolutelyContinuous). @audit:ok

Compact support of the sum law: since condTrunc P X Y n is concentrated on truncSet (both components bounded by n), the push-forward law of X + Y is concentrated on Icc (-(2n)) (2n), i.e. (condTrunc.map (X + Y)) (Icc (-(2n)) (2n))ᶜ = 0. @audit:ok

The negative part (negMulLog r)⁻ = max (-(negMulLog r)) 0 of negMulLog of the conditioned sum density r := (condTrunc.map (X + Y)).rnDeriv volume |>.toReal (the convolution p_n ∗ q_n) is volume-integrable. This is the genuine core of the per-n finite-entropy lemma (the positive part is immediate from compact support and negMulLog_le_one_sub_self).

Since p_n · volume is a probability measure and t ↦ t log t is convex, the integral form of Jensen's inequality gives (r z · log r z)⁺ ≤ ∫ x, p_n x · (q_n (z - x) · log q_n (z - x))⁺ dx, and Tonelli with translation invariance bounds ∫⁻ z (r log r)⁺ by 1 · C < ∞, where C = ∫ (q_n log q_n)⁺ < ∞ is the negative part of the integrable negMulLog q_n.

The hypothesis hY_ent is essential: a convolution of two singular densities can be unbounded, so finiteness of the negative part requires entropy-type control rather than absolute continuity and independence alone (the proof uses only hY_ent). @audit:ok

Per-n finite differential entropy of the sum: the density r := (condTrunc.map (X + Y)).rnDeriv volume |>.toReal (the convolution p_n ∗ q_n, supported on [-2n, 2n]) has integrable negMulLog, via a positive/negative-part split. The positive part is bounded using negMulLog_le_one_sub_self and integrability of r; the negative part is the preceding lemma. This re-supplies the hent_sum argument of the finite-variance black box. @audit:ok

Per-n finite-variance entropy power inequality: supplying all regularity to the black box entropyPowerExt_add_ge_of_finite_variance gives, for each positive-mass n, Nₑ(P_n.map (X + Y)) ≥ Nₑ(P_n.map X) + Nₑ(P_n.map Y). @audit:ok

Generalized Gibbs (cross-entropy lower bound): for probability measures with μ ≪ ν and μ ≪ volume, differentialEntropy μ ≤ -∫ x, log (ν.rnDeriv volume x).toReal ∂μ. It follows from (klDiv μ ν).toReal ≥ 0 and the log-likelihood-ratio decomposition toReal_klDiv_of_measure_eq. This generalizes the Gaussian-reference template differentialEntropy_le_gaussian_of_variance_le to an arbitrary reference ν. @audit:ok