Marginal identification. For a bounded-density observable g : ℝ → ℝ, the joint integral of g ∘ snd against p ⊗ₘ W equals the integral of g against the output marginal outputDistribution p W = (p ⊗ₘ W).snd.

General log-density entropy identification. For any μ : Measure ℝ with μ ≪ volume and measurable density f := μ.rnDeriv volume, the integral of log f against μ is −differentialEntropy μ. This is the generalization of integral_log_density_fibre to an arbitrary ≪ volume measure (the proof never used that μ was a channel fibre); it is reused for both the fibre term (μ := W x) and the output term (μ := outputDistribution p W) in the assembly below. @audit:ok

Fibre differential-entropy identification. For an ≪ volume fibre W x with measurable density f := (W x).rnDeriv volume, the inner integral of log f against W x is −differentialEntropy (W x). Thin wrapper around the general integral_log_rnDeriv_eq_neg_diffEntropy.

Proxy form of the fibre differential-entropy identification (Route B). Same conclusion as integral_log_density_fibre, but stated with a measurable PDF proxy g in place of the (non-jointly-measurable) measure-form rnDeriv. The proxy↔rnDeriv bridge is absorbed inside the integral via integral_congr_ae fed by the per-fibre a.e. agreement hg_ae, so no joint measurability is ever needed. This is the step that lets the body keep its fibre term in proxy form.

Linchpin: fibre form of the compProd Radon-Nikodym derivative (Mathlib TODO, Composition/RadonNikodym.lean:28-29). For finite μ, κ, η with μ ⊗ₘ κ ≪ μ ⊗ₘ η, the conditional rnDeriv ∂(μ⊗ₘκ)/∂(μ⊗ₘη) is (μ⊗ₘη)-a.e. the fibrewise kernel rnDeriv Kernel.rnDeriv κ η p.1 p.2.

Proof (withDensity route): μ⊗ₘκ ≪ μ⊗ₘη gives κ a ≪ η a a.e. (kernel_of_compProd), so κ =ᵐ[μ] η.withDensity (κ.rnDeriv η) (withDensity_rnDeriv_eq); hence μ⊗ₘκ = μ⊗ₘ(η.withDensity (κ.rnDeriv η)) = (μ⊗ₘη).withDensity (fun p ↦ κ.rnDeriv η p.1 p.2) (compProd_congr + compProd_withDensity); finish with Measure.rnDeriv_withDensity.

Per-measure log-density split (Bayes step). For ν ≪ q ≪ volume all σ-finite, the log of the relative density dν/dq splits as the difference of the two volume-log-densities: log (dν/dq y) = log (dν/dvol y) − log (dq/dvol y), ν-a.e. Built from the rnDeriv chain rule dν/dq · dq/dvol =ᵐ dν/dvol plus positivity (q ≪ vol ⇒ dq/dvol > 0 on ν since ν ≪ q).

★ General Bayes density split of the joint llr (modulo named ac hyps). For input law p, Markov channel W, output q := outputDistribution p W, with each fibre ≪ q ≪ volume and joint ≪ p.prod q, the log-likelihood ratio of the joint against the product factorizes into fibre/output log-densities. This is the body of the residual hypothesis h_llr_split. Combines the linchpin rnDeriv_compProd_fibre (at η := Kernel.const ℝ q) with rnDeriv_eq_rnDeriv_measure and the per-fibre log_rnDeriv_split.

★ Continuous-channel MI chain rule body (AWGN-independent).

(mutualInfoOfChannel p W).toReal = h(Y) − ∫ h(Y|X=x) dp(x), the density-level analogue of the discrete mutualInfo_eq_entropy_add_entropy_sub_jointEntropy.

Assembled from the local helpers. The proof opens mutualInfoOfChannel = klDiv (p⊗ₘW) (p.prod q) (q := outputDistribution p W) via toReal_klDiv_of_measure_eq (both factors are probability measures, so the univ-mass condition is automatic), rewrites the joint log-likelihood ratio by the Bayes density split llr_compProd_prod_split, splits the resulting integral with integral_sub, identifies the fibre term with integral_compProd + integral_log_proxy_fibre (each fibre ↦ −h(W x)), and identifies the output term with integral_snd_outputDistribution + integral_log_rnDeriv_eq_neg_diffEntropy (↦ −h(q)). @audit:ok

Generic marginal identification. For a ref-integrable observable g : β → ℝ, the joint integral of g ∘ snd against p ⊗ₘ W equals the integral of g against the output marginal outputDistribution p W = (p ⊗ₘ W).snd. Generic in α, β.

Generic per-measure log-density split (Bayes step). For ν ≪ q ≪ ref all σ-finite (with ν.HaveLebesgueDecomposition q, q.HaveLebesgueDecomposition ref), log (dν/dq y) = log (dν/dref y) − log (dq/dref y), ν-a.e. Generic reference ref.

★ Generic Bayes density split of the joint llr. For input law p, Markov channel W : Channel α β, output q := outputDistribution p W, with each fibre ≪ q ≪ ref and joint ≪ p.prod q, the log-likelihood ratio of the joint against the product factorizes into fibre/output log-densities. Generic in α, β, ref.

★ Generic continuous-channel MI chain rule body (output type β, reference ref), in log-density-integral form:

I.toReal = (∫ x, ∫ y, log(d(W x)/d ref y) ∂(W x) ∂p) − (∫ y, log(dq/d ref y) ∂q),

i.e. I = (−h(Y|X)) − (−h(Y)) = h(Y) − h(Y|X) once each integral is identified with the relevant neg-entropy by integral_log_rnDeriv_self_eq_neg. Mirrors the 1-D body mutualInfoOfChannel_toReal_eq_diffEntropy_sub. The hypothesis bundle is all-regularity (AC chain hWx_q/hq_ref/h_joint_ac, measurable proxy g + a.e.-identity hg_ae, compProd-level integrabilities, fibre/output integral-equality h_fibre_self/h_out_self); the core (KL→llr→Bayes split→Fubini) lives in the body via llr_compProd_prod_split_gen. @audit:ok