The 2-variable joint differential entropy. Defined -∫ negMulLog (dμ/dvol) on Measure (ℝ × ℝ), identical in shape to the 1-D differentialEntropy, so the existing 1-D density lemmas apply through volume_eq_prod (which holds by rfl).

The n-variable joint differential entropy on Measure (Fin n → ℝ) (the parallel-Gaussian consumer form). Fin n → ℝ is chosen over EuclideanSpace so that the product-Lebesgue API (volume_pi, Measure.pi) applies directly.

For μ ≪ ν, ∫ x, log((μ.rnDeriv ν x).toReal) ∂μ = -∫ x, negMulLog((μ.rnDeriv ν x).toReal) ∂ν.

The RHS is the (joint/1-D) differential entropy when ν is the relevant Lebesgue measure.

A generic withDensity_map (Mathlib absent, rnDeriv-version de-specialized). Pushforward of a withDensity measure along a measurable equivalence e: (μ.withDensity g).map e = (μ.map e).withDensity (g ∘ e.symm). Mathlib only ships the rnDeriv-specialized MeasurableEmbedding.map_withDensity_rnDeriv; the generic form below de-specializes its 5-line proof, replacing the final rnDeriv_map congruence by the trivial e.symm_apply_apply cancellation. @audit:ok

2-variable subadditivity bridge: (klDiv(joint ‖ μ_X ⊗ μ_Y)).toReal = h(μ_X) + h(μ_Y) − h(joint).

Hypotheses: absolute continuity + Bayes llr split h_llr_split + integrability. Superseded by klDiv_prod_marginals_toReal_eq_sum_sub_joint, which internalizes the split.

@audit:superseded-by(klDiv_prod_marginals_toReal_eq_sum_sub_joint)

2-variable differential-entropy subadditivity h(X,Y) ≤ h(X) + h(Y).

Requires an explicit h_llr_split hypothesis for the Bayes density split. Superseded by jointDifferentialEntropy_le_sum, which internalizes the split.

@audit:superseded-by(jointDifferentialEntropy_le_sum)

pi_withDensity (Mathlib absent, built by piFinSuccAbove induction). The product measure of withDensity factors is the withDensity of the product measure with the product density z ↦ ∏ᵢ fᵢ (z i). Specialized to Fin n → ℝ (all factors on ℝ), the form the n-variable density split requires. @audit:ok

n-variable product-marginals factorization: Measure.pi (μ.map (· i)) expressed as a withDensity on Lebesgue measure with product density z ↦ ∏ᵢ (μ.map (· i)).rnDeriv volume (z i). @audit:ok

n-variable LLR split (a.e.[μ]): the log-likelihood ratio of μ against the product of its marginals equals log(joint density) − ∑ᵢ log(marginalᵢ density) almost-everywhere wrt μ. The n-variable analogue of llr_split_from_density_factorize. @audit:ok

n-variable subadditivity bridge: (klDiv(joint ‖ ∏ᵢ μᵢ)).toReal = ∑ᵢ h(μᵢ) − h(joint), where μᵢ := μ.map (· i).

Regularity hypotheses: absolute continuity + Bochner integrability of log-density observables. @audit:ok

n-variable differential-entropy subadditivity h(Yⁿ) ≤ ∑ᵢ h(Yᵢ) (the parallel-Gaussian consumer form). KL ≥ 0 + the bridge, by linarith. @audit:ok

Product of marginals expressed as a withDensity on Lebesgue measure.

For a joint probability measure μ on ℝ × ℝ with marginals μX, μY both absolutely continuous wrt the Lebesgue measure, the product μX × μY factors through the Lebesgue measure on ℝ × ℝ as (μX).prod (μY) = volume.withDensity (z ↦ μX.rnDeriv volume z.1 * μY.rnDeriv volume z.2).

Log-likelihood ratio split for the 2-variable joint (a.e.[μ]).

The LLR of μ against the product of its marginals equals log(joint density) − log(marginal_X density on z.1) − log(marginal_Y density on z.2) almost-everywhere wrt μ.

2-variable subadditivity bridge without explicit h_llr_split: (klDiv(joint ‖ μ_X ⊗ μ_Y)).toReal = h(μ_X) + h(μ_Y) − h(joint).

The Bayes density split is produced internally by llr_split_from_density_factorize.

2-variable differential-entropy subadditivity h(X,Y) ≤ h(X) + h(Y).

The Bayes density split is internalized via llr_split_from_density_factorize; no explicit h_llr_split argument required.