InformationTheory

InformationTheory.Shannon.RateDistortion.AchievabilityGeneralSource

source

Imports 2

Rate-distortion achievability — general (arbitrary) source #

The unconditional operational achievability theorem rate_distortion_achievability_operational carries a full-support regularity precondition hP_supp : ∀ a, 0 < P_X a. This file removes it: the general version rate_distortion_achievability_operational_general holds for any source pmf P_X ∈ stdSimplex ℝ α.

Approach #

Restrict to the support subtype α' := {a // 0 < P_X a}, apply the full-support theorem there, then lift the resulting lossy code back to the whole alphabet.

  • A feasible joint pmf q ∈ RDConstraint P_X d D vanishes off the support (marginalFst q = P_X with q ≥ 0 forces q (a, b) = 0 when P_X a = 0). Hence the restriction/padding maps between joint pmfs on α × β and α' × β are mutually inverse on feasible sets and preserve mutualInfoPmf, expectedDistortionPmf, and marginalFst (negMulLog 0 = 0).
  • Therefore rateDistortionFunctionPmf agrees on α and α', the hypotheses transport, and the full-support theorem produces a code c' on α'.
  • A retraction r : α → α' (identity on the support, a fixed default off it) lifts c' to a code on α. The source measure never charges the off-support symbols, so the expected block distortion is unchanged.

Support subtype, restriction, and padding #

noncomputable abbrev

InformationTheory.Shannon.rdSupportPmf

source
@[reducible, inline]
{α : Type u_1} (P_X : α → ℝ) :
{ a : α // 0 < P_X a } → ℝ

Source pmf restricted to the support subtype.

Equations
Instances For
    Used by
      noncomputable abbrev

      InformationTheory.Shannon.rdSupportDist

      source
      @[reducible, inline]
      {α : Type u_1} {β : Type u_2} (P_X : α → ℝ) (d : DistortionFn α β) :
      DistortionFn { a : α // 0 < P_X a } β

      Distortion function restricted to the support subtype.

      Equations
      Instances For
        Used by
          noncomputable def

          InformationTheory.Shannon.rdRestrict

          source
          {α : Type u_1} {β : Type u_2} (P_X : α → ℝ) (q : α × β → ℝ) :
          { a : α // 0 < P_X a } × β → ℝ

          Restrict a joint pmf on α × β to the support subtype α' × β.

          Equations
          Instances For
            Used by
              noncomputable def

              InformationTheory.Shannon.rdPad

              source
              {α : Type u_1} {β : Type u_2} (P_X : α → ℝ) (q' : { a : α // 0 < P_X a } × β → ℝ) :
              α × β → ℝ

              Pad a joint pmf on α' × β back to α × β by zero off the support.

              Equations
              Instances For
                Used by
                  noncomputable def

                  InformationTheory.Shannon.rdRetract

                  source
                  {α : Type u_1} (P_X : α → ℝ) (a₀ : { a : α // 0 < P_X a }) :
                  α → { a : α // 0 < P_X a }

                  Retraction of the whole alphabet onto the support subtype: the identity on the support and a fixed default off it.

                  Equations
                  Instances For
                    Used by

                      G0: support-zero #

                      theorem

                      InformationTheory.Shannon.rd_support_row_zero

                      source
                      {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] {q : α × β → ℝ} (hq : q ∈ stdSimplex ℝ (α × β)) {P_X : α → ℝ} (hmarg : marginalFst q = P_X) {a : α} (ha : ¬0 < P_X a) (b : β) :
                      q (a, b) = 0

                      A feasible joint pmf vanishes on rows outside the source support.

                      Used by
                        theorem

                        InformationTheory.Shannon.rd_support_nonempty

                        source
                        {α : Type u_1} [MeasurableSpace α] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) :
                        ∃ (a : α), 0 < P_X a

                        There is a symbol in the support of any source pmf.

                        Used by

                          G1: finite-sum transfer between α and the support subtype #

                          theorem

                          InformationTheory.Shannon.rd_sum_support_transfer

                          source
                          {α : Type u_1} [MeasurableSpace α] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] (P_X F : α → ℝ) (hF : ∀ (a : α), ¬0 < P_X a → F a = 0) :
                          ∑ a : α, F a = ∑ a : { a : α // 0 < P_X a }, F ↑a

                          Sum transfer: a function vanishing off the support has equal sums over α and over the support subtype.

                          Used by
                            theorem

                            InformationTheory.Shannon.rd_sum_prod_support_transfer

                            source
                            {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (G : α × β → ℝ) (hG : ∀ (a : α) (b : β), ¬0 < P_X a → G (a, b) = 0) :
                            ∑ p : α × β, G p = ∑ p : { a : α // 0 < P_X a } × β, G (↑p.1, p.2)

                            Product sum transfer: a function vanishing on off-support rows has equal sums over α × β and over α' × β.

                            Used by
                              theorem

                              InformationTheory.Shannon.rdRestrict_pad

                              source
                              {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (q' : { a : α // 0 < P_X a } × β → ℝ) :
                              rdRestrict P_X (rdPad P_X q') = q'

                              Restriction then padding is the identity on feasible pmfs.

                              Used by
                                theorem

                                InformationTheory.Shannon.marginalFst_rdRestrict

                                source
                                {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (q : α × β → ℝ) (a' : { a : α // 0 < P_X a }) :
                                marginalFst (rdRestrict P_X q) a' = marginalFst q ↑a'

                                The first marginal of a restriction is the restriction of the first marginal.

                                Used by
                                  theorem

                                  InformationTheory.Shannon.marginalSnd_rdRestrict

                                  source
                                  {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) {q : α × β → ℝ} (hq_supp : ∀ (a : α) (b : β), ¬0 < P_X a → q (a, b) = 0) (b : β) :
                                  marginalSnd (rdRestrict P_X q) b = marginalSnd q b

                                  The second marginal is preserved under restriction of a support-zero pmf.

                                  Used by
                                    theorem

                                    InformationTheory.Shannon.mutualInfoPmf_eq_restrict

                                    source
                                    {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) {q : α × β → ℝ} (hq_supp : ∀ (a : α) (b : β), ¬0 < P_X a → q (a, b) = 0) :
                                    mutualInfoPmf q = mutualInfoPmf (rdRestrict P_X q)

                                    Mutual information is preserved by restriction of a support-zero pmf.

                                    Used by
                                      theorem

                                      InformationTheory.Shannon.expectedDistortionPmf_eq_restrict

                                      source
                                      {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (d : DistortionFn α β) {q : α × β → ℝ} (hq_supp : ∀ (a : α) (b : β), ¬0 < P_X a → q (a, b) = 0) :
                                      expectedDistortionPmf d q = expectedDistortionPmf (rdSupportDist P_X d) (rdRestrict P_X q)

                                      Expected distortion is preserved by restriction of a support-zero pmf.

                                      Used by

                                        Membership transport #

                                        theorem

                                        InformationTheory.Shannon.rdPad_support_zero

                                        source
                                        {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (q' : { a : α // 0 < P_X a } × β → ℝ) (a : α) (b : β) (ha : ¬0 < P_X a) :
                                        rdPad P_X q' (a, b) = 0

                                        Padding is support-zero by construction.

                                        Used by
                                          theorem

                                          InformationTheory.Shannon.rdRestrict_mem_stdSimplex

                                          source
                                          {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) {q : α × β → ℝ} (hq : q ∈ stdSimplex ℝ (α × β)) (hq_supp : ∀ (a : α) (b : β), ¬0 < P_X a → q (a, b) = 0) :
                                          rdRestrict P_X q ∈ stdSimplex ℝ ({ a : α // 0 < P_X a } × β)

                                          Restriction lands in the simplex.

                                          Used by
                                            theorem

                                            InformationTheory.Shannon.rdPad_mem_stdSimplex

                                            source
                                            {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) {q' : { a : α // 0 < P_X a } × β → ℝ} (hq' : q' ∈ stdSimplex ℝ ({ a : α // 0 < P_X a } × β)) :
                                            rdPad P_X q' ∈ stdSimplex ℝ (α × β)

                                            Padding lands in the simplex.

                                            Used by
                                              theorem

                                              InformationTheory.Shannon.marginalFst_rdRestrict_eq

                                              source
                                              {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) {q : α × β → ℝ} (hmarg : marginalFst q = P_X) :
                                              marginalFst (rdRestrict P_X q) = rdSupportPmf P_X

                                              The first marginal of a restriction equals the restricted source pmf.

                                              Used by
                                                theorem

                                                InformationTheory.Shannon.marginalFst_rdPad_eq

                                                source
                                                {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) {q' : { a : α // 0 < P_X a } × β → ℝ} (hmarg' : marginalFst q' = rdSupportPmf P_X) :
                                                marginalFst (rdPad P_X q') = P_X

                                                The first marginal of a padding equals the original source pmf.

                                                Used by
                                                  theorem

                                                  InformationTheory.Shannon.rdSupportPmf_mem_stdSimplex

                                                  source
                                                  {α : Type u_1} [MeasurableSpace α] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) :
                                                  rdSupportPmf P_X ∈ stdSimplex ℝ { a : α // 0 < P_X a }

                                                  The restricted source pmf lies in the simplex of the support subtype.

                                                  Used by

                                                    G2: rate-distortion function invariance #

                                                    theorem

                                                    InformationTheory.Shannon.rdRestrict_mem_constraint

                                                    source
                                                    {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (d : DistortionFn α β) {D : ℝ} {q : α × β → ℝ} (hq : q ∈ RDConstraint P_X d D) :
                                                    rdRestrict P_X q ∈ RDConstraint (rdSupportPmf P_X) (rdSupportDist P_X d) D

                                                    Membership transports along restriction.

                                                    Used by
                                                      theorem

                                                      InformationTheory.Shannon.rdPad_mem_constraint

                                                      source
                                                      {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) (d : DistortionFn α β) {D : ℝ} {q' : { a : α // 0 < P_X a } × β → ℝ} (hq' : q' ∈ RDConstraint (rdSupportPmf P_X) (rdSupportDist P_X d) D) :
                                                      rdPad P_X q' ∈ RDConstraint P_X d D

                                                      Membership transports along padding.

                                                      Used by
                                                        theorem

                                                        InformationTheory.Shannon.rd_function_eq

                                                        source
                                                        {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) (d : DistortionFn α β) (D : ℝ) :
                                                        rateDistortionFunctionPmf P_X d D = rateDistortionFunctionPmf (rdSupportPmf P_X) (rdSupportDist P_X d) D

                                                        The pmf-direct rate-distortion function is unchanged by support restriction.

                                                        Used by

                                                          G4: source measure charges only the support #

                                                          theorem

                                                          InformationTheory.Shannon.pmfToMeasure_support_compl_null

                                                          source
                                                          {α : Type u_1} [MeasurableSpace α] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) :
                                                          (ChannelCoding.pmfToMeasure P_X) {a : α | ¬0 < P_X a} = 0

                                                          The source measure gives zero mass to the off-support symbols.

                                                          Used by
                                                            theorem

                                                            InformationTheory.Shannon.pmfToMeasure_map_retract

                                                            source
                                                            {α : Type u_1} [MeasurableSpace α] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) (a₀ : { a : α // 0 < P_X a }) :
                                                            MeasureTheory.Measure.map (rdRetract P_X a₀) (ChannelCoding.pmfToMeasure P_X) = ChannelCoding.pmfToMeasure (rdSupportPmf P_X)

                                                            Pushing the source measure through the support retraction yields the restricted source pmf.

                                                            Used by
                                                              theorem

                                                              InformationTheory.Shannon.expectedBlockDistortion_lift_le

                                                              source
                                                              {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) (d : DistortionFn α β) {M n : ℕ} (c' : LossyCode M n { a : α // 0 < P_X a } β) (a₀ : { a : α // 0 < P_X a }) {v : ℝ} (hc' : c'.expectedBlockDistortion (ChannelCoding.pmfToMeasure (rdSupportPmf P_X)) (rdSupportDist P_X d) ≤ v) :
                                                              { encoder := fun (x : Fin n → α) => c'.encoder fun (i : Fin n) => rdRetract P_X a₀ (x i), decoder := c'.decoder }.expectedBlockDistortion (ChannelCoding.pmfToMeasure P_X) d ≤ v

                                                              Lift the expected block distortion bound from the support subtype to the whole alphabet.

                                                              Used by

                                                                Wrapper: general-source operational achievability #

                                                                theorem

                                                                InformationTheory.Shannon.rate_distortion_achievability_operational_general

                                                                source
                                                                {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (P_X : α → ℝ) (hP_pmf : P_X ∈ stdSimplex ℝ α) (d : DistortionFn α β) {D : ℝ} (h_ne : (RDConstraint P_X d D).Nonempty) {R : ℝ} (hR : rateDistortionFunctionPmf P_X d D < R) {ε : ℝ} (hε : 0 < ε) :
                                                                ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (_ : ↑M ≤ Real.exp (↑n * R) + 1) (c : LossyCode M n α β), c.expectedBlockDistortion (ChannelCoding.pmfToMeasure P_X) d ≤ D + ε

                                                                Rate-distortion theorem (achievability, general source).

                                                                Removes the full-support precondition from rate_distortion_achievability_operational: for any source P_X ∈ stdSimplex with a feasible constraint set and any rate R > R(D), for every ε > 0 there is a block length N such that every n ≥ N admits a rate-R lossy code whose expected block distortion is at most D + ε.

                                                                @audit:ok

                                                                Used by