G2 Vitali witness — a.e. pointwise convergence of the entropy integrands (subsequence) #

This file supplies the genuine a.e.-convergence building block consumed by the layer-2 machinery differentialEntropy_convDensity_integral_tendsto in EPI/G2/HeatFlowContinuity.lean. Along any sequence u → 0⁺, the entropy integrands negMulLog (convDensityAdd pX g_{u n}) converge to negMulLog pX a.e. along a subsequence n ↦ u (ns n) (StrictMono ns).

Why a subsequence (and why that is enough) #

The genuine scaffolding is the layer-1 L¹ convergence convDensityAdd_tendsto_L1_zero (EPI/ApproxIdentityL1.lean, @audit:ok). Composing it with hu_lim and feeding it through tendstoInMeasure_of_tendsto_eLpNorm (Lp → measure) and TendstoInMeasure.exists_seq_tendsto_ae (measure → a.e.) yields a.e. convergence of convDensityAdd pX g_{u n} → pX along a subsequence f (ns i) (StrictMono ns), composed through the continuous map Real.negMulLog.

Mathlib has no full-sequence a.e. lemma from L¹/measure convergence for the Gaussian kernel (every route — TendstoInMeasure.exists_seq_tendsto_ae / exists_seq_tendsto_ae' — is subsequence-only; the only full-sequence a.e. mollifier lemma ContDiffBump.ae_convolution_tendsto_right_of_locallyIntegrable is compact-support-bump-limited, and gaussianPDFReal is not a ContDiffBump). Rather than carry a parked full-sequence witness, the layer-2 consumer is shaped to use this subsequence statement directly via tendsto_of_subseq_tendsto (the same device Mathlib's own tendsto_Lp_of_tendstoInMeasure uses): the entropy integral limit is proved by showing every subsequence has a further a.e.-convergent sub-subsequence, which this lemma supplies. No full-sequence a.e. fact is needed, so there is no residual here — the file is fully genuine.