W2, the withDensity rnDeriv quotient identification (the largest gap, an assembly of existing parts). For f ≥ 0, g > 0, both measurable and integrable, the Radon–Nikodym derivative of volume.withDensity (ofReal∘f) w.r.t. volume.withDensity (ofReal∘g) is, γ-a.e. (with γ the g-weighted measure), the pointwise quotient ofReal (f x / g x).

Route: Measure.rnDeriv_withDensity collapses each withDensity rnDeriv to its density on the volume axis, rnDeriv_withDensity_right inverts the right withDensity, and the base is transferred =ᵐ[volume] ⟹ =ᵐ[γ] through volume ≪ γ (g > 0).

hf_meas/hg_meas/hf_nn/hg_pos/hf_int/hg_int are regularity preconditions. @audit:ok

W1, KL lower-semicontinuity via klFun-Fatou (the heart of the route). If μ_n.rnDeriv γ → μ.rnDeriv γ γ-a.e. (as reals), then klDiv μ γ ≤ liminf klDiv (μ_n) γ.

Route: rewrite both sides with the ℝ≥0∞ integral form klDiv_eq_lintegral_klFun_of_ac, apply Fatou lintegral_liminf_le (klFun ≥ 0, lifted by ENNReal.ofReal), and discharge the pointwise liminf bound via continuity of klFun composed with the a.e. convergence.

hμ_ac/hμn_ac (absolute continuity) and h_ae (a.e. convergence input) are preconditions; the conclusion is the LSC inequality (not bundled). @audit:ok

W4, density-level a.e. subsequence convergence (the negMulLog-free companion of negMulLog_convDensity_tendsto_ae_subseq in EPI/Vitali/AE.lean). Along any sequence u → 0⁺, the smoothed densities convDensityAdd pX g_{u n} converge to pX a.e. along a subsequence n ↦ u (ns n) (StrictMono ns), before composing with any continuous map.

Same route as EPI/Vitali/AE.lean but cut before the negMulLog composition: layer-1 L¹ convergence convDensityAdd_tendsto_L1_zero (@audit:ok, sorryAx-free) → tendstoInMeasure_of_tendsto_eLpNorm (Lp → measure) → TendstoInMeasure.exists_seq_tendsto_ae (measure → a.e. subsequence). No own sorry.

All hpX_* are regularity preconditions; hu_lim is the input filter. @audit:ok

The log of the Gaussian density as a quadratic (verbatim from the gaussianPDFReal definition (√(2πv))⁻¹ · exp(-(x-μ)²/(2v))). For v ≠ 0 and μ = 0: log (gaussianPDFReal 0 v x) = - log (√(2πv)) - x² / (2v). @audit:ok

The cross-term closed form for a smoothed density against a Gaussian log-density. With g := gaussianPDFReal 0 σ² (σ² ≠ 0) and f_t := convDensityAdd pX g_t (t > 0), the cross integral ∫ f_t · log g is an affine function of t: ∫ x, f_t x · log (g x) = c₀ · 1 − (1/(2σ²)) · (M2(pX) + (∫pX)·t), where c₀ = − log (√(2πσ²)) and M2(pX) = ∫ x²·pX. @audit:ok

The limit of the marginal cross-term ∫ pX · log g in the same expanded form. With g := gaussianPDFReal 0 σ², ∫ x, pX x · log (g x) = c₀·(∫pX) − (1/(2σ²))·M2(pX). @audit:ok

W3, cross-term convergence ∫ f_n · log g → ∫ pX · log g as u_n → 0⁺. Combines the affine closed form cross_term_closed_form (in t) with the marginal expansion pX_cross_term_expand; the difference is −(1/(2σ²))·(∫pX)·u_n → 0. @audit:ok