InformationTheory.Shannon.MultipleAccess.Converse

Imports 8

Multiple access channel — converse (outer bound) #

The converse to the MAC coding theorem (Cover–Thomas): for uniformly distributed, independent messages decoded by a joint decoder, the rate pair satisfies the three corner-point inequalities of InMACCapacityRegion.

Each of the three bounds is the message-level Fano converse, obtained from the encoder-free single-shot converse shannon_converse_single_shot by placing the conditioning message in the output slot:

user 1: log |M₁| ≤ I(M₁; (M₂, Yⁿ)) + h(Pe₁) + Pe₁ log(|M₁| − 1)
user 2: log |M₂| ≤ I(M₂; (M₁, Yⁿ)) + h(Pe₂) + Pe₂ log(|M₂| − 1)
sum: log |M₁| + log |M₂| ≤ I((M₁, M₂); Yⁿ) + h(Pe) + Pe log(|M₁·M₂| − 1)

Here I(M₁; (M₂, Yⁿ)) = I(M₁; Yⁿ | M₂) under message independence, the standard converse intermediate. Single-letterizing these bounds to the per-letter channel quantities I(X₁; Y | X₂) etc. is carried out in the second half of the file.

Main statements #

mac_converse_bound₁ / mac_converse_bound₂ / mac_converse_bound_sum — the three corner-point inequalities.
mac_converse_message_level — the packaged InMACCapacityRegion outer bound.
mac_converse — the single-letterized outer bound, whose information slots are the per-letter channel sums ∑ᵢ I(X₁ᵢ; Yᵢ | X₂ᵢ) etc.

theorem

InformationTheory.Shannon.MAC.mac_converse_bound₁

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg₁ : Ω → Fin M₁) (Msg₂ : Ω → Fin M₂) (Ys : Fin n → Ω → β) (c : MACCode M₁ M₂ n α₁ α₂ β) (hMsg₁ : Measurable Msg₁) (hMsg₂ : Measurable Msg₂) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (hMsg₁_uniform : MeasureTheory.Measure.map Msg₁ μ = (↑(Fintype.card (Fin M₁)))⁻¹ • MeasureTheory.Measure.count) (hcard₁ : 2 ≤ M₁) :

Real.log ↑M₁ ≤ (mutualInfo μ Msg₁ fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg₁ (fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₂ × (Fin n → β)) => (c.decoder p.2).1) + (MeasureFano.errorProb μ Msg₁ (fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₂ × (Fin n → β)) => (c.decoder p.2).1) * Real.log (↑M₁ - 1)

Message-level user-1 corner bound of the MAC converse: under a uniform message Msg₁, log |M₁| ≤ I(M₁; (M₂, Yⁿ)) + h(Pe₁) + Pe₁ · log(|M₁| − 1), where the user-1 error probability Pe₁ is measured against the joint decoder's first component.

Used by

theorem

InformationTheory.Shannon.MAC.mac_converse_bound₂

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg₁ : Ω → Fin M₁) (Msg₂ : Ω → Fin M₂) (Ys : Fin n → Ω → β) (c : MACCode M₁ M₂ n α₁ α₂ β) (hMsg₁ : Measurable Msg₁) (hMsg₂ : Measurable Msg₂) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (hMsg₂_uniform : MeasureTheory.Measure.map Msg₂ μ = (↑(Fintype.card (Fin M₂)))⁻¹ • MeasureTheory.Measure.count) (hcard₂ : 2 ≤ M₂) :

Real.log ↑M₂ ≤ (mutualInfo μ Msg₂ fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg₂ (fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₁ × (Fin n → β)) => (c.decoder p.2).2) + (MeasureFano.errorProb μ Msg₂ (fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₁ × (Fin n → β)) => (c.decoder p.2).2) * Real.log (↑M₂ - 1)

Message-level user-2 corner bound of the MAC converse, symmetric to mac_converse_bound₁.

Used by

theorem

InformationTheory.Shannon.MAC.mac_converse_bound_sum

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg₁ : Ω → Fin M₁) (Msg₂ : Ω → Fin M₂) (Ys : Fin n → Ω → β) (c : MACCode M₁ M₂ n α₁ α₂ β) (hMsg₁ : Measurable Msg₁) (hMsg₂ : Measurable Msg₂) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (hMsg₁₂_uniform : MeasureTheory.Measure.map (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) μ = (↑(Fintype.card (Fin M₁ × Fin M₂)))⁻¹ • MeasureTheory.Measure.count) (hcard₁ : 2 ≤ M₁) (hcard₂ : 2 ≤ M₂) :

Real.log ↑M₁ + Real.log ↑M₂ ≤ (mutualInfo μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) fun (ω : Ω) (i : Fin n) => Ys i ω).toReal + Real.binEntropy (MeasureFano.errorProb μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) (i : Fin n) => Ys i ω) c.decoder) + MeasureFano.errorProb μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) (i : Fin n) => Ys i ω) c.decoder * Real.log (↑(M₁ * M₂) - 1)

Message-level sum-rate bound of the MAC converse: treating the pair (M₁, M₂) as a single uniform message decoded jointly, log |M₁| + log |M₂| ≤ I((M₁, M₂); Yⁿ) + h(Pe) + Pe · log(|M₁·M₂| − 1).

Used by

theorem

InformationTheory.Shannon.MAC.mac_converse_message_level

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg₁ : Ω → Fin M₁) (Msg₂ : Ω → Fin M₂) (Ys : Fin n → Ω → β) (c : MACCode M₁ M₂ n α₁ α₂ β) (hMsg₁ : Measurable Msg₁) (hMsg₂ : Measurable Msg₂) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (hMsg₁_uniform : MeasureTheory.Measure.map Msg₁ μ = (↑(Fintype.card (Fin M₁)))⁻¹ • MeasureTheory.Measure.count) (hMsg₂_uniform : MeasureTheory.Measure.map Msg₂ μ = (↑(Fintype.card (Fin M₂)))⁻¹ • MeasureTheory.Measure.count) (hMsg₁₂_uniform : MeasureTheory.Measure.map (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) μ = (↑(Fintype.card (Fin M₁ × Fin M₂)))⁻¹ • MeasureTheory.Measure.count) (hcard₁ : 2 ≤ M₁) (hcard₂ : 2 ≤ M₂) :

InMACCapacityRegion (Real.log ↑M₁) (Real.log ↑M₂) ((mutualInfo μ Msg₁ fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg₁ (fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₂ × (Fin n → β)) => (c.decoder p.2).1) + (MeasureFano.errorProb μ Msg₁ (fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₂ × (Fin n → β)) => (c.decoder p.2).1) * Real.log (↑M₁ - 1)) ((mutualInfo μ Msg₂ fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg₂ (fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₁ × (Fin n → β)) => (c.decoder p.2).2) + (MeasureFano.errorProb μ Msg₂ (fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₁ × (Fin n → β)) => (c.decoder p.2).2) * Real.log (↑M₂ - 1)) ((mutualInfo μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) fun (ω : Ω) (i : Fin n) => Ys i ω).toReal + Real.binEntropy (MeasureFano.errorProb μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) (i : Fin n) => Ys i ω) c.decoder) + MeasureFano.errorProb μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) (i : Fin n) => Ys i ω) c.decoder * Real.log (↑(M₁ * M₂) - 1))

Message-level Fano outer bound for the MAC: for uniform messages decoded by a joint decoder, the rate pair (log |M₁|, log |M₂|) satisfies the three message-level Fano information bounds, packaged as InMACCapacityRegion.

The information slots are the n-letter message–output mutual informations, not the single-letter channel quantities I(X₁; Y | X₂) etc.; the single-letterized form of the converse (Cover–Thomas) is mac_converse.

Used by

Single-letterization #

The single-letterized MAC converse bridges the message-level mutual informations of mac_converse_message_level down to the single-letter channel quantities I(X₁ᵢ; Yᵢ | X₂ᵢ) etc. The analytic core is the conditional single-letterization of the block input–output mutual information; the link from the message-level mutual information to the block input mutual information uses the standard data-processing and conditioning identities under a memoryless channel.

This mirrors the single-user mutualInfo_le_sum_per_letter_of_memoryless_strong (CondEntropyMemoryless.lean) lifted to a conditional form with the other user's input X₂ⁿ sitting in the conditioner throughout.

theorem

InformationTheory.Shannon.MAC.condEntropy_pi_le_sum_condEntropy

source

{Ω : Type u_1} [MeasurableSpace Ω] {β : Type u_4} [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {n : ℕ} [Nonempty β] {γ : Type u_5} [Fintype γ] [DecidableEq γ] [Nonempty γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Zs : Fin n → Ω → γ) (Ys : Fin n → Ω → β) (hZs : ∀ (i : Fin n), Measurable (Zs i)) (hYs : ∀ (i : Fin n), Measurable (Ys i)) :

(MeasureFano.condEntropy μ (fun (ω : Ω) (j : Fin n) => Ys j ω) fun (ω : Ω) (j : Fin n) => Zs j ω) ≤ ∑ i : Fin n, MeasureFano.condEntropy μ (Ys i) (Zs i)

Conditional entropy is subadditive across a block: H(Yⁿ | Zⁿ) ≤ ∑ᵢ H(Yᵢ | Zᵢ). Holds for any inputs Zs (no memoryless assumption needed); the per-letter conditioner Zᵢ is a coarsening of the block conditioner (Zⁿ, Y^{<i}), so conditioning-reduces-entropy gives each summand bound.

Used by

theorem

InformationTheory.Shannon.MAC.condMutualInfo_singleletter_le_of_memoryless

source

(condMutualInfo μ (fun (ω : Ω) (j : Fin n) => X₁s j ω) (fun (ω : Ω) (j : Fin n) => Ys j ω) fun (ω : Ω) (j : Fin n) => X₂s j ω).toReal ≤ ∑ i : Fin n, (condMutualInfo μ (X₁s i) (Ys i) (X₂s i)).toReal

Single-letterization of the conditional mutual information: under a strong memoryless channel on the joint input (X₁ᵢ, X₂ᵢ), I(X₁ⁿ; Yⁿ | X₂ⁿ) ≤ ∑ᵢ I(X₁ᵢ; Yᵢ | X₂ᵢ) (as reals).

Used by

theorem

InformationTheory.Shannon.MAC.mac_message_le_condMI

source

(mutualInfo μ Msg₁ fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)).toReal ≤ (condMutualInfo μ (fun (ω : Ω) (j : Fin n) => c.encoder₁ (Msg₁ ω) j) (fun (ω : Ω) (j : Fin n) => Ys j ω) fun (ω : Ω) (j : Fin n) => c.encoder₂ (Msg₂ ω) j).toReal

Link from the message level to the channel level: under message independence and the block channel Markov chain (M₁, M₂) → (X₁ⁿ, X₂ⁿ) → Yⁿ, the message-level mutual information is bounded by the block input–output conditional mutual information, I(M₁; (M₂, Yⁿ)) ≤ I(X₁ⁿ; Yⁿ | X₂ⁿ).

The first half is the identity I(M₁; (M₂, Yⁿ)) = I(M₁; Yⁿ | M₂), from the Y-axis chain rule and message independence. The second half is the data-processing reduction I(M₁; Yⁿ | M₂) ≤ I(X₁ⁿ; Yⁿ | X₂ⁿ), which lowers both the data variable M₁ → X₁ⁿ and the conditioner M₂ → X₂ⁿ (each a deterministic function of the message) under the block channel Markov chain. It is carried out on the entropy difference I(·;·|·) = H(Yⁿ|·) − H(Yⁿ|·,·), with H(Yⁿ | (M₂, M₁)) = H(Yⁿ | (X₂ⁿ, X₁ⁿ)) (deterministic encoders plus the block Markov chain) and H(Yⁿ | M₂) ≤ H(Yⁿ | X₂ⁿ) (conditioning on the finer message reduces entropy).

Used by

theorem

InformationTheory.Shannon.MAC.mac_singleletterize_bound₁

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSingletonClass α₁] [StandardBorelSpace α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSingletonClass α₂] [StandardBorelSpace α₂] [DecidableEq β] [Nonempty β] [StandardBorelSpace β] [NeZero M₁] [NeZero M₂] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg₁ : Ω → Fin M₁) (Msg₂ : Ω → Fin M₂) (Ys : Fin n → Ω → β) (c : MACCode M₁ M₂ n α₁ α₂ β) (hMsg₁ : Measurable Msg₁) (hMsg₂ : Measurable Msg₂) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (h_memo : ChannelCodingConverseGeneral.IsMemorylessChannel μ (fun (i : Fin n) (ω : Ω) => (c.encoder₁ (Msg₁ ω) i, c.encoder₂ (Msg₂ ω) i)) Ys) (h_indep : mutualInfo μ Msg₁ Msg₂ = 0) (hmarkov : IsMarkovChain μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) => (fun (j : Fin n) => c.encoder₁ (Msg₁ ω) j, fun (j : Fin n) => c.encoder₂ (Msg₂ ω) j)) fun (ω : Ω) (j : Fin n) => Ys j ω) :

(mutualInfo μ Msg₁ fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)) ≤ ∑ i : Fin n, condMutualInfo μ (fun (ω : Ω) => c.encoder₁ (Msg₁ ω) i) (Ys i) fun (ω : Ω) => c.encoder₂ (Msg₂ ω) i

Single-letterized user-1 corner bound of the MAC converse: under a memoryless joint channel, independent messages, and the block channel Markov chain, the message–output mutual information I(M₁; (M₂, Yⁿ)) is bounded by the per-letter single-letter channel sum ∑ᵢ I(X₁ᵢ; Yᵢ | X₂ᵢ).

Used by

theorem

InformationTheory.Shannon.MAC.mac_singleletterize_bound₂

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSingletonClass α₁] [StandardBorelSpace α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSingletonClass α₂] [StandardBorelSpace α₂] [DecidableEq β] [Nonempty β] [StandardBorelSpace β] [NeZero M₁] [NeZero M₂] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg₁ : Ω → Fin M₁) (Msg₂ : Ω → Fin M₂) (Ys : Fin n → Ω → β) (c : MACCode M₁ M₂ n α₁ α₂ β) (hMsg₁ : Measurable Msg₁) (hMsg₂ : Measurable Msg₂) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (h_memo : ChannelCodingConverseGeneral.IsMemorylessChannel μ (fun (i : Fin n) (ω : Ω) => (c.encoder₁ (Msg₁ ω) i, c.encoder₂ (Msg₂ ω) i)) Ys) (h_indep : mutualInfo μ Msg₁ Msg₂ = 0) (hmarkov : IsMarkovChain μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) => (fun (j : Fin n) => c.encoder₁ (Msg₁ ω) j, fun (j : Fin n) => c.encoder₂ (Msg₂ ω) j)) fun (ω : Ω) (j : Fin n) => Ys j ω) :

(mutualInfo μ Msg₂ fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)) ≤ ∑ i : Fin n, condMutualInfo μ (fun (ω : Ω) => c.encoder₂ (Msg₂ ω) i) (Ys i) fun (ω : Ω) => c.encoder₁ (Msg₁ ω) i

Single-letterized user-2 corner bound of the MAC converse, symmetric to mac_singleletterize_bound₁ with the two users swapped.

Used by

theorem

InformationTheory.Shannon.MAC.mac_singleletterize_bound_sum

source

(mutualInfo μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) fun (ω : Ω) (i : Fin n) => Ys i ω) ≤ ∑ i : Fin n, mutualInfo μ (fun (ω : Ω) => (c.encoder₁ (Msg₁ ω) i, c.encoder₂ (Msg₂ ω) i)) (Ys i)

Single-letterized sum-rate bound of the MAC converse: treating (M₁, M₂) as one joint message and (X₁ᵢ, X₂ᵢ) as one joint input, the joint message–output mutual information I((M₁, M₂); Yⁿ) is bounded by the unconditional per-letter sum ∑ᵢ I((X₁ᵢ, X₂ᵢ); Yᵢ).

Used by

theorem

InformationTheory.Shannon.MAC.mac_converse

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [MeasurableSpace α₁] [MeasurableSpace α₂] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M₁ M₂ n : ℕ} [Fintype α₁] [DecidableEq α₁] [Nonempty α₁] [MeasurableSingletonClass α₁] [StandardBorelSpace α₁] [Fintype α₂] [DecidableEq α₂] [Nonempty α₂] [MeasurableSingletonClass α₂] [StandardBorelSpace α₂] [DecidableEq β] [Nonempty β] [StandardBorelSpace β] [NeZero M₁] [NeZero M₂] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Msg₁ : Ω → Fin M₁) (Msg₂ : Ω → Fin M₂) (Ys : Fin n → Ω → β) (c : MACCode M₁ M₂ n α₁ α₂ β) (hMsg₁ : Measurable Msg₁) (hMsg₂ : Measurable Msg₂) (hYs : ∀ (i : Fin n), Measurable (Ys i)) (hMsg₁_uniform : MeasureTheory.Measure.map Msg₁ μ = (↑(Fintype.card (Fin M₁)))⁻¹ • MeasureTheory.Measure.count) (hMsg₂_uniform : MeasureTheory.Measure.map Msg₂ μ = (↑(Fintype.card (Fin M₂)))⁻¹ • MeasureTheory.Measure.count) (hMsg₁₂_uniform : MeasureTheory.Measure.map (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) μ = (↑(Fintype.card (Fin M₁ × Fin M₂)))⁻¹ • MeasureTheory.Measure.count) (h_memo : ChannelCodingConverseGeneral.IsMemorylessChannel μ (fun (i : Fin n) (ω : Ω) => (c.encoder₁ (Msg₁ ω) i, c.encoder₂ (Msg₂ ω) i)) Ys) (h_indep : mutualInfo μ Msg₁ Msg₂ = 0) (hmarkov : IsMarkovChain μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) => (fun (j : Fin n) => c.encoder₁ (Msg₁ ω) j, fun (j : Fin n) => c.encoder₂ (Msg₂ ω) j)) fun (ω : Ω) (j : Fin n) => Ys j ω) (hcard₁ : 2 ≤ M₁) (hcard₂ : 2 ≤ M₂) :

InMACCapacityRegion (Real.log ↑M₁) (Real.log ↑M₂) ((∑ i : Fin n, condMutualInfo μ (fun (ω : Ω) => c.encoder₁ (Msg₁ ω) i) (Ys i) fun (ω : Ω) => c.encoder₂ (Msg₂ ω) i).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg₁ (fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₂ × (Fin n → β)) => (c.decoder p.2).1) + (MeasureFano.errorProb μ Msg₁ (fun (ω : Ω) => (Msg₂ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₂ × (Fin n → β)) => (c.decoder p.2).1) * Real.log (↑M₁ - 1)) ((∑ i : Fin n, condMutualInfo μ (fun (ω : Ω) => c.encoder₂ (Msg₂ ω) i) (Ys i) fun (ω : Ω) => c.encoder₁ (Msg₁ ω) i).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg₂ (fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₁ × (Fin n → β)) => (c.decoder p.2).2) + (MeasureFano.errorProb μ Msg₂ (fun (ω : Ω) => (Msg₁ ω, fun (i : Fin n) => Ys i ω)) fun (p : Fin M₁ × (Fin n → β)) => (c.decoder p.2).2) * Real.log (↑M₂ - 1)) ((∑ i : Fin n, mutualInfo μ (fun (ω : Ω) => (c.encoder₁ (Msg₁ ω) i, c.encoder₂ (Msg₂ ω) i)) (Ys i)).toReal + Real.binEntropy (MeasureFano.errorProb μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) (i : Fin n) => Ys i ω) c.decoder) + MeasureFano.errorProb μ (fun (ω : Ω) => (Msg₁ ω, Msg₂ ω)) (fun (ω : Ω) (i : Fin n) => Ys i ω) c.decoder * Real.log (↑(M₁ * M₂) - 1))

Per-letter-sum outer bound for the MAC (Cover–Thomas): for uniform, independent messages sent over a memoryless joint channel and decoded jointly, the rate pair (log |M₁|, log |M₂|) lies in the capacity region whose information bounds are the per-letter single-letter channel sums (plus the Fano error slack).

This is the single-letterized MAC converse, distinct from the message-level mac_converse_message_level: the information slots are the per-time-step channel quantities ∑ᵢ I(X₁ᵢ; Yᵢ | X₂ᵢ), ∑ᵢ I(X₂ᵢ; Yᵢ | X₁ᵢ), ∑ᵢ I((X₁ᵢ, X₂ᵢ); Yᵢ), obtained from the message-level bound via the single-letterization lemmas and InMACCapacityRegion.mono.

The information bounds are per-letter sums, one marginal input distribution per time step; the single-distribution convex-hull form is mac_timesharing_converse.

The Fano slack is stated in terms of the joint-decoder error probability MeasureFano.errorProb, with the memoryless channel structure and block Markov chain taken as preconditions (parity with the single-user channel_coding_converse_general_memoryless_pure). The operational instantiation — building μ from uniform messages through the encoders and the memoryless channel W, and identifying the error with MACCode.averageErrorProb W — is the wrapper mac_converse_from_code. @audit:ok

Used by