InformationTheory.Shannon.MultipleAccess.AchievabilityCore

Imports 3

Multiple access channel — achievability analytic core #

The conditional independent-pair probability bounds E1 / E2 / E3 for the two-user MAC random-coding argument (Cover–Thomas). These are the genuinely analytic ingredient of MAC achievability; the rest of the achievability proof (Bonferroni union bound + two-codebook averaging) is plumbing over these bounds.

Approach #

Each Eⱼ is a regrouping instance of the single-user independent-pair bound InformationTheory.Shannon.ChannelCoding.jointlyTypicalSet_indep_prob_le. For E1 (user 1 uses a wrong codeword X̃₁ ⟂ (X₂, Y)), the three-way jointly typical set macJointlyTypicalSet is contained, under the reshape (x₁, x₂, y) ↦ (x₁, fun i ↦ (x₂ i, y i)), in the single-user jointly typical set jointlyTypicalSet μ X₁s (jointSequence X₂s Ys) (treating the pair (X₂, Y) as the single "output" axis). Measure monotonicity plus the product-measure pushforward identity Measure.map_prod_map then reduce the bound to the single-user lemma, whose exit form is exactly the desired H-form exponent H(X₁, X₂, Y) − H(X₁) − H(X₂, Y) + 3ε.

theorem

InformationTheory.Shannon.MAC.macJTS_indep_prob_le_X1

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) (hX1s : ∀ (i : ℕ), Measurable (X1s i)) (hX2s : ∀ (i : ℕ), Measurable (X2s i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepX1 : ProbabilityTheory.iIndepFun (fun (i : ℕ) => X1s i) μ) (hidentX1 : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X1s i) (X1s 0) μ μ) (hindepX2Y : ProbabilityTheory.iIndepFun (fun (i : ℕ) => ChannelCoding.jointSequence X2s Ys i) μ) (hidentX2Y : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence X2s Ys i) (ChannelCoding.jointSequence X2s Ys 0) μ μ) (hposX1 : ∀ (x : α₁), 0 < (MeasureTheory.Measure.map (X1s 0) μ).real {x}) (hposX2Y : ∀ (p : α₂ × β), 0 < (MeasureTheory.Measure.map (ChannelCoding.jointSequence X2s Ys 0) μ).real {p}) (hposZ : ∀ (p : α₁ × α₂ × β), 0 < (MeasureTheory.Measure.map (macJointSequence X1s X2s Ys 0) μ).real {p}) (n : ℕ) {ε : ℝ} (hε : 0 < ε) :

((MeasureTheory.Measure.map (jointRV X1s n) μ).prod (MeasureTheory.Measure.map (fun (ω : Ω) => (jointRV X2s n ω, jointRV Ys n ω)) μ)).real (macJointlyTypicalSet μ X1s X2s Ys n ε) ≤ Real.exp (↑n * (entropy μ (macJointSequence X1s X2s Ys 0) - entropy μ (X1s 0) - entropy μ (ChannelCoding.jointSequence X2s Ys 0) + 3 * ε))

Conditional independent-pair bound for user 1, controlling the E1 alias event: when user 1's codeword X̃₁ is drawn independently of the jointly distributed pair (X₂, Y), the probability that the triple lands in the three-way jointly typical set is at most exp(n·(H(X₁,X₂,Y) − H(X₁) − H(X₂,Y) + 3ε)).

The measure is the product of user 1's block law and the joint block law of (X₂, Y). The exponent is the single-user exit form; combined with input independence (downstream) it equals exp(-n·(I(X₁;Y|X₂) − 3ε)).

@audit:ok

Used by

theorem

InformationTheory.Shannon.MAC.macJTS_indep_prob_le_both

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) (hX1s : ∀ (i : ℕ), Measurable (X1s i)) (hX2s : ∀ (i : ℕ), Measurable (X2s i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepX1X2 : ProbabilityTheory.iIndepFun (fun (i : ℕ) => ChannelCoding.jointSequence X1s X2s i) μ) (hidentX1X2 : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence X1s X2s i) (ChannelCoding.jointSequence X1s X2s 0) μ μ) (hindepY : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Ys i) μ) (hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ) (hposX1X2 : ∀ (p : α₁ × α₂), 0 < (MeasureTheory.Measure.map (ChannelCoding.jointSequence X1s X2s 0) μ).real {p}) (hposY : ∀ (y : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {y}) (hposZ : ∀ (p : (α₁ × α₂) × β), 0 < (MeasureTheory.Measure.map (ChannelCoding.jointSequence (ChannelCoding.jointSequence X1s X2s) Ys 0) μ).real {p}) (n : ℕ) {ε : ℝ} (hε : 0 < ε) :

((MeasureTheory.Measure.map (jointRV (ChannelCoding.jointSequence X1s X2s) n) μ).prod (MeasureTheory.Measure.map (jointRV Ys n) μ)).real ((fun (q : (Fin n → α₁ × α₂) × (Fin n → β)) => (fun (i : Fin n) => (q.1 i).1, fun (i : Fin n) => (q.1 i).2, q.2)) ⁻¹' macJointlyTypicalSet μ X1s X2s Ys n ε) ≤ Real.exp (↑n * (entropy μ (macJointSequence X1s X2s Ys 0) - entropy μ (ChannelCoding.jointSequence X1s X2s 0) - entropy μ (Ys 0) + 3 * ε))

Conditional independent-pair bound for both users, controlling the E3 alias event: when the pair of codewords (X̃₁, X̃₂) is drawn independently of the output block Y, the probability that the (reshuffled) triple lands in the three-way jointly typical set is at most exp(n·(H(X₁,X₂,Y) − H(X₁,X₂) − H(Y) + 3ε)).

This is the direct three-axis analogue of the single-user independent-pair bound, with the (X₁,X₂) axes grouped as the "input" and Y as the "output". Combined with input independence (downstream) the exponent equals exp(-n·(I(X₁,X₂;Y) − 3ε)).

@audit:ok

Used by

theorem

InformationTheory.Shannon.MAC.macJTS_indep_prob_le_X2

source

{Ω : Type u_1} [MeasurableSpace Ω] {α₁ : Type u_2} {α₂ : Type u_3} {β : Type u_4} [Fintype α₁] [Nonempty α₁] [MeasurableSpace α₁] [MeasurableSingletonClass α₁] [Fintype α₂] [Nonempty α₂] [MeasurableSpace α₂] [MeasurableSingletonClass α₂] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X1s : ℕ → Ω → α₁) (X2s : ℕ → Ω → α₂) (Ys : ℕ → Ω → β) (hX1s : ∀ (i : ℕ), Measurable (X1s i)) (hX2s : ∀ (i : ℕ), Measurable (X2s i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepX2 : ProbabilityTheory.iIndepFun (fun (i : ℕ) => X2s i) μ) (hidentX2 : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X2s i) (X2s 0) μ μ) (hindepX1Y : ProbabilityTheory.iIndepFun (fun (i : ℕ) => ChannelCoding.jointSequence X1s Ys i) μ) (hidentX1Y : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (ChannelCoding.jointSequence X1s Ys i) (ChannelCoding.jointSequence X1s Ys 0) μ μ) (hposX2 : ∀ (x : α₂), 0 < (MeasureTheory.Measure.map (X2s 0) μ).real {x}) (hposX1Y : ∀ (p : α₁ × β), 0 < (MeasureTheory.Measure.map (ChannelCoding.jointSequence X1s Ys 0) μ).real {p}) (hposZ : ∀ (p : α₂ × α₁ × β), 0 < (MeasureTheory.Measure.map (ChannelCoding.jointSequence X2s (ChannelCoding.jointSequence X1s Ys) 0) μ).real {p}) (n : ℕ) {ε : ℝ} (hε : 0 < ε) :

((MeasureTheory.Measure.map (jointRV X2s n) μ).prod (MeasureTheory.Measure.map (jointRV (ChannelCoding.jointSequence X1s Ys) n) μ)).real ((fun (q : (Fin n → α₂) × (Fin n → α₁ × β)) => (fun (i : Fin n) => (q.2 i).1, q.1, fun (i : Fin n) => (q.2 i).2)) ⁻¹' macJointlyTypicalSet μ X1s X2s Ys n ε) ≤ Real.exp (↑n * (entropy μ (macJointSequence X1s X2s Ys 0) - entropy μ (X2s 0) - entropy μ (ChannelCoding.jointSequence X1s Ys 0) + 3 * ε))

Conditional independent-pair bound for user 2, controlling the E2 alias event: when user 2's codeword X̃₂ is drawn independently of the jointly distributed pair (X₁, Y), the probability that the (reshuffled) triple lands in the three-way jointly typical set is at most exp(n·(H(X₁,X₂,Y) − H(X₂) − H(X₁,Y) + 3ε)).

This is the user-1/user-2 mirror image of macJTS_indep_prob_le_X1, with (X₁, Y) as the jointly distributed "output" axis. Combined with input independence (downstream) the exponent equals exp(-n·(I(X₂;Y|X₁) − 3ε)).

@audit:ok

Used by