Explicit-density variant of isDeBruijnRegularityHyp_of_methodX_unitnoise.

Replaces the canonical rnDeriv prefix with an explicit pX : ℝ → ℝ argument, allowing the caller to pass a pointwise-regular density such as conv(pX_base, g_t) directly without having to transport IsRegularDensityV2 through an a.e.-equality. @audit:ok

Explicit-density variant of entropy_power_inequality_of_density.

States regularity hypotheses for pX, pY, pXY as explicit ℝ → ℝ arguments rather than canonical rnDeriv representatives, and adds withDensity links. All hypotheses are regularity preconditions; they do not encode the EPI inequality core. @audit:ok

Blachman bridge — IsBlachmanConvReady (convDensityAdd p_base g_τ) (gaussianPDFReal 0 v).

The explicit entropy_power_inequality_of_density_explicit requires, for each density witness q, a hready : ∀ v ≠ 0, IsBlachmanConvReady q (gaussianPDFReal 0 v). When q is itself a conv-density convDensityAdd p_base g_τ, the bare IsBlachmanConvReady (conv …) (g_v) shape is supplied by the asymmetric producer isBlachmanConvReady_convDensityAdd_gaussian_asym: take its second arm pY := gaussianPDFReal 0 ⟨v/2,_⟩ at time v/2, so its second factor convDensityAdd g_{v/2} g_{v/2} collapses to gaussianPDFReal 0 v via the variance-doubling identity convDensityAdd_gaussian_variance_double.

All hypotheses are regularity preconditions; the conclusion (19-field bundle) is genuinely derived. No bundled analytic core.

Per-t smoothing EPI.

For smoothed variables X_t = X + √t·Z_X, Y_t = Y + √t·Z_Y (independent standard-normal noises), the entropy-power inequality holds at every fixed t > 0. Proved by instantiating the explicit-density EPI entropy_power_inequality_of_density_explicit at X := X_t, Y := Y_t, with conv-density witnesses convDensityAdd p_base g_τ (canonical-base densities convolved with the smoothing Gaussian), and discharging all regularity obligations via the public conv-Gaussian producers (regularity / normalization / Blachman / finite Fisher / finite entropy). @audit:ok

Finite-variance classical EPI (Real, no noise).

The base-level entropy-power inequality N(X+Y) ≥ N(X) + N(Y) for absolutely continuous, finite-variance, independent X, Y — with NO smoothing noise. Obtained by lifting to a 3-noise space, instantiating the per-t smoothing EPI entropyPower_smoothed_epi_perT at every t > 0, and pushing t → 0⁺ via heat-flow endpoint continuity (heatFlowEntropyPower_continuousWithinAt_zero) with le_of_tendsto_of_tendsto.

The entropy-integrability hypotheses hX_ent/hY_ent/hent_sum are regularity preconditions (finite differential entropy of the marginals/sum); they do NOT encode the EPI conclusion (load-bearing-free). @audit:ok

Finite-variance classical EPI (ext, ℝ≥0∞).

The entropyPowerExt (ℝ≥0∞-valued) version of entropy_power_add_ge_of_finite_variance. Under the same hypotheses, Nₑ(X+Y) ≥ Nₑ(X) + Nₑ(Y) in ℝ≥0∞. Obtained by lifting the Real inequality through entropyPowerExt_of_ac_integrable (entropyPowerExt μ = ENNReal.ofReal (entropyPower μ) for a.c. + finite-entropy μ) and ENNReal.ofReal_add (both entropy powers nonneg). @audit:ok