Stam inequality body — Step 3 (Cauchy–Schwarz to symmetric Fisher coupling) #

The 1-dimensional Stam inequality proof (Cover–Thomas / Stam 1959 / Blachman 1965) splits into four steps: the convolution score representation s_Z = E[s_X | Z] = E[s_Y | Z], pointwise Cauchy–Schwarz on the conditional expectation, total expectation against p_Z giving the symmetric Fisher coupling J(X + Y) ≤ λ² J(X) + (1 - λ)² J(Y), and optimization over λ giving 1 / J(X + Y) ≥ 1 / J(X) + 1 / J(Y). This file makes Step 3 — integrating the earlier steps into the symmetric Fisher coupling and bridging into the optimization — explicit.

Main statements #

• isStamInequalityHyp_of_indepFun — the full chain to the IsStamInequalityHyp signature, from regularity alone via stamCauchySchwarzOptimal_of_indepFun.
• stam_optimal_lambda_mem_unit — membership of the optimal λ in the unit interval.
• stam_coupling_saturates — the Gaussian saturation arithmetic kernel.
• entropyPower_add_ge_of_gaussian — pipeline integration via Gaussian saturation.

Implementation notes #

The analytic content of Steps 2-3 — the conditional Cauchy–Schwarz integrated against p_Z giving the convex Fisher bound and its λ-optimum — is localized to the single lemma StamInequality.stamCauchySchwarzOptimal_of_indepFun, which takes regularity preconditions only.

References #

[CoverThomas2006]; [Stam1959]; [Blachman1965].

§1 — Optimal λ membership (arithmetic) #

§4 — Full Step 1 → 4 chain to the Stam signature #

§5 — Gaussian saturation: Step 3 holds with equality at the optimum #

The Gaussian entropy power inequality runs via entropyPower_gaussian_additivity (see entropyPower_add_ge_of_gaussian below); stam_coupling_saturates is the arithmetic saturation kernel.

§6 — EPI pipeline integration #