InformationTheory

InformationTheory.Shannon.MultipleAccess.Reconciliation

source

Imports 9

Multiple access channel — converse/achievability reconciliation bridge #

Under the independent product input p₁ ⊗ p₂, the achievability rate quantities macInfo₁ / macInfo₂ / macInfoBoth (entropy differences, ℝ-valued) of InformationTheory.Shannon.MultipleAccess.Achievability coincide with the converse information quantities (condMutualInfo / mutualInfo, klDiv-based, ℝ≥0∞-valued) taken on the per-coordinate joint law macJointDistribution p₁ p₂ W:

  • macInfo₁ = (I(X₁; Y | X₂)) ,
  • macInfo₂ = (I(X₂; Y | X₁)) ,
  • macInfoBoth = (I((X₁, X₂); Y)) .

The crux is that the input coordinates X₁, X₂ are independent under p₁ ⊗ p₂, so the chain rule I(X₁; (X₂, Y)) = I(X₁; Y | X₂) (and its user-2 mirror) closes the gap between the achievability corner informations and the textbook conditional informations of the MAC capacity region.

Main statements #

theorem

InformationTheory.Shannon.MAC.mutualInfo_toReal_eq_entropy_form

source
{Ω : Type u_1} [MeasurableSpace Ω] {A : Type u_2} {B : Type u_3} [Fintype A] [DecidableEq A] [Nonempty A] [MeasurableSpace A] [MeasurableSingletonClass A] [Fintype B] [DecidableEq B] [Nonempty B] [MeasurableSpace B] [MeasurableSingletonClass B] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (f : Ω → A) (g : Ω → B) (hf : Measurable f) (hg : Measurable g) :
(mutualInfo μ f g).toReal = entropy μ f + entropy μ g - entropy μ fun (ω : Ω) => (f ω, g ω)

Generic entropy-form expression of the klDiv mutual information, lifting the Prod.fst/Prod.snd bridge mutualInfo_eq_entropy_add_entropy_sub_jointEntropy to an arbitrary pair of finite-alphabet random variables.

Used by
    theorem

    InformationTheory.Shannon.MAC.macJoint_mutualInfo_X1_X2_eq_zero

    source
    {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
    (mutualInfo (macJointDistribution p₁ p₂ W) Prod.fst fun (q : α₁ × α₂ × β) => q.2.1) = 0

    The two input coordinates are independent under the product input p₁ ⊗ p₂, hence their mutual information vanishes. @audit:ok

    Used by
      theorem

      InformationTheory.Shannon.MAC.macInfo₁_eq_mutualInfo_toReal

      source
      {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
      macInfo₁ p₁ p₂ W = (mutualInfo (macJointDistribution p₁ p₂ W) Prod.fst fun (q : α₁ × α₂ × β) => (q.2.1, q.2.2)).toReal

      Achievability user-1 corner information equals the joint mutual information I(X₁; (X₂, Y)) on the per-coordinate joint law.

      Used by
        theorem

        InformationTheory.Shannon.MAC.macInfo₂_eq_mutualInfo_toReal

        source
        {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
        macInfo₂ p₁ p₂ W = (mutualInfo (macJointDistribution p₁ p₂ W) (fun (q : α₁ × α₂ × β) => q.2.1) fun (q : α₁ × α₂ × β) => (q.1, q.2.2)).toReal

        Achievability user-2 corner information equals the joint mutual information I(X₂; (X₁, Y)) on the per-coordinate joint law.

        Used by
          theorem

          InformationTheory.Shannon.MAC.macJoint_mutualInfo_eq_condMutualInfo₁

          source
          {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [StandardBorelSpace α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
          (mutualInfo (macJointDistribution p₁ p₂ W) Prod.fst fun (q : α₁ × α₂ × β) => (q.2.1, q.2.2)) = condMutualInfo (macJointDistribution p₁ p₂ W) Prod.fst (fun (q : α₁ × α₂ × β) => q.2.2) fun (q : α₁ × α₂ × β) => q.2.1

          Chain rule under input independence (user 1): I(X₁; (X₂, Y)) = I(X₁; Y | X₂).

          Used by
            theorem

            InformationTheory.Shannon.MAC.macJoint_mutualInfo_eq_condMutualInfo₂

            source
            {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [StandardBorelSpace α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
            (mutualInfo (macJointDistribution p₁ p₂ W) (fun (q : α₁ × α₂ × β) => q.2.1) fun (q : α₁ × α₂ × β) => (q.1, q.2.2)) = condMutualInfo (macJointDistribution p₁ p₂ W) (fun (q : α₁ × α₂ × β) => q.2.1) (fun (q : α₁ × α₂ × β) => q.2.2) Prod.fst

            Chain rule under input independence (user 2): I(X₂; (X₁, Y)) = I(X₂; Y | X₁).

            Used by
              theorem

              InformationTheory.Shannon.MAC.macInfo₁_eq_condMutualInfo_toReal

              source
              {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [StandardBorelSpace α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
              macInfo₁ p₁ p₂ W = (condMutualInfo (macJointDistribution p₁ p₂ W) Prod.fst (fun (q : α₁ × α₂ × β) => q.2.2) fun (q : α₁ × α₂ × β) => q.2.1).toReal

              The user-1 corner informations of the two MAC descriptions agree: under the independent product input p₁ ⊗ p₂, the achievability corner information macInfo₁ equals the textbook conditional mutual information I(X₁; Y | X₂) of the converse, taken on the per-coordinate joint law macJointDistribution p₁ p₂ W. @audit:ok

              Used by
                theorem

                InformationTheory.Shannon.MAC.macInfo₂_eq_condMutualInfo_toReal

                source
                {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [StandardBorelSpace α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
                macInfo₂ p₁ p₂ W = (condMutualInfo (macJointDistribution p₁ p₂ W) (fun (q : α₁ × α₂ × β) => q.2.1) (fun (q : α₁ × α₂ × β) => q.2.2) Prod.fst).toReal

                The user-2 corner informations of the two MAC descriptions agree: under the independent product input p₁ ⊗ p₂, the achievability corner information macInfo₂ equals the textbook conditional mutual information I(X₂; Y | X₁) of the converse. @audit:ok

                Used by
                  theorem

                  InformationTheory.Shannon.MAC.macInfoBoth_eq_mutualInfo_toReal

                  source
                  {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
                  macInfoBoth p₁ p₂ W = (mutualInfo (macJointDistribution p₁ p₂ W) (fun (q : α₁ × α₂ × β) => (q.1, q.2.1)) fun (q : α₁ × α₂ × β) => q.2.2).toReal

                  The sum-corner informations of the two MAC descriptions agree: the achievability sum-corner information macInfoBoth equals the joint mutual information I((X₁, X₂); Y) of the converse, taken on the per-coordinate joint law macJointDistribution p₁ p₂ W. @audit:ok

                  Used by
                    theorem

                    InformationTheory.Shannon.MAC.mac_capacity_region_reconciliation

                    source
                    {α₁ : Type u_1} {α₂ : Type u_2} {β : Type u_3} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [StandardBorelSpace α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [StandardBorelSpace α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] [StandardBorelSpace β] (R₁ R₂ : ℝ) (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] :
                    InMACCapacityRegion R₁ R₂ (macInfo₁ p₁ p₂ W) (macInfo₂ p₁ p₂ W) (macInfoBoth p₁ p₂ W) ↔ InMACCapacityRegion R₁ R₂ (condMutualInfo (macJointDistribution p₁ p₂ W) Prod.fst (fun (q : α₁ × α₂ × β) => q.2.2) fun (q : α₁ × α₂ × β) => q.2.1).toReal (condMutualInfo (macJointDistribution p₁ p₂ W) (fun (q : α₁ × α₂ × β) => q.2.1) (fun (q : α₁ × α₂ × β) => q.2.2) Prod.fst).toReal (mutualInfo (macJointDistribution p₁ p₂ W) (fun (q : α₁ × α₂ × β) => (q.1, q.2.1)) fun (q : α₁ × α₂ × β) => q.2.2).toReal

                    The achievability and converse descriptions of the MAC capacity region coincide: under the independent product input p₁ ⊗ p₂, a rate pair lies in the achievability region (with corner informations macInfo₁ / macInfo₂ / macInfoBoth) iff it lies in the converse region (with the textbook conditional/joint informations I(X₁; Y | X₂) / I(X₂; Y | X₁) / I((X₁, X₂); Y) on macJointDistribution p₁ p₂ W).

                    The equivalence is not vacuous: the left-hand macInfo₁/₂/Both (entropy-difference ℝ values) and the right-hand condMutualInfo/mutualInfo .toReal (klDiv-based) are syntactically distinct quantities, so the iff is closed only through the three corner-information equivalences above, not by a definitional P ↔ P. @audit:ok

                    Used by