InformationTheory

InformationTheory.Shannon.RateDistortion.AchievabilityAmbientMeasure

source

Imports 5

Rate-distortion achievability — i.i.d. ambient measure instantiation #

The witness form of the rate-distortion achievability theorem carries the ambient i.i.d. construction (μ, Xs, Ys) and several entropy / distortion-bridge hypotheses as pass-throughs. This file fixes the ambient as iidAmbientJointMeasure (pmfToMeasure qStar), where qStar is a feasible joint pmf, and derives those pass-through hypotheses from that concrete choice. The only remaining external hypothesis is the codebook-averaged random-coding failure sequence, which requires strong-typicality machinery beyond the weak (entropy-only) typicality available here.

Hypotheses derived from the concrete ambient #

  • μ := iidAmbientJointMeasure (pmfToMeasure qStar) — i.i.d. ambient.
  • Xs := iidXs, Ys := iidYs — coordinate projections.
  • Measurability of Xs i, Ys i via measurable_iidXs, measurable_iidYs.
  • IsProbabilityMeasure (μ.map (Xs 0)), similarly for Ys 0, via the marginal identities and pmfToMeasure_isProbabilityMeasure.
  • expectedJointDistortion μ (Xs 0) (Ys 0) d = expectedDistortionPmf d qStar via the dirac/atom decomposition of pmfToMeasure.
  • Marginal-source identity: μ.map (Xs 0) = pmfToMeasure (marginalFst qStar).

Hypothesis left external #

  • h_codebook_avg_failure: requires strong typicality (joint type ~ q*) to bound the per-codebook conditional failure probability via the product law. Weak (entropy-only) typicality cannot give an exponential decay here; left as an external hypothesis on a failure_seq → 0 sequence.

pmfToMeasure marginal identities #

theorem

InformationTheory.Shannon.pmfToMeasure_map_fst_real_singleton

source
{α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {q : α × β → ℝ} (hq : q ∈ stdSimplex ℝ (α × β)) (a : α) :
(MeasureTheory.Measure.map Prod.fst (ChannelCoding.pmfToMeasure q)).real {a} = marginalFst q a

(pmfToMeasure q).map Prod.fst .real {a} = marginalFst q a for any joint pmf q : α × β → ℝ with q ∈ stdSimplex ℝ (α × β).

Used by
    theorem

    InformationTheory.Shannon.pmfToMeasure_map_snd_real_singleton

    source
    {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {q : α × β → ℝ} (hq : q ∈ stdSimplex ℝ (α × β)) (b : β) :
    (MeasureTheory.Measure.map Prod.snd (ChannelCoding.pmfToMeasure q)).real {b} = marginalSnd q b

    Symmetric: (pmfToMeasure q).map Prod.snd .real {b} = marginalSnd q b.

    Used by

      Positivity of joint pmf carries to pmfToMeasure singletons #

      theorem

      InformationTheory.Shannon.pmfToMeasure_real_singleton_pos

      source
      {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {q : α × β → ℝ} (hq : q ∈ stdSimplex ℝ (α × β)) (hq_pos : ∀ (p : α × β), 0 < q p) (p : α × β) :
      0 < (ChannelCoding.pmfToMeasure q).real {p}

      If every qStar p > 0, then (pmfToMeasure qStar).real {p} > 0.

      Used by

        Ambient setup from a feasible joint pmf #

        The remaining setup builds the i.i.d. ambient (μ, Xs, Ys) consumed by the witness form. We use iidAmbientJointMeasure (pmfToMeasure qStar) with the coordinate projections iidXs, iidYs.

        noncomputable def

        InformationTheory.Shannon.rdAmbient

        source
        {α : Type u_1} {β : Type u_2} [Fintype α] [MeasurableSpace α] [Fintype β] [MeasurableSpace β] (qStar : α × β → ℝ) :
        MeasureTheory.Measure (ℕ → α × β)

        Ambient i.i.d. measure built from qStar lifted to a measure.

        Equations
        Instances For
          Used by
            theorem

            InformationTheory.Shannon.rdAmbient_isProbabilityMeasure

            source
            {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hq : qStar ∈ stdSimplex ℝ (α × β)) :
            MeasureTheory.IsProbabilityMeasure (rdAmbient qStar)
            Used by
              theorem

              InformationTheory.Shannon.rdAmbient_map_iidXs

              source
              {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hq : qStar ∈ stdSimplex ℝ (α × β)) :
              MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar) = MeasureTheory.Measure.map Prod.fst (ChannelCoding.pmfToMeasure qStar)

              The iidXs 0 marginal of rdAmbient qStar is (pmfToMeasure qStar).map Prod.fst.

              Used by
                theorem

                InformationTheory.Shannon.rdAmbient_map_iidYs

                source
                {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hq : qStar ∈ stdSimplex ℝ (α × β)) :
                MeasureTheory.Measure.map (ChannelCoding.iidYs 0) (rdAmbient qStar) = MeasureTheory.Measure.map Prod.snd (ChannelCoding.pmfToMeasure qStar)

                The iidYs 0 marginal of rdAmbient qStar is (pmfToMeasure qStar).map Prod.snd.

                Used by
                  theorem

                  InformationTheory.Shannon.rdAmbient_map_jointSequence

                  source
                  {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hq : qStar ∈ stdSimplex ℝ (α × β)) :
                  MeasureTheory.Measure.map (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs 0) (rdAmbient qStar) = ChannelCoding.pmfToMeasure qStar

                  The joint sequence marginal of rdAmbient qStar is pmfToMeasure qStar.

                  Used by
                    theorem

                    InformationTheory.Shannon.rdAmbient_iidXs_isProbabilityMeasure

                    source
                    {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hq : qStar ∈ stdSimplex ℝ (α × β)) :
                    MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (ChannelCoding.iidXs 0) (rdAmbient qStar))
                    Used by
                      theorem

                      InformationTheory.Shannon.rdAmbient_iidYs_isProbabilityMeasure

                      source
                      {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hq : qStar ∈ stdSimplex ℝ (α × β)) :
                      MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map (ChannelCoding.iidYs 0) (rdAmbient qStar))
                      Used by

                        Expected distortion bridge #

                        expectedJointDistortion (rdAmbient qStar) (iidXs 0) (iidYs 0) d = expectedDistortionPmf d qStar.

                        theorem

                        InformationTheory.Shannon.expectedJointDistortion_rdAmbient

                        source
                        {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hqStar_simp : qStar ∈ stdSimplex ℝ (α × β)) (d : DistortionFn α β) :
                        expectedJointDistortion (rdAmbient qStar) (ChannelCoding.iidXs 0) (ChannelCoding.iidYs 0) d = expectedDistortionPmf d qStar

                        The expected joint distortion under rdAmbient qStar equals the pmf-form expectedDistortionPmf d qStar. Proved by unfolding the integral over the i.i.d. ambient, pushing forward to pmfToMeasure qStar, and decomposing the dirac sum.

                        Used by