The continuous conditional differential entropy h(X | Z). Defined directly on the Mathlib regular conditional distribution condDistrib X Z μ (the conditional law of X given Z, a Kernel α ℝ): the fiber differential entropy differentialEntropy ((condDistrib X Z μ) z) averaged over the law μ.map Z of Z.

Mathlib-shape: the textbook ∫_z h(X | Z = z) dμ_Z(z) is realized through the condDistrib disintegration so that compProd_map_condDistrib and differentialEntropy_map_add_const are usable verbatim.

Differential mutual information expressed as a Kullback-Leibler divergence:

h(X) − h(X | Z) = KL(joint ‖ product).toReal,

where joint := (μ.map Z) ⊗ₘ condDistrib X Z μ (the law of (Z, X), by compProd_map_condDistrib) and product := (μ.map Z) ⊗ₘ Kernel.const _ (μ.map X) (= (μ.map Z).prod (μ.map X), by Measure.compProd_const). This is the differential-entropy-level statement of I(X;Z) = h(X) − h(X|Z).

Assembled from three components, with the regularity / integrability hypotheses threaded as honest preconditions:

• (a) InformationTheory.klDiv_compProd_const_toReal_integral (CondKLIntegral.lean) turns the joint KL toReal into the μ_Z-average of the fiberwise KL ∫ z, (klDiv (κ z) μ_X).toReal ∂μ_Z;
• (b) klDiv_toReal_eq_neg_differentialEntropy_sub_cross (BridgeDensityHelpers.lean) expands each fiber into −h(κ z) − ∫ p_z · log q_X;
• (c) integral_condDistrib_density_marginal_eq (BridgeDensityHelpers.lean) identifies ∫_z ∫ p_z log q_X ∂μ_Z = ∫ q_X log q_X = −h(μ_X) (Fubini marginal).

Assembling: RHS = −h(X|Z) − (−h(X)) = h(X) − h(X|Z). The classical continuous I(X;Z) = h(X) − h(X|Z) = D(P_{Z,X} ‖ P_Z ⊗ P_X) identity.

All added hypotheses are regularity preconditions (absolute continuity, per-fiber absolute continuity, equal mass via Markov, integrability = KL finiteness), not load-bearing bundles. The equal-mass condition κ z univ = μ_X univ is discharged internally (both probability measures). @audit:ok

Conditioning reduces the differential entropy: h(X | Z) ≤ h(X).

The differential analogue of I(X;Z) = h(X) − h(X|Z) = KL(joint ‖ product) ≥ 0. The bridge differentialEntropy_sub_condDifferentialEntropy_eq_toReal_klDiv identifies the entropy difference with (klDiv joint product).toReal, whose non-negativity is type-trivial (ENNReal.toReal_nonneg, since klDiv is ℝ≥0∞-valued), so the conditioning-reduces-entropy inequality follows by sub_nonneg.

The hypotheses are all preconditions (regularity / absolute continuity / integrability = KL finiteness), not load-bearing: hX_ac : μ.map X ≪ volume ensures h(X) reflects the density, measurability is structural, and the bridge's regularity / integrability preconditions are threaded through unchanged. @audit:ok

The z-dependent affine-shift kernel κ z := νX.map (· + c·z), built as a Kernel ℝ ℝ. Construction: push the parametrized pairing z ↦ νX.map (Prod.mk z) (measurable by Measurable.map_prodMk_left) through the measurable affine map (z, x) ↦ x + c·z.

@audit:ok

Plumbing core (buildable, not a Mathlib wall): the pushforward of the product measure νZ ⊗ νX through the affine map g (z, x) = (z, x + c·z) equals the composition product of νZ with the z-dependent affine-shift kernel affineShiftKernel νX c.

@audit:ok

Fiber identification for an independent sum: for X ⊥ Z, h(X + c·Z | Z) = h(X).

Conditioned on Z = z, the variable fun ω ↦ X ω + c · Z ω is the constant shift X + c·z, whose differential entropy equals h(X) by translation invariance (differentialEntropy_map_add_const). Averaging the constant h(X) over the probability law μ.map Z reproduces h(X).

The fiber identification condDistrib (X + c·Z) Z μ =ᵐ[μ.map Z] affineShiftKernel (μ.map X) c is assembled via:

1. indepFun_iff_map_prod_eq_prod_map_map gives μ.map (fun ω ↦ (Z ω, X ω)) = (μ.map Z).prod (μ.map X) (independence).
2. Push the product through the affine map g (z, x) = (z, x + c·z) and identify it with (μ.map Z) ⊗ₘ (affineShiftKernel (μ.map X) c) (prod_map_affine_eq_compProd, the z-dependent affine-shift kernel built above).
3. condDistrib_ae_eq_of_measure_eq_compProd then gives the fiber identification, and differentialEntropy_map_add_const discharges each fiber to h(μ.map X).

The hypotheses are all preconditions: IndepFun X Z μ is a genuine independence precondition (not a load-bearing bundle), hX_ac is absolute continuity, measurability is structural.

@audit:ok

The (β) device form: convolution does not decrease differential entropy, stated through an underlying independent pair X ⊥ Z with Z Gaussian.

h(X) ≤ h(X + √s·Z) via the chain h(X) = h(X+√s·Z | Z) ≤ h(X+√s·Z) (condDifferentialEntropy_indep_add_eq + condDifferentialEntropy_le).

All hypotheses are regularity preconditions (the fields of IsHeatFlowEndpointRegular): measurability, independence, the noise law, and the absolute continuity of μ.map X. The bridge regularity / integrability preconditions (stated at the heat-flow path W := X + √s·Z) are threaded through unchanged. @audit:ok

The (β) density form: the target consumed by the EPI G2 sandwich layer-2.

Convolution with a Gaussian does not decrease the negMulLog entropy integral: ∫ negMulLog pX ≤ ∫ negMulLog (pX ∗ g_{u n}). Equivalently h(pX) ≤ h(pX ∗ g_t).

The underlying independent pair X ⊥ Z (with Z ∼ 𝒩(0, v_Z), s·v_Z = u n) is supplied as regularity preconditions, matching the fields of IsHeatFlowEndpointRegular. pX is identified with the density of μ.map X. The bridge regularity / integrability preconditions (stated at the heat-flow path W := X + √s·Z with s := u n / v_Z) are threaded through unchanged. @audit:ok