Stam → de Bruijn → EPI conclusion assembly #

The EPI proof pieces:

• The Stam inequality (Cover-Thomas). Step 4 (λ-optimization closed form J_sum ≤ J_X J_Y / (J_X + J_Y)) is fully arithmetic, in EPI/Stam/Inequality.lean (stam_lambda_min, stam_lambda_lower_bound, stam_inverse_form_of_harmonic_mean). The Step 2-3 analytic core (the conditional Cauchy-Schwarz + convex Fisher bound) is localized to the single lemma StamInequality.stamCauchySchwarzOptimal_of_indepFun, via convex_fisher_bound_of_ready (regularity preconditions only). The chain isStamInequalityHyp_of_indepFun discharges IsStamInequalityHyp from regularity alone via that lemma.
• The de Bruijn identity (V2). deBruijn_identity_v2 gives, from IsRegularDeBruijnHypV2, the heat-flow derivative (d/dt) h(X + √t · Z) = (1/2) · J(g_t), with the Gaussian case deBruijn_identity_v2_gaussian fully discharged hypothesis-free.

This file is the conclusion-assembly layer: it wires those discharged Stam + de Bruijn pieces into a tighter EPI pipeline, reducing the EPI main theorem's remaining hypothesis to the irreducible primitives.

Approach #

This file wires the Stam + de Bruijn pieces directly into the EPI conclusion, with no intermediate scaling-decomposition structure. The wiring proceeds two ways:

1. Stam from regularity (§2). The Step 2-3 analytic core is localized to stamCauchySchwarzOptimal_of_indepFun; isStamInequalityHyp_of_primitives derives IsStamInequalityHyp from regularity preconditions alone (no load-bearing analytic hypothesis).
2. The de Bruijn gap-monotonicity engine (§1, §6). The de Bruijn derivative g'(t) = (1/2) · J(g_t) is ≥ 0 because Fisher information is non-negative (fisherInfoOfDensityReal_nonneg). This is the monotonicity content that makes the EPI gap monotone along the heat-flow scaling path — we discharge g'(t) ≥ 0 outright from the de Bruijn V2 witness.

The EPI conclusion (§3) is landed from regularity by deriving the Stam inequality from stamCauchySchwarzOptimal_of_indepFun and feeding it through the monolithic IsEPIL3IntegratedPipeline. The Gaussian EPI (§5) is obtained directly from Gaussian saturation (entropy_power_inequality_gaussian'), with no Stam claim.

Main statements #

• IsEPIGapMonotoneHyp — de Bruijn gap-monotonicity sub-predicate (§1)
• deBruijn_deriv_nonneg / isEPIGapMonotoneHyp_of_deBruijnV2 — g'(t) ≥ 0 (§1)
• isStamInequalityHyp_of_primitives — Stam from regularity (§2)
• entropy_power_inequality_gaussian' — Gaussian EPI via saturation (§5)
• deBruijn_gap_deriv_nonneg_gaussian — composed Gaussian gap monotonicity (§6)

Implementation notes #

The conditional Cauchy-Schwarz plus convex Fisher bound (Cover-Thomas's deepest analytic content) is localized to stamCauchySchwarzOptimal_of_indepFun, which produces it from regularity preconditions alone via convex_fisher_bound_of_ready; isStamInequalityHyp_via_body (EPI/Stam/Inequality.lean) reshapes that harmonic-mean bound into the published IsStamInequalityHyp signature. The Stam→EPI bridge (IsStamToEPIBridgeHyp, Csiszár scaling-path coupling, Cover-Thomas) is not a field of the integrated pipeline: consumers that need the entropy power inequality supply it separately through epi_via_stam, discharged in the Gaussian case by isStamToEPIBridgeHyp_of_gaussian.

§1 — de Bruijn gap-monotonicity engine #

§2 — Stam inequality from regularity #

§3 — Main EPI from regularity #

isStamInequalityHyp_of_primitives above supplies IsStamInequalityHyp from regularity alone; combined with an IsStamToEPIBridgeHyp witness through epi_via_stam this yields IsEntropyPowerInequalityHypothesis. The analytic content is localized to stamCauchySchwarzOptimal_of_indepFun.

§5 — Gaussian EPI (via saturation) #

The Gaussian EPI is entropy_power_inequality_gaussian' below (direct from entropyPower_gaussian_additivity), which carries no Stam claim: the inequality comes entirely from Gaussian saturation.

§6 — Composed de Bruijn gap-monotonicity into the EPI gap #