Wyner–Ziv objective convexity (Cover–Thomas) #

This file discharges the h_obj_convex hypothesis carried by WynerZiv/FactorizableRate.lean (wynerZivRateFactorizable_convex, wynerZivRateFactorizable_convex_in_D_of_obj_convex): the convexity of the Wyner–Ziv objective I(X;U) − I(Y;U) in the joint pmf q, along convex combinations of factorizable joints q = κ(u|x)·P_XY(x,y).

Approach #

The objective wzMutualInfoXU U q − wzMutualInfoYU U q is expanded through the entropy form mutualInfoPmf m = H(fst m) + H(snd m) − H(m). Two exact algebraic cancellations make the deep content explicit and isolate it from the trivial parts:

• H(U) cancellation (any q): the U-marginal of wzMarginalXU U q and of wzMarginalYU U q coincide — both equal P_U(u) = ∑_{x,y} q(x,y,u) — by Fubini. Hence the ∑_u negMulLog(P_U u) terms (the H(U) blocks) cancel between I(X;U) and I(Y;U). This needs no factorization.

• H(X) − H(Y) constancy (factorizable q): the X-marginal of wzMarginalXU U q equals ∑_y q(x,y,·) summed over u, i.e. the (X)-marginal of wzMarginalXY U q. For factorizable q the latter is P_XY, so this block is the constant H(P_X) — independent of the kernel κ. Likewise the Y-block is the constant H(P_Y). Along a convex combination of two factorizable joints these constants are identical, so they cancel out of the convexity inequality.

After both cancellations the objective reads objective(q) = (H(P_X) − H(P_Y)) + (H(m_YU) − H(m_XU)), where m_XU = wzMarginalXU U q, m_YU = wzMarginalYU U q, and H(m) = ∑ negMulLog(m ·) is the joint Shannon block. The whole non-trivial content is therefore exactly the convexity of the conditional-entropy difference κ ↦ H(m_YU) − H(m_XU) (this is the conditional mutual information I(X;U|Y)).

That residual is published as the primitive predicate WynerZivCondEntDiffConvex — a genuine ConvexOn-shaped convexity-of-MI statement, the irreducible Lemma-15.9 core. h_obj_convex is then derived in full from this single predicate (wzObjective_convex_of_condEntDiff), and the rate-level wrapper wynerZivRateFactorizable_convex_in_D_of_obj_convex is re-published with h_obj_convex replaced by the strictly more primitive WynerZivCondEntDiffConvex.

Implementation notes #

The bare convexity of the conditional-entropy difference WynerZivCondEntDiffConvex is the irreducible analytic core of Cover–Thomas (convexity of I(X;U|Y) in κ, a joint-convexity-of-KL argument); it is carried as a predicate rather than proved here. Everything around it — the H(U) cancellation, the H(X)−H(Y) constancy, and the assembly into h_obj_convex — is discharged.

§1 Joint Shannon block of the (·,U) marginals #

§2 The U-marginals of wzMarginalXU and wzMarginalYU agree #

§3 The X/Y-marginals of the (·,U) marginals #

§4 Objective decomposition: H(U) cancellation #

§5 The marginal-block constant on factorizable joints #

§6 The primitive convexity predicate (Lemma-15.9 core) #

§7 h_obj_convex from the primitive predicate #

§8 Re-published rate-level convexity wrapper #