Single-variable truncation: truncW P W n conditions P on the event {ω | |W ω| ≤ n}, i.e. on W taking values in [-n, n]. Each truncW P W n has compact support (hence finite variance and finite entropy) and preserves absolute continuity.

@audit:ok

Radon–Nikodym derivative of a conditioned measure: for a probability measure μ and a measurable set s of positive mass, (cond μ s).rnDeriv volume =ᵐ (μ s)⁻¹ · 1_s · μ.rnDeriv volume.

@audit:ok

At the measure level the truncated sum law is dominated by the full sum law: pushing the truncated measure truncW P W n = P[| {|W| ≤ n}] forward through W + V is bounded above by the inverse-mass scaled pushforward of P through W + V. Pure measure monotonicity (no convolution / density): cond P E = (P E)⁻¹ • P.restrict E ≤ (P E)⁻¹ • P via restrict_le_self, then push forward (Measure.map_smul + Measure.map_mono). Used downstream for the klDiv expansion of the truncated sum law. (hn is a regularity precondition kept for API symmetry; the ≤ direction does not use it, since cond P E = 0 ≤ anything when P E = 0.) @audit:ok

A corollary of the truncated-sum-law domination: the truncated sum law truncW P W n pushed through W + V is absolutely continuous w.r.t. the full sum law P.map (W + V). Immediate from map_truncW_add_le_smul_map_add via absolutelyContinuous_of_le_smul (μ' ≤ c • μ → μ' ≪ μ, unconditional in c). Used downstream for the klDiv expansion of the truncated truncW sum law. @audit:ok

Positive part of the cross-entropy (ℝ≥0∞): ∫⁻ x, ofReal (-log ((ν.rnDeriv volume x).toReal)) ∂μ, integrating the negative values of the log-density of ν against μ.

Negative part of the cross-entropy (ℝ≥0∞): ∫⁻ x, ofReal (log ((ν.rnDeriv volume x).toReal)) ∂μ, integrating the positive values of the log-density of ν against μ.

Self-identity (positive part): the cross-entropy positive part of ν against itself equals the positive part A(ν) = ∫⁻ x, ofReal (negMulLog ((ν.rnDeriv volume x).toReal)) ∂volume of the a.c. branch of differentialEntropyExt. Obtained by change of measure (lintegral_rnDeriv_mul).

@audit:ok

Self-identity (negative part): the cross-entropy negative part of ν against itself equals the negative part B(ν) = ∫⁻ x, ofReal (-(negMulLog ((ν.rnDeriv volume x).toReal))) ∂volume of the a.c. branch of differentialEntropyExt. The sign-flipped analogue of crossPos_self.

@audit:ok

Rearranged ℝ≥0∞ Gibbs inequality (consumer form): for μ ≪ ν ≪ volume (both probability measures) with B(μ) and crossNeg μ ν finite, A(μ) + crossNeg μ ν ≤ crossPos μ ν + B(μ), where A(μ) = ∫⁻ ofReal(negMulLog fμ) ∂vol and B(μ) = ∫⁻ ofReal(-(negMulLog fμ)) ∂vol. This version allows A(μ) = ⊤ (i.e. h(μ) = +∞): the proof splits on A(μ), delegating the finite branch to ennreal_gibbs_rearranged_of_finite_ent and closing the ⊤ branch via the universal bound ∫⁻ ofReal(-log r) ∂μ ≤ 1 (the content of klFun ≥ 0), which forces crossPos μ ν = ⊤.

@audit:ok

Translation invariance of per-fibre entropy integrability: if negMulLog (rnDeriv ν volume) is integrable for ν ≪ volume, then so is the corresponding integrand for the translate ν.map (· + y), by Lebesgue translation invariance.

@audit:ok

Convolution density as a translate-average (only the LEFT factor a.c.): for μW ≪ volume the sum law μW ∗ μV is volume.withDensity (z ↦ ∫⁻ v, f_W (z - v) ∂μV) where f_W = μW.rnDeriv vol. Unlike the route-T convDensityAdd machinery (EPIConvDensity, which requires both components a.c.), this only needs μW a.c.; μV is a general (probability) measure. lintegral_conv (Tonelli)

• withDensity_rnDeriv_eq (recover μW = vol.withDensity f_W) + translation invariance. @audit:ok

A translate of an a.c. measure expressed as a withDensity: (vol.withDensity f).map (·+z) = vol.withDensity (f (·-z)). Lebesgue translation invariance. Used to express the affine-shift fibre (Q.map W).map(·+z) as a withDensity for the per-fibre a.c. argument. @audit:ok

Per-fibre absolute continuity (continuous disintegration with sum structure): for W ⊥ V under Q with Q.map W ≪ volume, the affine-shift fibre (Q.map W).map (·+z) (= the per-fibre conditional law of W+V given V=z, via affineShiftKernel) is a.c. w.r.t. the sum marginal (Q.map W) ∗ (Q.map V) for a.e. z ∂(Q.map V). This is the continuous version of the general disintegration fact condDistrib z ≪ μ.map X (Mathlib's general/non-discrete version is absent; the in-tree Bridge.condDistrib_ae_absolutelyContinuous_map is [Countable X]-only, unusable for X = ℝ).

The argument uses the sum density r(x) = ∫⁻ v, f_W(x-v) ∂μ_V and the translate density f_W(·-z): a Fubini argument gives (μ_V × vol)({(z,x) : r(x) = 0 ∧ 0 < f_W(x-z)}) = 0, and a swap yields {r = 0} ⊆ {f_W(·-z) = 0} vol-a.e. for a.e. z, which converts to absolute continuity between the withDensity measures. @audit:ok

Per-z Jensen a.e. bound feeding negPart_negMulLog_conv_single_ne_top: max (φ (r z)) 0 ≤ ∫ v, max (φ (fW (z - v))) 0 ∂μV a.e., where φ t = t log t, fW = toReal ∘ μW.rnDeriv, r = toReal ∘ (μW ∗ μV).rnDeriv.

Single-component negative-part finiteness of the sum law: B(μW ∗ μV) < ⊤ from B(μW) < ⊤. The averaging is over the general probability measure μV (no absolute continuity on μV needed, so it works even when V is non-a.c.), bounding the W-marginal negative part B(μW). The core is a per-z Jensen bound on the convex t ↦ t log t against the convolution density, followed by a Tonelli collapse using translation invariance.

@audit:ok