InformationTheory.Shannon.ChannelCoding.Achievability.RandomCodebook

Imports 9

Channel coding achievability — random codebook average bound #

Part of the longFile split of Achievability.lean. This part holds the Fubini-style swap helpers (private lemmas block_law_X_eq_pi_p, block_law_Y_eq_pi, block_joint_law_eq_pi, codebook_marginal_one, codebook_marginal_two, random_codebook_E1_swap, random_codebook_E2_swap) and their sole consumer random_codebook_average_le. The private lemmas and their consumer are deliberately kept in the same file (file-scoped private).

theorem

InformationTheory.Shannon.ChannelCoding.measureReal_pi_singleton_eq_prod

source

{ι : Type u_3} [Fintype ι] {δ : ι → Type u_4} [(i : ι) → MeasurableSpace (δ i)] (κ : (i : ι) → MeasureTheory.Measure (δ i)) [∀ (i : ι), MeasureTheory.SigmaFinite (κ i)] [∀ (i : ι), MeasureTheory.IsFiniteMeasure (κ i)] (x : (i : ι) → δ i) :

(MeasureTheory.Measure.pi κ).real {x} = ∏ i : ι, (κ i).real {x i}

Used by

theorem

InformationTheory.Shannon.ChannelCoding.jointDistribution_real_singleton

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (a : α) (b : β) :

(jointDistribution p W).real {(a, b)} = p.real {a} * (W a).real {b}

Used by

theorem

InformationTheory.Shannon.ChannelCoding.outputDistribution_real_singleton_eq_sum

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [MeasurableSingletonClass β] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (b : β) :

(outputDistribution p W).real {b} = ∑ a : α, p.real {a} * (W a).real {b}

Used by

Fubini helpers for the random codebook average. #

The two helper lemmas below carry the Fubini-style swap between "codebook expectation" and the (X^n, Y^n) joint law under μ. They are the only ingredients that use the marginal-matching hypotheses h_match_X / h_match_Z.

theorem

InformationTheory.Shannon.ChannelCoding.block_law_X_eq_pi_p

source

{α : Type u_1} [MeasurableSpace α] {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindepX : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hidentX : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (h_match_X : MeasureTheory.Measure.map (Xs 0) μ = p) (n : ℕ) :

MeasureTheory.Measure.map (jointRV Xs n) μ = MeasureTheory.Measure.pi fun (x : Fin n) => p

Block X-law identification. Under iIndepFun (Xs ·) μ and h_match_X : μ.map (Xs 0) = p, the block law μ.map (jointRV Xs n) equals Measure.pi (fun _ : Fin n ↦ p). This is the bridge to the codebookMeasure p M n structure.

Promoted to non-private so the two-codebook MAC achievability averaging in InformationTheory.Shannon.MultipleAccess.Achievability can reuse it for the user-1 alias axis and the (X₂, Y) joint-sequence axis (signature unchanged; no cross-file consumer existed before).

Used by

Codebook-row marginalization. #

The codebookMeasure p M n is a product over Fin M of Measure.pi p-rows. When the integrand depends only on the m-th row (resp. m-th and m'-th rows for m ≠ m'), we can factorize and sum out the other rows.

theorem

InformationTheory.Shannon.ChannelCoding.prod_erase_eq_prod_subtype_ne

source

{M : ℕ} [DecidableEq (Fin M)] (m : Fin M) {R : Type u_3} [CommMonoid R] (g : Fin M → R) (g' : { m' : Fin M // m' ≠ m } → R) (hg : ∀ (m'' : Fin M) (h : m'' ≠ m), g m'' = g' ⟨m'', h⟩) :

∏ m'' ∈ Finset.univ.erase m, g m'' = ∏ m'' : { m' : Fin M // m' ≠ m }, g' m''

Used by

theorem

InformationTheory.Shannon.ChannelCoding.sum_prod_measureReal_singleton_eq_one

source

{J : Type u_3} {γ : Type u_4} [Fintype J] [DecidableEq J] [Fintype γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (P : MeasureTheory.Measure γ) [MeasureTheory.IsProbabilityMeasure P] :

∑ c : J → γ, ∏ j : J, P.real {c j} = 1

Used by

theorem

InformationTheory.Shannon.ChannelCoding.codebook_marginal_one

source

{α : Type u_1} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (M n : ℕ) (m : Fin M) (f : (Fin n → α) → ℝ) (_hf_nn : ∀ (x : Fin n → α), 0 ≤ f x) :

∑ c : Codebook M n α, (codebookMeasure p M n).real {c} * f (c m) = ∑ x : Fin n → α, (MeasureTheory.Measure.pi fun (x : Fin n) => p).real {x} * f x

Single-row marginalization. Sum out all rows other than m.

Promoted to non-private for reuse by the two-codebook MAC achievability averaging (both Codebook/MACCodebook reduce to Fin M → Fin n → α).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.codebook_marginal_two

source

{α : Type u_1} [MeasurableSpace α] [Fintype α] [MeasurableSingletonClass α] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (M n : ℕ) (m m' : Fin M) (hne : m ≠ m') (f : (Fin n → α) → (Fin n → α) → ℝ) (_hf_nn : ∀ (x x' : Fin n → α), 0 ≤ f x x') :

∑ c : Codebook M n α, (codebookMeasure p M n).real {c} * f (c m) (c m') = ∑ x : Fin n → α, ∑ x' : Fin n → α, (MeasureTheory.Measure.pi fun (x : Fin n) => p).real {x} * (MeasureTheory.Measure.pi fun (x : Fin n) => p).real {x'} * f x x'

Two-row marginalization. Sum out all rows other than m and m' (with m ≠ m').

Promoted to non-private for reuse by the two-codebook MAC achievability averaging (the user-1 true/alias two-row marginalization).

Used by

theorem

InformationTheory.Shannon.ChannelCoding.sum_weighted_diag_offdiag_decomp

source

{ι : Type u_3} [Fintype ι] [DecidableEq ι] {M : ℕ} (w : ι → ℝ) (a : ι → Fin M → ℝ) (b : ι → Fin M → Fin M → ℝ) (Minv : ℝ) :

∑ c : ι, w c * (Minv * ∑ m : Fin M, (a c m + ∑ m' ∈ Finset.univ.erase m, b c m m')) = Minv * ∑ m : Fin M, (∑ c : ι, w c * a c m + ∑ m' ∈ Finset.univ.erase m, ∑ c : ι, w c * b c m m')

Used by

theorem

InformationTheory.Shannon.ChannelCoding.diag_add_offdiag_sum_le

source

{M : ℕ} (hM : 0 < M) (a : ℝ) (b : Fin M → ℝ) (A B : ℝ) {m : Fin M} (ha : a ≤ A) (hb : ∀ m' ∈ Finset.univ.erase m, b m' ≤ B) :

a + ∑ m' ∈ Finset.univ.erase m, b m' ≤ A + (↑M - 1) * B

Used by

theorem

InformationTheory.Shannon.ChannelCoding.sum_average_le_of_forall_le

source

{M : ℕ} (g : Fin M → ℝ) (Minv B : ℝ) (hMinv : 0 ≤ Minv) (hMinvM : Minv * ↑M = 1) (hg : ∀ (m : Fin M), g m ≤ B) :

Minv * ∑ m : Fin M, g m ≤ B

Used by

theorem

InformationTheory.Shannon.ChannelCoding.random_codebook_average_le

source

{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] (hp_pos : ∀ (a : α), 0 < p.real {a}) {M n : ℕ} (hM : 0 < M) {ε : ℝ} (hε : 0 < ε) {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepX : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hidentX : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hindepY : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Ys i) μ) (hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ) (hindepZ : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (jointSequence Xs Ys i) (jointSequence Xs Ys j) μ) (hindepZ_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => jointSequence Xs Ys i) μ) (hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (jointSequence Xs Ys i) (jointSequence Xs Ys 0) μ μ) (hposX : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (hposY : ∀ (y : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {y}) (hposZ : ∀ (q : α × β), 0 < (MeasureTheory.Measure.map (jointSequence Xs Ys 0) μ).real {q}) (h_match_X : MeasureTheory.Measure.map (Xs 0) μ = p) (h_match_Z : MeasureTheory.Measure.map (jointSequence Xs Ys 0) μ = jointDistribution p W) :

∑ codebook : Codebook M n α, (codebookMeasure p M n).real {codebook} * ((codebookToCode μ Xs Ys hM ε codebook).averageErrorProb W).toReal ≤ μ.real {ω : Ω | (jointRV Xs n ω, jointRV Ys n ω) ∉ jointlyTypicalSet μ Xs Ys n ε} + (↑M - 1) * Real.exp (↑n * (entropy μ (jointSequence Xs Ys 0) - entropy μ (Xs 0) - entropy μ (Ys 0) + 3 * ε))

Random codebook average (probabilistic-method form). With each codeword drawn i.i.d. from p^n (so the codebook law is codebookMeasure p M n), the codebook-average of the (uniform-over-message) error probability decomposes via Fubini into the "joint typical event probability" (E1) plus (M - 1) · the independent-pair bound (E2).

The structural backbone (per-codebook bound via errorProbAt_le_E1_plus_E2, sum / swap arithmetic) is assembled here from the two Fubini swap ingredients random_codebook_E1_swap and random_codebook_E2_swap (private lemmas above).

Used by