InformationTheory.Shannon.EPI.Case1.RatioLimit.Producer

The standardized noise Z' = Z/√v (v > 0) on the time-reparametrized path X + √(t·v)·Z' agrees pointwise (everywhere, not just a.e.) with the original path X + √t·Z. Used to bridge the sum-instance's 𝒩(0,2) noise to a unit W. The hypothesis 0 < v is required (√v ≠ 0); the v = 0 degeneracy (division by √0 = 0) is excluded.

@audit:ok — pointwise identity (funext + Real.sqrt_mul + field_simp). Signature: the conclusion is an equality of two explicit gaussianConvolution functions, not embedded in any hypothesis; 0 < v is a non-degeneracy precondition (excludes the √0 = 0 division), NOT load-bearing. map_gaussianConvolution_rescale_eq likewise @audit:ok (single rw).

In P.map form, the laws of the standardized time-reparam path and the original path coincide (consequence of the pointwise identity).

Fisher monotonicity under Gaussian convolution (Stam lam = 1 corollary).

For densities fX, fY satisfying the Stam regularity preconditions (IsRegularDensityV2, normalization to 1, and the IsBlachmanConvReady integrability / boundedness bundle), convolution decreases Fisher information:

`(J(convDensityAdd fX fY)).toReal ≤ (J fX).toReal`.

Derivation: specialize convex_fisher_bound_of_ready at lam = 1 (RHS collapses to 1²·J(fX) + 0²·J(fY) = J(fX)). The hypotheses are regularity preconditions, NOT load-bearing — the inequality core is supplied by the @audit:ok convex_fisher_bound_of_ready.

From method-X input regularity (X measurable, a.c., finite second moment) and standard-normal noise Z_X independent of X, supply the IsDeBruijnRegularityHyp X Z_X P group threaded by the case-1 wrapper.

The V2 reg_at instance is built directly (mirroring IsRegularDeBruijnHypV2.ofHeatFlow's field plumbing, but taking the unit Z_law from hZX_law instead of an IsHeatFlowDensity witness — ofHeatFlow only consumes h_heat.Z_law anyway, so going direct avoids bundling the load-bearing heat-equation field). The density_path/conv-pin fields use the convolution density. The pX series is a regularity precondition (X has a Lebesgue density + finite variance), discharged from hX_ac/h_mom_X.

The integrable_deriv field — interval-integrability of t ↦ (1/2)·J(density_t) on [0,T] — is supplied via design (b) (strengthened input regularity).

Design (b). Three input-regularity preconditions are threaded (hreg_pX, hnorm_pX, hready_pX — see signature below), together with the earlier h_fisher_X. They state that pX = (P.map X).rnDeriv volume is a regular L¹ density (IsRegularDensityV2 pX: differentiable + strictly positive + tails → 0 + integrable derivative), is normalized (∫ pX = 1), and satisfies the Integrable/boundedness/positivity bundle IsBlachmanConvReady pX (gaussianPDFReal 0 v) against every centered Gaussian (h_fisher_X adds finiteness of the input's Fisher info). None of these encode the Fisher-monotonicity / de Bruijn inequality core — they are regularity preconditions, NOT load-bearing.

With them the bound is supplied in two steps:

1. Fisher monotonicity (Stam). For every t ∈ Ioc 0 T, t.toNNReal ≠ 0, so g_t := gaussianPDFReal 0 t.toNNReal is a regular normalized density (isRegularDensityV2_gaussianPDFReal, integral_gaussianPDFReal_eq_one). PB-2b (fisherInfoOfDensity_convDensityAdd_le, = convex_fisher_bound_of_ready at lam = 1) fires directly on fX := pX, fY := g_t, giving the uniform bound (1/2)·J(density_t).toReal ≤ (1/2)·J(pX).toReal =: C on Ioc 0 T, finite and t-independent. (The bridge fisherInfoOfMeasureV2 _ f = fisherInfoOfDensity f is rfl, so the measure argument is dropped; the integrand reduces to (1/2)·J(convDensityAdd pX g_t).toReal.)
2. The t-measurability of t ↦ J(density_t).toReal (AEStronglyMeasurable on Ι 0 T), required by Measure.integrableOn_of_bounded. The (t,x)-jointly measurable logDeriv (convDensityAdd pX g_t) feeding the fisherInfoOfDensity lintegral has no direct Mathlib parameter-measurability lemma; it is supplied by EPICase1ProducerMeasurability.aestronglyMeasurable_fisherInfo_t (the C-b closed-form score route).

The rest of the group is the standard regularity plumbing, and the finite-Fisher precondition is in place so PB-6 can thread it to the case-1 wrapper.

@audit:ok (the integrable_deriv t-measurability is supplied (not residual), via EPICase1ProducerMeasurability.aestronglyMeasurable_fisherInfo_t (the closed-form score route; the joint (t,x)-measurability of logDeriv (convDensityAdd pX g_t) follows from deriv (conv_t) = ∫ x, pX x · deriv g_t (z-x) divided by conv_t). All threaded preconditions (IsRegularDensityV2 / normalization / IsBlachmanConvReady / finite Fisher / a.c. / second moment) are regularity, NOT load-bearing: the IsDeBruijnRegularityHyp structure carries no analytic-core field — de Bruijn is delivered externally by debruijnIdentityV2_holds_assembled, and IsBlachmanConvReady's fields assert only integrability of the Tonelli-expansion integrands, never their values or any inequality, so the Fisher-monotonicity conclusion J(conv) ≤ J(pX) is not smuggled through them — it is produced by convex_fisher_bound_of_ready at lam = 1. The density_t_eq := fun _ _ => rfl anti-trivial-zero pin keeps the conclusion non-degenerate.)