InformationTheory

InformationTheory.Shannon.MultipleAccess.Achievability.RandomCoding

source

Imports 3

Multiple access channel — two-codebook random-coding average and achievability #

The random-coding argument on top of the codebook plumbing (Cover–Thomas): the per-event codebook-average swaps, the arithmetic aggregating them, the two-codebook average bound, the random → deterministic pigeonhole, and the achievability headline mac_achievability.

Two-codebook averaging: per-event swaps #

theorem

InformationTheory.Shannon.MAC.mac_random_codebook_E0_swap

source
{α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [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] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) {M₁ M₂ n : ℕ} {ε : ℝ} (m₁ : Fin M₁) (m₂ : Fin M₂) :
∑ c₁ : MACCodebook M₁ n α₁, ∑ c₂ : MACCodebook M₂ n α₂, (ChannelCoding.codebookMeasure p₁ M₁ n).real {c₁} * (ChannelCoding.codebookMeasure p₂ M₂ n).real {c₂} * (MeasureTheory.Measure.pi fun (i : Fin n) => W (c₁ m₁ i, c₂ m₂ i)).real {y : Fin n → β | (c₁ m₁, c₂ m₂, y) ∉ macJointlyTypicalSet (macAmbientMeasure p₁ p₂ W) macX1s macX2s macYs n ε} ≤ (macAmbientMeasure p₁ p₂ W).real {ω : ℕ → α₁ × α₂ × β | (jointRV macX1s n ω, jointRV macX2s n ω, jointRV macYs n ω) ∉ macJointlyTypicalSet (macAmbientMeasure p₁ p₂ W) macX1s macX2s macYs n ε}

Codebook-average swap for the correct-pair atypicality event E0: the two-codebook average of the probability that the transmitted triple (c₁ m₁, c₂ m₂, y) fails to be jointly typical is bounded by the ambient atypicality mass, which the AEP sends to 0.

Used by
    theorem

    InformationTheory.Shannon.MAC.mac_random_codebook_E1_swap

    source
    {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [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] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) {M₁ M₂ n : ℕ} {ε : ℝ} (hε : 0 < ε) (m₁ m₁' : Fin M₁) (m₂ : Fin M₂) (hne : m₁ ≠ m₁') :
    ∑ c₁ : MACCodebook M₁ n α₁, ∑ c₂ : MACCodebook M₂ n α₂, (ChannelCoding.codebookMeasure p₁ M₁ n).real {c₁} * (ChannelCoding.codebookMeasure p₂ M₂ n).real {c₂} * (MeasureTheory.Measure.pi fun (i : Fin n) => W (c₁ m₁ i, c₂ m₂ i)).real {y : Fin n → β | (c₁ m₁', c₂ m₂, y) ∈ macJointlyTypicalSet (macAmbientMeasure p₁ p₂ W) macX1s macX2s macYs n ε} ≤ Real.exp (↑n * (-macInfo₁ p₁ p₂ W + 3 * ε))

    Codebook-average swap for the user-1 alias event E1: the two-codebook average of the event that a wrong user-1 codeword (m₁' ≠ m₁, user 2 correct) is jointly typical with the output is bounded by exp(n·(−I(X₁;(X₂,Y)) + 3ε)).

    Used by
      theorem

      InformationTheory.Shannon.MAC.mac_random_codebook_E2_swap

      source
      {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [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] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) {M₁ M₂ n : ℕ} {ε : ℝ} (hε : 0 < ε) (m₁ : Fin M₁) (m₂ m₂' : Fin M₂) (hne : m₂ ≠ m₂') :
      ∑ c₁ : MACCodebook M₁ n α₁, ∑ c₂ : MACCodebook M₂ n α₂, (ChannelCoding.codebookMeasure p₁ M₁ n).real {c₁} * (ChannelCoding.codebookMeasure p₂ M₂ n).real {c₂} * (MeasureTheory.Measure.pi fun (i : Fin n) => W (c₁ m₁ i, c₂ m₂ i)).real {y : Fin n → β | (c₁ m₁, c₂ m₂', y) ∈ macJointlyTypicalSet (macAmbientMeasure p₁ p₂ W) macX1s macX2s macYs n ε} ≤ Real.exp (↑n * (-macInfo₂ p₁ p₂ W + 3 * ε))

      Codebook-average swap for the user-2 alias event E2: the two-codebook average of the event that a wrong user-2 codeword (m₂' ≠ m₂, user 1 correct) is jointly typical with the output is bounded by exp(n·(−I(X₂;(X₁,Y)) + 3ε)).

      Used by
        theorem

        InformationTheory.Shannon.MAC.mac_random_codebook_E3_swap

        source
        {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [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] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) {M₁ M₂ n : ℕ} {ε : ℝ} (hε : 0 < ε) (m₁ m₁' : Fin M₁) (m₂ m₂' : Fin M₂) (hne₁ : m₁ ≠ m₁') (hne₂ : m₂ ≠ m₂') :
        ∑ c₁ : MACCodebook M₁ n α₁, ∑ c₂ : MACCodebook M₂ n α₂, (ChannelCoding.codebookMeasure p₁ M₁ n).real {c₁} * (ChannelCoding.codebookMeasure p₂ M₂ n).real {c₂} * (MeasureTheory.Measure.pi fun (i : Fin n) => W (c₁ m₁ i, c₂ m₂ i)).real {y : Fin n → β | (c₁ m₁', c₂ m₂', y) ∈ macJointlyTypicalSet (macAmbientMeasure p₁ p₂ W) macX1s macX2s macYs n ε} ≤ Real.exp (↑n * (-macInfoBoth p₁ p₂ W + 3 * ε))

        Codebook-average swap for the both-wrong alias event E3: the two-codebook average of the event that a pair of wrong codewords (m₁' ≠ m₁ and m₂' ≠ m₂) is jointly typical with the output is bounded by exp(n·(−I((X₁,X₂);Y) + 3ε)).

        Used by

          Two-codebook averaging: arithmetic #

          theorem

          InformationTheory.Shannon.MAC.mac_averageErrorProb_toReal_eq

          source
          {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} (c : MACCode M₁ M₂ n α₁ α₂ β) (W : MACChannel α₁ α₂ β) (hM : 0 < M₁ * M₂) (h_ne_top : ∀ (m : Fin M₁ × Fin M₂), c.errorProbAt W m ≠ ⊤) :
          (c.averageErrorProb W).toReal = (↑(M₁ * M₂))⁻¹ * ∑ m : Fin M₁ × Fin M₂, (c.errorProbAt W m).toReal

          (averageErrorProb).toReal = (1/(M₁·M₂)) · ∑ (errorProbAt).toReal.

          Used by
            theorem

            InformationTheory.Shannon.MAC.mac_errorProbAt_ne_top

            source
            {Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] {M₁ M₂ n : ℕ} (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) (ε : ℝ) (c₁ : MACCodebook M₁ n α₁) (c₂ : MACCodebook M₂ n α₂) (m : Fin M₁ × Fin M₂) :
            (macCodebookToCode μ X1s X2s Ys hM₁ hM₂ ε c₁ c₂).errorProbAt W m ≠ ⊤

            Each MAC per-pair error probability is finite.

            Used by
              theorem

              InformationTheory.Shannon.MAC.mac_sum_weighted_quad_decomp

              source
              {ι₁ : Type u_5} {ι₂ : Type u_6} [Fintype ι₁] [DecidableEq ι₁] [Fintype ι₂] [DecidableEq ι₂] {M₁ M₂ : ℕ} (w₁ : ι₁ → ℝ) (w₂ : ι₂ → ℝ) (a : ι₁ → ι₂ → Fin M₁ → Fin M₂ → ℝ) (b1 : ι₁ → ι₂ → Fin M₁ → Fin M₂ → Fin M₁ → ℝ) (b2 : ι₁ → ι₂ → Fin M₁ → Fin M₂ → Fin M₂ → ℝ) (b3 : ι₁ → ι₂ → Fin M₁ → Fin M₂ → Fin M₁ × Fin M₂ → ℝ) (Minv : ℝ) :
              ∑ c₁ : ι₁, ∑ c₂ : ι₂, w₁ c₁ * w₂ c₂ * (Minv * ∑ m₁ : Fin M₁, ∑ m₂ : Fin M₂, (a c₁ c₂ m₁ m₂ + ∑ m₁' ∈ Finset.univ.erase m₁, b1 c₁ c₂ m₁ m₂ m₁' + ∑ m₂' ∈ Finset.univ.erase m₂, b2 c₁ c₂ m₁ m₂ m₂' + ∑ p ∈ Finset.univ.erase m₁ ×ˢ Finset.univ.erase m₂, b3 c₁ c₂ m₁ m₂ p)) = Minv * ∑ m₁ : Fin M₁, ∑ m₂ : Fin M₂, (∑ c₁ : ι₁, ∑ c₂ : ι₂, w₁ c₁ * w₂ c₂ * a c₁ c₂ m₁ m₂ + ∑ m₁' ∈ Finset.univ.erase m₁, ∑ c₁ : ι₁, ∑ c₂ : ι₂, w₁ c₁ * w₂ c₂ * b1 c₁ c₂ m₁ m₂ m₁' + ∑ m₂' ∈ Finset.univ.erase m₂, ∑ c₁ : ι₁, ∑ c₂ : ι₂, w₁ c₁ * w₂ c₂ * b2 c₁ c₂ m₁ m₂ m₂' + ∑ p ∈ Finset.univ.erase m₁ ×ˢ Finset.univ.erase m₂, ∑ c₁ : ι₁, ∑ c₂ : ι₂, w₁ c₁ * w₂ c₂ * b3 c₁ c₂ m₁ m₂ p)

              Linearity decomposition of the product-codebook expectation into the four error-event sums (E0 diagonal + the three alias families), with the codebook-weight average swapped to the inside of each term.

              Used by
                theorem

                InformationTheory.Shannon.MAC.mac_quad_aggregate

                source
                {M₁ M₂ : ℕ} (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) (A e1 e2 e3 : ℝ) (d : Fin M₁ → Fin M₂ → ℝ) (b1 : Fin M₁ → Fin M₂ → Fin M₁ → ℝ) (b2 : Fin M₁ → Fin M₂ → Fin M₂ → ℝ) (b3 : Fin M₁ → Fin M₂ → Fin M₁ × Fin M₂ → ℝ) (Minv : ℝ) (hMinv : 0 ≤ Minv) (hMinvM : Minv * ↑(M₁ * M₂) = 1) (hd : ∀ (m₁ : Fin M₁) (m₂ : Fin M₂), d m₁ m₂ ≤ A) (hb1 : ∀ (m₁ : Fin M₁) (m₂ : Fin M₂), ∀ m₁' ∈ Finset.univ.erase m₁, b1 m₁ m₂ m₁' ≤ e1) (hb2 : ∀ (m₁ : Fin M₁) (m₂ m₂' : Fin M₂), m₂' ∈ Finset.univ.erase m₂ → b2 m₁ m₂ m₂' ≤ e2) (hb3 : ∀ (m₁ : Fin M₁) (m₂ : Fin M₂), ∀ p ∈ Finset.univ.erase m₁ ×ˢ Finset.univ.erase m₂, b3 m₁ m₂ p ≤ e3) (he1 : 0 ≤ e1) (he2 : 0 ≤ e2) (he3 : 0 ≤ e3) :
                Minv * ∑ m₁ : Fin M₁, ∑ m₂ : Fin M₂, (d m₁ m₂ + ∑ m₁' ∈ Finset.univ.erase m₁, b1 m₁ m₂ m₁' + ∑ m₂' ∈ Finset.univ.erase m₂, b2 m₁ m₂ m₂' + ∑ p ∈ Finset.univ.erase m₁ ×ˢ Finset.univ.erase m₂, b3 m₁ m₂ p) ≤ A + (↑M₁ - 1) * e1 + (↑M₂ - 1) * e2 + (↑M₁ - 1) * (↑M₂ - 1) * e3

                Per-pair aggregation of the four uniform bounds into the closed-form average bound.

                Used by

                  Two-codebook averaging #

                  theorem

                  InformationTheory.Shannon.MAC.mac_random_codebook_average_le

                  source
                  {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) {M₁ M₂ n : ℕ} (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) {ε : ℝ} (hε : 0 < ε) :
                  ∑ c₁ : MACCodebook M₁ n α₁, ∑ c₂ : MACCodebook M₂ n α₂, (ChannelCoding.codebookMeasure p₁ M₁ n).real {c₁} * (ChannelCoding.codebookMeasure p₂ M₂ n).real {c₂} * ((macCodebookToCode (macAmbientMeasure p₁ p₂ W) macX1s macX2s macYs hM₁ hM₂ ε c₁ c₂).averageErrorProb W).toReal ≤ (macAmbientMeasure p₁ p₂ W).real {ω : ℕ → α₁ × α₂ × β | (jointRV macX1s n ω, jointRV macX2s n ω, jointRV macYs n ω) ∉ macJointlyTypicalSet (macAmbientMeasure p₁ p₂ W) macX1s macX2s macYs n ε} + (↑M₁ - 1) * Real.exp (↑n * (-macInfo₁ p₁ p₂ W + 3 * ε)) + (↑M₂ - 1) * Real.exp (↑n * (-macInfo₂ p₁ p₂ W + 3 * ε)) + (↑M₁ - 1) * (↑M₂ - 1) * Real.exp (↑n * (-macInfoBoth p₁ p₂ W + 3 * ε))

                  Two-codebook random-coding average bound: for the i.i.d. MAC ambient measure macAmbientMeasure p₁ p₂ W, averaging the per-pair error probability of the joint-typical pair decoder over the product of the two codebook laws is bounded by the four-event sum: the correct-pair atypicality probability E0, plus the three exponential alias terms E1/E2/E3 controlled by the independent-pair bounds macJTS_indep_prob_le_X1/_X2/_both.

                  This is the two-codebook generalization of the single-user random_codebook_average_le, assembled from the four per-event swaps (mac_random_codebook_E0_swap/_E1_swap/_E2_swap/_E3_swap), the four-event linearity decomposition (mac_sum_weighted_quad_decomp), and the per-pair aggregation (mac_quad_aggregate). @audit:ok

                  Used by

                    Random → deterministic (two-codebook pigeonhole) #

                    theorem

                    InformationTheory.Shannon.MAC.mac_exists_codebook_le_avg

                    source
                    {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [MeasurableSpace β] {Ω : Type u_5} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] {M₁ M₂ n : ℕ} (hM₁ : 0 < M₁) (hM₂ : 0 < M₂) {ε : ℝ} (B : ℝ) (h_avg : ∑ c₁ : MACCodebook M₁ n α₁, ∑ c₂ : MACCodebook M₂ n α₂, (ChannelCoding.codebookMeasure p₁ M₁ n).real {c₁} * (ChannelCoding.codebookMeasure p₂ M₂ n).real {c₂} * ((macCodebookToCode μ X1s X2s Ys hM₁ hM₂ ε c₁ c₂).averageErrorProb W).toReal ≤ B) :
                    ∃ (c₁ : MACCodebook M₁ n α₁) (c₂ : MACCodebook M₂ n α₂), ((macCodebookToCode μ X1s X2s Ys hM₁ hM₂ ε c₁ c₂).averageErrorProb W).toReal ≤ B

                    Pigeonhole over the product codebook law: if the two-codebook expectation is ≤ B, some deterministic codebook pair achieves averageErrorProb ≤ B. @audit:ok

                    Used by
                      theorem

                      InformationTheory.Shannon.MAC.mac_E3_lt_of_rate

                      source
                      {Iboth R₁ R₂ ε ε' : ℝ} (hgap : 0 < Iboth - (R₁ + R₂) - 3 * ε) (hε' : 0 < ε') :
                      ∃ (N : ℕ), ∀ n ≥ N, (↑⌈Real.exp (↑n * R₁)⌉₊ - 1) * (↑⌈Real.exp (↑n * R₂)⌉₊ - 1) * Real.exp (↑n * (-Iboth + 3 * ε)) < ε'

                      Closed-form N for the two-user (E3) "both indices wrong" term: with the AEP gap Iboth − (R₁ + R₂) − 3ε > 0, the product (⌈exp(nR₁)⌉−1)(⌈exp(nR₂)⌉−1) of the two codebook sizes times exp(n(−Iboth+3ε)) falls below any tolerance for large n. @audit:ok

                      Used by

                        Headline #

                        theorem

                        InformationTheory.Shannon.MAC.mac_achievability

                        source
                        {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (p₁ : MeasureTheory.Measure α₁) [MeasureTheory.IsProbabilityMeasure p₁] (p₂ : MeasureTheory.Measure α₂) [MeasureTheory.IsProbabilityMeasure p₂] (W : MACChannel α₁ α₂ β) [ProbabilityTheory.IsMarkovKernel W] (hp₁ : ∀ (a : α₁), 0 < p₁.real {a}) (hp₂ : ∀ (a : α₂), 0 < p₂.real {a}) (hW : ∀ (a : α₁ × α₂) (b : β), 0 < (W a).real {b}) {R₁ R₂ : ℝ} (_hR₁ : 0 < R₁) (_hR₂ : 0 < R₂) (hR₁lt : R₁ < macInfo₁ p₁ p₂ W) (hR₂lt : R₂ < macInfo₂ p₁ p₂ W) (hRsum : R₁ + R₂ < macInfoBoth p₁ p₂ W) {ε' : ℝ} (hε' : 0 < ε') :
                        ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M₁ : ℕ) (M₂ : ℕ) (_ : ⌈Real.exp (↑n * R₁)⌉₊ ≤ M₁) (_ : ⌈Real.exp (↑n * R₂)⌉₊ ≤ M₂) (c : MACCode M₁ M₂ n α₁ α₂ β), (c.averageErrorProb W).toReal < ε'

                        Achievability of the MAC corner-point region (Cover–Thomas): for an independent product input p₁ ⊗ p₂ with full-support marginals and a full-support MAC channel W, any rate pair (R₁, R₂) strictly inside the corner-point region R₁ < I(X₁; (X₂, Y)), R₂ < I(X₂; (X₁, Y)), R₁ + R₂ < I((X₁, X₂); Y) is achievable: for every target error ε' > 0 there is N such that for all n ≥ N there is a length-n two-user code with at least exp(n R₁) / exp(n R₂) messages per user whose average error probability is < ε'. @audit:ok

                        Used by