InformationTheory

InformationTheory.Shannon.WynerZiv.ConditionalEntropyConvexity

source

Imports 8

Wyner–Ziv conditional-entropy-difference convexity #

This file proves the irreducible Lemma-15.9 core WynerZivCondEntDiffConvex (WynerZiv/ObjectiveConvexity.lean) from P_XY ≥ 0 alone, which is supplied at rate level by P_XY ∈ stdSimplex.

The core asserts convexity of H(m_YU) − H(m_XU) = I(X;U|Y) along convex combinations of factorizable joints. The proof routes the whole content through the per-atom log_sum_inequality_negMulLog (Fano/DPI.lean):

Step A — affine translation of the marginals #

theorem

InformationTheory.Shannon.wzMarginalXU_smul_add

source
{α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] (a b : ℝ) (q₁ q₂ : α × β × U → ℝ) :
wzMarginalXU U (a • q₁ + b • q₂) = a • wzMarginalXU U q₁ + b • wzMarginalXU U q₂

wzMarginalXU is affine in q: marginal of the mix = mix of marginals.

Used by
    theorem

    InformationTheory.Shannon.wzMarginalYU_smul_add

    source
    {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] (a b : ℝ) (q₁ q₂ : α × β × U → ℝ) :
    wzMarginalYU U (a • q₁ + b • q₂) = a • wzMarginalYU U q₁ + b • wzMarginalYU U q₂

    wzMarginalYU is affine in q.

    Used by

      Step B — per-u block convexity (the core) #

      theorem

      InformationTheory.Shannon.negMulLog_marginal_gap_le_joint_gap

      source
      {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (r₁ r₂ : α × β → ℝ) (hr₁ : ∀ (p : α × β), 0 ≤ r₁ p) (hr₂ : ∀ (p : α × β), 0 ≤ r₂ p) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
      ∑ y : β, ((∑ x : α, (a * r₁ (x, y) + b * r₂ (x, y))).negMulLog - a * (∑ x : α, r₁ (x, y)).negMulLog - b * (∑ x : α, r₂ (x, y)).negMulLog) ≤ ∑ y : β, ∑ x : α, ((a * r₁ (x, y) + b * r₂ (x, y)).negMulLog - a * (r₁ (x, y)).negMulLog - b * (r₂ (x, y)).negMulLog)

      Refinement / coarsening inequality (the DPI core). For two non-negative joint slices r₁, r₂ : α × β → ℝ and weights a, b ≥ 0 with a + b = 1, writing the mixture m = a • r₁ + b • r₂, the convexity of the Y-marginal-vs-joint entropy gap holds: ∑_y [neg(∑_x m(x,y)) − a·neg(∑_x r₁(x,y)) − b·neg(∑_x r₂(x,y))] ≤ ∑_y ∑_x [neg(m(x,y)) − a·neg(r₁(x,y)) − b·neg(r₂(x,y))].

      This is the data-processing inequality for the Jensen–Shannon gap under the coarsening (x,y) ↦ y, proved per y by log_sum_inequality_negMulLog with the two mixture components as the log-sum "fiber".

      Used by
        theorem

        InformationTheory.Shannon.wzCondEntDiff_block_convex

        source
        {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (h_pmf_nn : ∀ (p : α × β), 0 ≤ P_XY p) {q₁ q₂ : α × β × U → ℝ} (hq₁ : IsWynerZivFactorizable U P_XY q₁) (hq₂ : IsWynerZivFactorizable U P_XY q₂) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (u : U) :
        ∑ y : β, (wzMarginalYU U (a • q₁ + b • q₂) (y, u)).negMulLog - ∑ x : α, (wzMarginalXU U (a • q₁ + b • q₂) (x, u)).negMulLog ≤ a * (∑ y : β, (wzMarginalYU U q₁ (y, u)).negMulLog - ∑ x : α, (wzMarginalXU U q₁ (x, u)).negMulLog) + b * (∑ y : β, (wzMarginalYU U q₂ (y, u)).negMulLog - ∑ x : α, (wzMarginalXU U q₂ (x, u)).negMulLog)

        Per-u block convexity. For factorizable q₁, q₂ and weights a, b ≥ 0 with a + b = 1, the conditional-entropy-difference block at a fixed u, (∑_y negMulLog m_YU(y,u)) − (∑_x negMulLog m_XU(x,u)), is convex.

        Used by

          Step C/D — ∑_u aggregation + identification with joint blocks #

          theorem

          InformationTheory.Shannon.wzCondEntDiff_blockSum_eq_jointEntDiff

          source
          {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] (q : α × β × U → ℝ) :
          ∑ u : U, (∑ y : β, (wzMarginalYU U q (y, u)).negMulLog - ∑ x : α, (wzMarginalXU U q (x, u)).negMulLog) = wzJointEntYU U q - wzJointEntXU U q

          The ∑_u of the per-u block differences equals wzJointEntYU − wzJointEntXU.

          Used by

            Main theorem — convexity of the conditional-entropy difference #

            theorem

            InformationTheory.Shannon.wynerZivCondEntDiffConvex_holds

            source
            {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] (P_XY : α × β → ℝ) (h_pmf_nn : ∀ (p : α × β), 0 ≤ P_XY p) :
            WynerZivCondEntDiffConvex U P_XY

            The Lemma-15.9 core: WynerZivCondEntDiffConvex holds for every non-negative P_XY.

            Used by

              Rate-level convexity wrapper #

              theorem

              InformationTheory.Shannon.wynerZivRateFactorizable_convex_in_D

              source
              {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [MeasurableSpace α] [MeasurableSpace β] (U : Type u_3) [Fintype U] [MeasurableSpace U] {γ : Type u_4} {P_XY : α × β → ℝ} (h_pmf : P_XY ∈ stdSimplex ℝ (α × β)) (d : α → γ → ℝ) (f : U × β → γ) {D₁ D₂ : ℝ} {q₁ q₂ : α × β × U → ℝ} (h_feasible₁ : (q₁, f) ∈ WynerZivFactorizableConstraint U P_XY d D₁) (h_feasible₂ : (q₂, f) ∈ WynerZivFactorizableConstraint U P_XY d D₂) (h_attain₁ : wynerZivRateFactorizable U P_XY d D₁ = wzMutualInfoXU U q₁ - wzMutualInfoYU U q₁) (h_attain₂ : wynerZivRateFactorizable U P_XY d D₂ = wzMutualInfoXU U q₂ - wzMutualInfoYU U q₂) {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
              wynerZivRateFactorizable U P_XY d (a * D₁ + b * D₂) ≤ a * wynerZivRateFactorizable U P_XY d D₁ + b * wynerZivRateFactorizable U P_XY d D₂

              Convexity of the factorizable rate function in D, with the objective-convexity hypothesis supplied internally by wynerZivCondEntDiffConvex_holds.

              Used by