The conditional density p_{X|Z}(x|z) := fX(x) · fY(z - x) / p_Z(z), where p_Z = convDensityAdd fX fY. Explicit ratio form (no condDistrib).

The score weight W_λ(x,z) := λ · logDeriv fX x + (1-λ) · logDeriv fY (z - x).

Normalization of the conditional density: ∫ x, p_{X|Z}(x|z) dx = 1.

Numerator ∫ x, fX x · fY (z - x) = convDensityAdd fX fY z = p_Z(z) (by definition), divided by p_Z(z) > 0.

hpZ is a regularity precondition (positivity of the convolution density at z, satisfied whenever fX, fY > 0 are integrable). @audit:ok

S2, the symmetric derivative identity of the convolution density: ∫ x, deriv fX x · fY (z - x) = ∫ x, fX x · deriv fY (z - x) (both = p_Z'(z)). @audit:ok

S3, the score representation (the Blachman core, condExp-free).

For any λ, with W_λ(x,z) := λ · logDeriv fX x + (1-λ) · logDeriv fY (z - x), logDeriv (convDensityAdd fX fY) z = ∫ x, W_λ x z · p_{X|Z}(x|z) dx.

Proof skeleton (explicit Bochner integrals + cancellation, NO disintegration):

• logDeriv p_Z z = p_Z'(z) / p_Z(z) (gateway HasDerivAt + logDeriv_apply).
• ∫ W_λ · p_{X|Z} = (1/p_Z) ∫ W_λ · fX(x) fY(z-x).
• `W_λ · fX(x) fY(z-x) = λ (logDeriv fX x · fX x) fY(z-x)
  • (1-λ) fX x (logDeriv fY(z-x) · fY(z-x)), and logDeriv f · f = deriv f` pointwise (positivity).
• ∫ deriv fX(x) fY(z-x) = p_Z'(z) (S2) and ∫ fX(x) deriv fY(z-x) = p_Z'(z) (gateway derivative). Numerator = λ p_Z' + (1-λ) p_Z' = p_Z'. Divide by p_Z.

h_int_W is the regularity precondition that the weighted integrand is integrable. @audit:ok

Atom A, the lintegral↔Bochner bridge for the Fisher information of a density.

(fisherInfoOfDensity f).toReal = ∫ x, (logDeriv f x)² · f x ∂volume.

fisherInfoOfDensity f = ∫⁻ x, ofReal((logDeriv f x)²) · ofReal(f x) by definition; ofReal((logDeriv f x)² · f x) = ofReal((logDeriv f x)²) · ofReal(f x) by ENNReal.ofReal_mul (both factors nonneg), and the integrand (logDeriv f x)² · f x is nonnegative (hpos), so integral_eq_lintegral_of_nonneg_ae applies.

hpos (f ≥ 0) and hint (Bochner-integrability of the squared-score density) are regularity preconditions, satisfied by any probability density with finite Fisher information; neither bundles the Fisher-info value. @audit:ok

S4, the probability-weighted pointwise Cauchy-Schwarz of the score.

With W_λ(x,z) := scoreWeight fX fY lam z x and p_{X|Z}(x|z) := condDensityX fX fY z x (a probability weight: ≥ 0, ∫ = 1), and the S3 representation logDeriv p_Z z = ∫ x, W_λ · p_{X|Z}, Jensen / Cauchy-Schwarz gives

(logDeriv (convDensityAdd fX fY) z)² ≤ ∫ x, (W_λ x z)² · p_{X|Z}(x|z) dx.

hpZ (positivity of p_Z(z)) is a regularity precondition; the squared-weight integrability hint_Wsq is a regularity precondition on admissible densities. None of the hyps bundles the conclusion inequality.

With the probability measure μ := volume.withDensity (fun x => ENNReal.ofReal (condDensityX fX fY z x)) (IsProbabilityMeasure from 3b condDensityX_integral_eq_one via ofReal_integral_eq_lintegral_ofReal), S4 is exactly Jensen for the convex (·)²: Even.convexOn_pow + ConvexOn.map_integral_le (Mathlib/Analysis/Convex/Integral.lean:199, [IsProbabilityMeasure μ], g (∫ f ∂μ) ≤ ∫ g∘f ∂μ) composed with the change-of-variables integral_withDensity_eq_integral_toReal_smul₀ (Bochner/ContinuousLinearMap.lean:310) to rewrite ∫ · ∂μ = ∫ condDensityX·· ∂volume, and S3 score_conv_eq_weighted_integral to identify ∫ scoreWeight ∂μ with logDeriv p_Z z. condExp/condDistrib/disintegration absent (density route).

hcond_int (integrability of the conditional density), hint_W (integrability of the score weight against condDensityX) and hint_Wsq are regularity preconditions on admissible densities; none bundles the conclusion inequality. @audit:ok

The convex Fisher bound (density route).

For 0 ≤ lam ≤ 1, (fisherInfoOfDensity (convDensityAdd fX fY)).toReal ≤ lam² · (fisherInfoOfDensity fX).toReal + (1-lam)² · (fisherInfoOfDensity fY).toReal.

Proof shape (explicit density route, condExp-free):

• J_sum = ∫ z, (logDeriv p_Z z)² · p_Z(z) dz (atom A on p_Z = convDensityAdd fX fY).
• (logDeriv p_Z z)² ≤ ∫ x, W_λ² · p_{X|Z} pointwise (S4 score_sq_le_weighted_integral).
• integrate against p_Z, cancel p_{X|Z}·p_Z = fX(x)·fY(z-x), swap order (Tonelli), expand W_λ² = λ²s_X² + (1-λ)²s_Y² + 2λ(1-λ)s_X s_Y:
• λ² term = λ²·J_X (∫_z fY(z-x) dz = 1 by translation invariance + normalization),
• (1-λ)² term = (1-λ)²·J_Y,
• cross term = 0 (∫ logDeriv fX · fX = 0 and ∫ logDeriv fY · fY = 0, integral_logDeriv_density_eq_zero).

All bundled hypotheses are regularity preconditions (IsRegularDensityV2, boundedness, integrability side-conditions, normalization ∫ = 1, positivity of p_Z, and the three product-measure Integrable (uncurry …) Tonelli preconditions); none bundles the inequality core.

Assembly:

• atom A fisherInfoOfDensity_toReal_eq_integral rewrites all three Fisher informations to Bochner integrals;
• S4 score_sq_le_weighted_integral (@audit:ok, Jensen on a withDensity probability measure) gives (logDeriv p_Z z)² ≤ ∫ x, W_λ²·p_{X|Z} pointwise, integrated against p_Z ≥ 0 via integral_mono_ae;
• condDensityX·p_Z = fX(x)·fY(z-x) cancellation;
• the 3-term Tonelli evaluation convex_fisher_term1/2/cross (integral_integral_swap

• translation invariance integral_sub_right_eq_self + normalization / integral_logDeriv_density_eq_zero for the cross term) yields λ²·J_X + (1-λ)²·J_Y (cross term = 0). @audit:ok

Regularity precondition bundle for the convolution-Fisher analysis.

All 19 fields are regularity / integrability / boundedness / positivity preconditions; the bundle is field-for-field the same hypotheses convex_fisher_bound takes individually (see convex_fisher_bound_of_ready). The logDeriv (convDensityAdd fX fY)-containing fields (int_fisherZ / int_prod1/2/3) assert only Integrable (…) of the verbatim integrands, not the value of any integral nor any inequality, so none bundles the convex Fisher inequality core (which lives inside convex_fisher_bound's body). A proven Gaussian inhabitant isBlachmanConvReady_gaussianPDFReal (GaussianDensityRoute.lean, sorryAx-free) establishes non-vacuousness. @audit:ok

Symmetry of the regularity bundle under the X ↔ Y swap.

IsBlachmanConvReady is symmetric: convDensityAdd is commutative (convDensityAdd_comm) and each integrability / boundedness field transports across the reflection substitution x ↦ z - x (volume-preserving) together with the marginal swap on the product-measure fields. All 19 fields are constructed:

• int_fX/int_fY/bdd_*/int_fisherX/int_fisherY — direct X ↔ Y projection of h.
• pos_pZ/int_fisherZ — convDensityAdd_comm rewrite of the corresponding h field.
• int_X/int_Y/cond_int — reflection (Integrable.comp_sub_left) of the swapped h field, then a pointwise mul_comm.
• int_W/int_Wsq — reflection of h.int_W (1-lam) / h.int_Wsq (1-lam) (the lam ↔ 1-lam relabelling is exactly the X↔Y swap under x ↦ z - x).
• int_inner — z-pointwise congruence with h.int_inner (1-lam), the inner x-integral being reflection-invariant (integral_sub_left_eq_self).
• int_prod1/int_prod2 — separable rebuild from h Fisher/integrability fields, sheared by measurePreserving_prod_sub_swap ((z,x) ↦ (x, z-x)).
• int_prod3 — transport of h.int_prod3 by the skew map (z,x) ↦ (z, z-x) (MeasurePreserving.skew_product with the x ↦ z - x reflection on the 2nd coord).

Consumed only by the (unused) API-completeness lemmas isStamCauchySchwarz_symm / isStamCondExpCSHyp_symm. @audit:ok

The convex Fisher bound from the regularity bundle. Applies convex_fisher_bound by projecting the integrability / boundedness / positivity preconditions out of the IsBlachmanConvReady bundle. Pure plumbing — no analytic content beyond convex_fisher_bound. @audit:ok