InformationTheory.Shannon.EPI.Case1.RatioLimit.PathRegular

The order-limit bridge to EPI. If the log-ratio gap R = csiszarLogRatioGap … is antitone on Set.Ici 0 and R t → 0 as t → ∞, then R 0 ≥ 0, and therefore the entropy power inequality holds.

R 0 ≥ R t for every t ≥ 0 (antitonicity); since R t → 0 and the tail predicate R 0 ≥ R t holds eventually, ge_of_tendsto gives R 0 ≥ 0. The final EPI step is epi_of_csiszarLogRatioGap_zero_nonneg. @audit:ok

The single-path scaling identity: for t > 0, entropyPower (P.map (fun ω => A ω + √t · B ω)) = t · entropyPower (P.map (fun ω => A ω / √t + B ω)).

A + √t·B = √t·(A/√t + B), so the law on the left is the law on the right pushed forward by (· * √t); entropyPower_map_mul_const with c = √t (squared = t) finishes. The a.c. + entropy-integrability of the unscaled W-path law are regularity preconditions (consumed by entropyPower_map_mul_const). @audit:ok

A per-t regularity bundle for the rescaled path A/√t + B, holding the preconditions of the two envelope lemmas (differentialEntropy_add_ge_of_indep for the lower bound, applied with X := B, Y := A/√t; differentialEntropy_le_gaussian_of_variance_le for the upper bound on μ := P.map (A/√t + B) with variance bound varA/t + v_B).

This is a regularity bundle (IndepFun / a.c. / fibre integrabilities / mean + variance-bound + integrabilities), NOT load-bearing: it never contains the conclusion Tendsto … N(B) nor either envelope inequality — those are derived in entropyPower_rescaled_path_tendsto by calling the lemmas with these preconditions.

Not load-bearing: each conjunct matches a regularity precondition of differentialEntropy_add_ge_of_indep (lower bundle, X:=B Y:=A/√t) or differentialEntropy_le_gaussian_of_variance_le (upper bundle). The variance-bound conjunct ∫(x-m)² ≤ varA/t + v_B is the standard h_var max-entropy input (not the squeeze core): varA is pinned ≥ Var A by the all-t requirement and the squeeze limit N(B) is independent of varA's value. Not vacuous (real constraints, satisfiable by Gaussian-smoothed a.c. paths, falsifiable by non-a.c. paths; conclusion nontrivial via the separate hB_law/hv_B).

As t → ∞, the rescaled W-path entropy power N(law(A/√t + B)) converges to the noise entropy power N(law B) when B has a Gaussian law of nonzero variance.

Squeeze: lower bound N(A/√t + B) ≥ N(B) (independent-noise monotonicity, differentialEntropy_add_ge_of_indep applied with X := B, Y := A/√t), upper bound N(A/√t + B) ≤ 2πe·(varA/t + v_B) → 2πe·v_B = N(B) (Gaussian max-entropy, differentialEntropy_le_gaussian_of_variance_le), both sandwiching N(law B) = 2πe·v_B (entropyPower_gaussianReal) as varA/t → 0 (tendsto_of_tendsto_of_tendsto_of_le_of_le').

The squeeze structure (constant lower envelope from independent-noise monotonicity

• decaying upper envelope from Gaussian max-entropy → common limit N(B)) is the analytic content of this lemma. All the per-t data feeding the two envelope lemmas are threaded as regularity preconditions (NOT load-bearing): IndepFun B (A/√t) (h_indep), a.c. of the path laws (h_path_ac, hB_ac), the 8 fibre integrabilities of the lower-bound lemma (h_lb), the max-entropy data of the upper-bound lemma (mean / variance bound by varA/t + v_B / integrabilities, packaged in h_ub). The conclusion N(W t) → N(B) is not encoded in any hypothesis — both envelopes are produced by Mathlib / in-tree lemmas, and their common limit is computed here.

varA (= Var A, threaded as a real regularity datum with h_varA_nn : 0 ≤ varA) @audit:ok

Scaling preserves absolute continuity: if P.map A ≪ volume then P.map (A/√t) ≪ volume for t > 0 (the map (·/√t) is a Lebesgue-a.c. linear isomorphism).

A density witness for A/√t: from P.map A ≪ volume, the rescaled input A/√t admits a Real density witness pX := ((P.map (A/√t)).rnDeriv volume).toReal with all the regularity (≥ 0, measurable, withDensity law, integrable, mass = 1, finite second moment) needed to invoke convDensityAdd_negMulLog_integrable_pub and the pPath_eq_convDensityAdd identification.

Discharge IsRescaledPathRegular from method-X regularity.

Given a Gaussian noise B (P.map B = gaussianReal 0 v_B, v_B ≠ 0) independent of the input A (hAB : IndepFun A B P), with A measurable + finite-second-moment data threaded as varA-regularity, construct the per-t regularity bundle IsRescaledPathRegular A B P varA v_B.

The key insight: the fibre of condDistrib (B + A/√t) (A/√t) P is the translated Gaussian gaussianReal z v_B (the law of B + z by affineShiftKernel/Gaussian translation). This avoids the density-witness obstruction for the general fibre: the fibre identification condDistrib (B + A/√t) (A/√t) P =ᵐ affineShiftKernel (P.map B) 1 (h_fibre_ae) and the per-fibre a.c. condDistrib z ≪ volume (hκ_v, via gaussianReal z v_B) are both closed — exactly the conjuncts that are intractable in the general case.

Preconditions only (NOT load-bearing): measurability, IndepFun A B P, the Gaussian noise law, finite-second-moment h_mom_A + varA-regularity (h_var_bound). The bundle being constructed is itself regularity (audited non-load-bearing at its def site §3).

All 9 integrability conjuncts are supplied. The 3 conditional-KL integrabilities are supplied via the extracted standalone lemmas in EPI/G2/ConvEntropyDensity.lean (convCrossEntropy_perFibre_integrable / convCrossEntropy_zAvg_integrable / convJointLlr_integrable), instantiated here with the Gaussian fibre q := gaussianPDFReal 0 v_B (translated by z) and the target convolution density g := convDensityAdd pX g_{v_B}. No signature change was needed: because the fibre is Gaussian (not the input density), the joint-llr branch (b) abs-entropy ∫ q·|log q| is the Gaussian self-entropy (finite via integrable_density_log_density_of_gaussian), so the inventory's suspected hpX_ent input-density-entropy precondition is not required (the X/Z roles are swapped vs. the density template, where the fibre is the input). All preconditions: hA_ac : P.map A ≪ volume (case-1 a.c. input, NOT load-bearing — consumed only for the density witness and P.map (A/√t) ≪ volume), h_mom_A (finite second moment, feeds the Gaussian-fibre moment domination), the Gaussian noise law, h_var_bound.

• The regularity conjuncts (closed here): IndepFun B (A/√t) (h_indep), a.c. of B + A/√t and A/√t + B (hW_ac/hμ_ac), the fibre identification h_fibre_ae + per-fibre a.c. hκ_v, the variance bound (threaded h_var_bound), joint-≪-product, the fibre/path self-entropy + log-density integrabilities, the squared-deviation, and the 3 cross-entropy conjuncts (per-z cross integrand, z-averaged cross-term, joint llr).
• The cross-entropy analytic core (condDifferentialEntropy_le's h_int/hκ_cross_int/h_cross_int): integrability of the path-density log g against each Gaussian fibre, dominated by the convDensityAdd_logFactor_poly_majorant |log g| ≤ (A+1)+B·x² and the Gaussian-fibre quadratic moments. @audit:ok