InformationTheory

InformationTheory.Shannon.RateDistortion.Convexity

source

Imports 3

Rate-distortion convexity #

Convexity of the rate-distortion function in the distortion threshold (Cover–Thomas): for all D₁ D₂ : ℝ and λ ∈ [0, 1], R(λ D₁ + (1-λ) D₂) ≤ λ R(D₁) + (1-λ) R(D₂).

Main definitions #

  • mixtureMeasure — the convex combination of two joint measures at weight λ.

Main statements #

Implementation notes #

The joint convexity of klDiv (Cover–Thomas) is not available directly in Mathlib, so it is derived along the data-processing route in three layers: klDiv_joint_convex (a selector-extension on Bool × Ω combined with the pushforward DPI klDiv_map_le and the per-slice KL additivity of mutually singular components) → klDiv_mixture_le → rateDistortionFunction_convexOn. The infimum over feasible joints is pressed through ENNReal.mul_iInf_of_ne / iInf_add / add_iInf, with the boundary weights λ = 0, 1 handled in separate branches.

References #

  • T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Mixture measure and feasibility #

noncomputable def

InformationTheory.Shannon.mixtureMeasure

source
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (lam : ℝ) (ν₁ ν₂ : MeasureTheory.Measure (α × β)) :
MeasureTheory.Measure (α × β)

Convex combination of two joint measures on α × β with weight λ ∈ [0, 1].

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.mixtureMeasure_map_fst

      source
      {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (lam : ℝ) (ν₁ ν₂ : MeasureTheory.Measure (α × β)) :
      MeasureTheory.Measure.map Prod.fst (mixtureMeasure lam ν₁ ν₂) = ENNReal.ofReal lam • MeasureTheory.Measure.map Prod.fst ν₁ + ENNReal.ofReal (1 - lam) • MeasureTheory.Measure.map Prod.fst ν₂

      Prod.fst pushforward of a convex combination is the convex combination of pushforwards.

      Used by
        theorem

        InformationTheory.Shannon.mixtureMeasure_map_snd

        source
        {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (lam : ℝ) (ν₁ ν₂ : MeasureTheory.Measure (α × β)) :
        MeasureTheory.Measure.map Prod.snd (mixtureMeasure lam ν₁ ν₂) = ENNReal.ofReal lam • MeasureTheory.Measure.map Prod.snd ν₁ + ENNReal.ofReal (1 - lam) • MeasureTheory.Measure.map Prod.snd ν₂

        Prod.snd pushforward of a convex combination is the convex combination of pushforwards.

        Used by
          theorem

          InformationTheory.Shannon.mixtureMeasure_map_fst_eq

          source
          {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {lam : ℝ} (hlam₀ : 0 ≤ lam) (hlam₁ : lam ≤ 1) (P : MeasureTheory.Measure α) (ν₁ ν₂ : MeasureTheory.Measure (α × β)) (h₁ : MeasureTheory.Measure.map Prod.fst ν₁ = P) (h₂ : MeasureTheory.Measure.map Prod.fst ν₂ = P) :
          MeasureTheory.Measure.map Prod.fst (mixtureMeasure lam ν₁ ν₂) = P

          If two joint distributions share the same Prod.fst marginal P, then so does their convex combination (with λ ∈ [0, 1]).

          Used by
            theorem

            InformationTheory.Shannon.expectedDistortion_mixtureMeasure

            source
            {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {lam : ℝ} (hlam₀ : 0 ≤ lam) (hlam₁ : lam ≤ 1) (d : α → β → ℝ) (ν₁ ν₂ : MeasureTheory.Measure (α × β)) (h_int₁ : MeasureTheory.Integrable (fun (p : α × β) => d p.1 p.2) ν₁) (h_int₂ : MeasureTheory.Integrable (fun (p : α × β) => d p.1 p.2) ν₂) :
            expectedDistortion d (mixtureMeasure lam ν₁ ν₂) = lam * expectedDistortion d ν₁ + (1 - lam) * expectedDistortion d ν₂

            Expected distortion is linear in the joint measure: distortion of the convex combination equals the convex combination of distortions, provided distortion is integrable under each joint.

            Used by
              theorem

              InformationTheory.Shannon.mixtureMeasure_feasible

              source
              {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {lam : ℝ} (hlam₀ : 0 ≤ lam) (hlam₁ : lam ≤ 1) (P : MeasureTheory.Measure α) (d : α → β → ℝ) (ν₁ ν₂ : MeasureTheory.Measure (α × β)) (h_marg₁ : MeasureTheory.Measure.map Prod.fst ν₁ = P) (h_marg₂ : MeasureTheory.Measure.map Prod.fst ν₂ = P) {D₁ D₂ : ℝ} (h_dist₁ : expectedDistortion d ν₁ ≤ D₁) (h_dist₂ : expectedDistortion d ν₂ ≤ D₂) (h_int₁ : MeasureTheory.Integrable (fun (p : α × β) => d p.1 p.2) ν₁) (h_int₂ : MeasureTheory.Integrable (fun (p : α × β) => d p.1 p.2) ν₂) :
              MeasureTheory.Measure.map Prod.fst (mixtureMeasure lam ν₁ ν₂) = P ∧ expectedDistortion d (mixtureMeasure lam ν₁ ν₂) ≤ lam * D₁ + (1 - lam) * D₂

              Feasibility is preserved under convex combinations: if ν₁ is feasible at D₁ and ν₂ is feasible at D₂, then mixtureMeasure λ ν₁ ν₂ is feasible at λ D₁ + (1-λ) D₂.

              Used by

                Convexity of the rate-distortion function #

                The joint convexity of klDiv is obtained along the data-processing route in three layers: klDiv_joint_convex (joint convexity stripped of the rate-distortion marginal structure), klDiv_mixture_le (its specialization to the mixture-measure form), and rateDistortionFunction_convexOn (the infimum press).

                klDiv joint convexity gateway #

                theorem

                InformationTheory.Shannon.klDiv_joint_convex

                source
                {Ω : Type u_3} [MeasurableSpace Ω] {lam : ℝ} (_hlam₀ : 0 ≤ lam) (_hlam₁ : lam ≤ 1) (μ₁ μ₂ σ₁ σ₂ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ₁] [MeasureTheory.IsFiniteMeasure μ₂] [MeasureTheory.IsFiniteMeasure σ₁] [MeasureTheory.IsFiniteMeasure σ₂] :
                klDiv (ENNReal.ofReal lam • μ₁ + ENNReal.ofReal (1 - lam) • μ₂) (ENNReal.ofReal lam • σ₁ + ENNReal.ofReal (1 - lam) • σ₂) ≤ ENNReal.ofReal lam * klDiv μ₁ σ₁ + ENNReal.ofReal (1 - lam) * klDiv μ₂ σ₂

                Joint convexity of klDiv, stated independently of the rate-distortion marginal structure: built from the selector extension on Bool × Ω, the pushforward DPI klDiv_map_le (forgetting the selector via Prod.snd), and the per-slice KL computation klDiv_two_slice.

                The hypotheses _hlam₀ / _hlam₁ (lam ∈ [0,1]) are unused in the body: the ENNReal.ofReal clamp of negative values makes the statement hold for every lam, so they are kept only as framing.

                @audit:ok

                Used by

                  klDiv joint convexity in mixture-measure form #

                  theorem

                  InformationTheory.Shannon.klDiv_mixture_le

                  source
                  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {lam : ℝ} (hlam₀ : 0 ≤ lam) (hlam₁ : lam ≤ 1) (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (ν₁ ν₂ : MeasureTheory.Measure (α × β)) [MeasureTheory.IsFiniteMeasure ν₁] [MeasureTheory.IsFiniteMeasure ν₂] (h₁ : MeasureTheory.Measure.map Prod.fst ν₁ = P) (h₂ : MeasureTheory.Measure.map Prod.fst ν₂ = P) :
                  klDiv (mixtureMeasure lam ν₁ ν₂) ((MeasureTheory.Measure.map Prod.fst (mixtureMeasure lam ν₁ ν₂)).prod (MeasureTheory.Measure.map Prod.snd (mixtureMeasure lam ν₁ ν₂))) ≤ ENNReal.ofReal lam * klDiv ν₁ ((MeasureTheory.Measure.map Prod.fst ν₁).prod (MeasureTheory.Measure.map Prod.snd ν₁)) + ENNReal.ofReal (1 - lam) * klDiv ν₂ ((MeasureTheory.Measure.map Prod.fst ν₂).prod (MeasureTheory.Measure.map Prod.snd ν₂))

                  Joint convexity of klDiv in mixture-measure form: the denominator P (the X-marginal) is fixed across both witnesses, only ν.map snd is linear. Specialization of klDiv_joint_convex.

                  @audit:ok

                  Used by

                    Convexity of the rate-distortion function (infimum press) #

                    theorem

                    InformationTheory.Shannon.rateDistortionFunction_convexOn

                    source
                    {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] (d : α → β → ℝ) (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] {lam : ℝ} (hlam₀ : 0 ≤ lam) (hlam₁ : lam ≤ 1) (D₁ D₂ : ℝ) (h_int_witness : ∀ (ν : MeasureTheory.Measure (α × β)), MeasureTheory.Measure.map Prod.fst ν = P → MeasureTheory.Integrable (fun (p : α × β) => d p.1 p.2) ν) :
                    rateDistortionFunction d P (lam * D₁ + (1 - lam) * D₂) ≤ ENNReal.ofReal lam * rateDistortionFunction d P D₁ + ENNReal.ofReal (1 - lam) * rateDistortionFunction d P D₂

                    The rate-distortion function is convex in the distortion threshold, R(λ D₁ + (1-λ) D₂) ≤ λ R(D₁) + (1-λ) R(D₂).

                    The hypothesis h_int_witness (integrability of d on every joint with Prod.fst-marginal P) is a regularity precondition, needed so that the mixture witness has well-defined feasibility (expectedDistortion linearity).

                    @audit:ok

                    Used by