InformationTheory

InformationTheory.Shannon.BroadcastChannel.Superposition.Region

source

Broadcast channel — the superposition inner bound #

Superposition coding sends a cloud center U to both receivers and a satellite X to the first one only. This file takes the union of its inner bound over the auxiliary alphabets, so that it can be compared with the outer bounds as a set.

Two unions are taken, over the same full-support indices and differing only in the constraints cutting out each member. Keeping the sum-rate constraint gives the general superposition bound, achievable over any broadcast channel; dropping it gives a superset, achievable as soon as the first receiver decodes the cloud at least as well as the second one does — which is exactly what IsBCLessNoisy asks, physical degradedness is not needed — because I(U; Y₁) ≥ I(U; Y₂) makes the omitted inequality follow from the two kept ones.

Main definitions #

Main statements #

Implementation notes #

The auxiliary alphabets range over Marton.bcAuxAlphabet, one cardinality at a time in the universe of the input alphabet. That universe is forced: IsBCLessNoisy quantifies its auxiliary variable over the universe of the input alphabet, so a member of the union has to live there for the class hypothesis to apply to it.

Nonnegativity of the satellite information #

theorem

InformationTheory.Shannon.BroadcastChannel.bcInfo₁_nonneg

source
Used by

    The three informations as (conditional) mutual informations #

    theorem

    InformationTheory.Shannon.BroadcastChannel.bcInfo₂_eq_mutualInfo_toReal

    source
    {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] {U : Type u_3} [Fintype U] [DecidableEq U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] (pU : MeasureTheory.Measure U) [MeasureTheory.IsProbabilityMeasure pU] (K : ProbabilityTheory.Kernel U α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] :
    bcInfo₂ pU K W = (mutualInfo (bcJointDistribution pU K W) (fun (q : U × α × β₁ × β₂) => q.1) fun (q : U × α × β₁ × β₂) => q.2.2.2).toReal
    Used by
      theorem

      InformationTheory.Shannon.BroadcastChannel.bcInfoJoint_eq_mutualInfo_toReal

      source
      {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] {U : Type u_3} [Fintype U] [DecidableEq U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] (pU : MeasureTheory.Measure U) [MeasureTheory.IsProbabilityMeasure pU] (K : ProbabilityTheory.Kernel U α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] :
      bcInfoJoint pU K W = (mutualInfo (bcJointDistribution pU K W) (fun (q : U × α × β₁ × β₂) => (q.1, q.2.1)) fun (q : U × α × β₁ × β₂) => q.2.2.1).toReal
      Used by
        theorem

        InformationTheory.Shannon.BroadcastChannel.bcInfo₁_eq_condMutualInfo_toReal

        source
        {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] {U : Type u_3} [Fintype U] [DecidableEq U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] (pU : MeasureTheory.Measure U) [MeasureTheory.IsProbabilityMeasure pU] (K : ProbabilityTheory.Kernel U α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] :
        bcInfo₁ pU K W = (condMutualInfo (bcJointDistribution pU K W) (fun (q : U × α × β₁ × β₂) => q.2.1) (fun (q : U × α × β₁ × β₂) => q.2.2.1) fun (q : U × α × β₁ × β₂) => q.1).toReal
        Used by

          Achievability over a less noisy channel #

          theorem

          InformationTheory.Shannon.BroadcastChannel.bc_lessNoisy_achievability

          source
          {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] {U : Type u} [Fintype U] [DecidableEq U] [Nonempty U] [MeasurableSpace U] [MeasurableSingletonClass U] (pU : MeasureTheory.Measure U) [MeasureTheory.IsProbabilityMeasure pU] (K : ProbabilityTheory.Kernel U α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hpU : ∀ (u : U), 0 < pU.real {u}) (hK : ∀ (u : U) (a : α), 0 < (K u).real {a}) (hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b}) (hln : IsBCLessNoisy W) {R₁ R₂ : } (hR₁ : 0 < R₁) (hR₂ : 0 < R₂) (hR₁lt : R₁ < bcInfo₁ pU K W) (hR₂lt : R₂ < bcInfo₂ pU K W) {ε' : } (hε' : 0 < ε') :
          ∃ (N : ), ∀ (n : ), N n∃ (M₁ : ) (M₂ : ) (_ : Real.exp (n * R₁)⌉₊ M₁) (_ : Real.exp (n * R₂)⌉₊ M₂) (c : BroadcastCode M₁ M₂ n α β₁ β₂), (c.averageErrorProb₁ W).toReal < ε' (c.averageErrorProb₂ W).toReal < ε'

          Achievability half of the superposition inner bound over a less noisy broadcast channel. The two-tier random-coding argument is shared with the degraded channel through bc_achievability_of_infoJoint_ge, which takes the rate-sum inequality I(X; Y₁ ∣ U) + I(U; Y₂) ≤ I((U, X); Y₁) as a hypothesis instead of deriving it; bc_lessNoisy_infoJoint_ge supplies it from the weaker class hypothesis. @audit:ok

          Used by

            The superposition inner bound as a region #

            noncomputable def

            InformationTheory.Shannon.BroadcastChannel.bcSuperpositionRegionNoSumRate

            source
            {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [MeasurableSpace α] [Fintype β₁] [MeasurableSpace β₁] [Fintype β₂] [MeasurableSpace β₂] (W : BCChannel α β₁ β₂) :

            The superposition inner bound of a broadcast channel: the closure of the union, over the full-support auxiliary laws on Marton.bcAuxAlphabet, of the rectangles cut out by R₁ ≤ I(X; Y₁ ∣ U) and R₂ ≤ I(U; Y₂).

            The general superposition bound also constrains the rate sum by R₁ + R₂ ≤ I((U, X); Y₁), and that constraint is dropped here. Dropping it is exact over a less noisy channel, where I(U; Y₁) ≥ I(U; Y₂) forces I(X; Y₁ ∣ U) + I(U; Y₂) ≤ I((U, X); Y₁) (bc_lessNoisy_infoJoint_ge), so the omitted inequality already follows from the two kept ones. Outside that class this set is only a superset of the superposition bound.

            The full-support indices are the ones the achievability theorem applies to, so this is the form of the union that is achievable. As for bcCapacityRegion and the outer bounds, no sign constraint is imposed: a nonpositive rate asks only for a single message. @audit:ok

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Used by
                theorem

                InformationTheory.Shannon.BroadcastChannel.bcSuperpositionRegionNoSumRate_isClosed

                source
                {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (W : BCChannel α β₁ β₂) :
                Used by
                  theorem

                  InformationTheory.Shannon.BroadcastChannel.bcSuperpositionRegionNoSumRate_subset_capacity

                  source
                  {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b}) (hln : IsBCLessNoisy W) :

                  The superposition inner bound of a less noisy broadcast channel is achievable: it is contained in the operational capacity region. @audit:ok

                  Used by

                    The superposition inner bound with the sum-rate constraint kept #

                    noncomputable def

                    InformationTheory.Shannon.BroadcastChannel.bcSuperpositionRegionSumRate

                    source
                    {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [MeasurableSpace α] [Fintype β₁] [MeasurableSpace β₁] [Fintype β₂] [MeasurableSpace β₂] (W : BCChannel α β₁ β₂) :

                    The superposition inner bound of a broadcast channel with the sum-rate constraint kept: the closure of the union, over the full-support auxiliary laws on Marton.bcAuxAlphabet, of the regions cut out by R₁ ≤ I(X; Y₁ ∣ U), R₂ ≤ I(U; Y₂) and max R₁ 0 + R₂ ≤ I((U, X); Y₁).

                    The sum constraint is written with the first rate clamped at zero because that is the form the achievability theorem takes: a nonpositive first rate asks for a single satellite codeword, so the wrong-cloud slack it costs is measured at max R₁ 0. With that shape the whole set is achievable with no comparison-class hypothesis, whereas the plain sum R₁ + R₂ would need one on the branch where the first rate is negative.

                    bcSuperpositionRegionNoSumRate drops the sum constraint, which is exact over a less noisy channel but not in general; this set is the general superposition bound and is contained in it.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Used by
                        theorem

                        InformationTheory.Shannon.BroadcastChannel.bcSuperpositionRegionSumRate_isClosed

                        source
                        {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [MeasurableSpace α] [Fintype β₁] [MeasurableSpace β₁] [Fintype β₂] [MeasurableSpace β₂] (W : BCChannel α β₁ β₂) :
                        Used by
                          theorem

                          InformationTheory.Shannon.BroadcastChannel.bcSuperpositionRegionSumRate_subset_capacity

                          source
                          {α : Type u} {β₁ : Type u_1} {β₂ : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] (hW : ∀ (a : α) (b : β₁ × β₂), 0 < (W a).real {b}) :

                          The three-constraint superposition inner bound of a broadcast channel is achievable: it is contained in the operational capacity region. No comparison between the two receivers is needed, because the region carries the sum constraint the achievability theorem asks for.

                          Used by