InformationTheory

InformationTheory.Shannon.ChannelCoding.Achievability.Main

source

Imports 9

Channel coding achievability — pigeonhole + main theorem #

Part of the longFile split of Achievability.lean. This part holds the probabilistic-method pigeonhole exists_codebook_le_avg and the headline theorem channel_coding_achievability, which combines the random-codebook average bound from ...Achievability.RandomCodebook with the pigeonhole.

References #

  • T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

Pigeonhole (probabilistic-method form) #

Codebooks are drawn from codebookMeasure p M n rather than uniformly over Codebook M n α. The pigeonhole: if the expectation ∑ codebook, μ_codebook · f(codebook) ≤ B, then some codebook in the support has f(codebook) ≤ B. The proof uses the fact that the codebook measure is a probability measure (mass sums to 1 over the finite space) so the weighted average is a convex combination.

theorem

InformationTheory.Shannon.ChannelCoding.exists_codebook_le_avg

source
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [MeasurableSingletonClass α] [Fintype β] {Ω : Type u_3} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (p : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure p] {M n : ℕ} (hM : 0 < M) {ε : ℝ} (B : ℝ) (h_avg : ∑ codebook : Codebook M n α, (codebookMeasure p M n).real {codebook} * ((codebookToCode μ Xs Ys hM ε codebook).averageErrorProb W).toReal ≤ B) :
∃ (codebook : Codebook M n α), ((codebookToCode μ Xs Ys hM ε codebook).averageErrorProb W).toReal ≤ B

Pigeonhole (probabilistic-method form). If the codebook expectation is ≤ B, then there exists a single codebook with averageErrorProb ≤ B.

Used by

    Existence of a low-error codebook for large n #

    The "eventual smallness of random-codebook average" step is folded into the main theorem's proof; this section deliberately exposes no extra public lemma. channel_coding_achievability combines random_codebook_average_le, exists_codebook_le_avg, and the rate-slack analysis.

    The main theorem instantiates random_codebook_average_le with the i.i.d. extension of (p, W) on Ω := ℕ → α × β, μ := iidAmbientMeasure p W, Xs i ω := (ω i).1, Ys i ω := (ω i).2. The bridges to the abstract formulation are:

    • iIndepFun (Xs/Ys) μ from iIndepFun_infinitePi + composition with Prod.fst/.snd.
    • IdentDistrib (Xs i) (Xs 0) μ μ from infinitePi_map_eval (identical marginals).
    • μ.map (Xs 0) = p, μ.map (Ys 0) = outputDistribution p W, μ.map (jointSequence Xs Ys 0) = jointDistribution p W.
    • hposX / hposY / hposZ (singleton positivity of the block marginals) follow from the channel-positivity hypotheses hp_pos / hW_pos.
    • The exponent entropy μ (jointSequence ...) − entropy μ (Xs 0) − entropy μ (Ys 0) = −(mutualInfoOfChannel p W).toReal is the entropy-MI three-term identity mutualInfoOfChannel_eq_HX_add_HY_sub_HZ (chain rule + commutativity).

    Shared helpers for the main theorem #

    theorem

    InformationTheory.Shannon.ChannelCoding.channelCoding_entropy_exponent_eq

    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] :
    entropy (iidAmbientMeasure p W) (jointSequence iidXs iidYs 0) - entropy (iidAmbientMeasure p W) (iidXs 0) - entropy (iidAmbientMeasure p W) (iidYs 0) = -(mutualInfoOfChannel p W).toReal

    The entropy exponent identity for the i.i.d. ambient measure: H(Z₀) - H(X₀) - H(Y₀) = -(mutualInfoOfChannel p W).toReal, where (X₀, Y₀, Z₀) are the 0-th marginals of the i.i.d. extension.

    Used by
      theorem

      InformationTheory.Shannon.ChannelCoding.complementProbReal_le_of_one_sub_le

      source
      {Ω : Type u_3} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s : Set Ω} (hs : MeasurableSet s) {b : ℝ} (h : 1 - b ≤ (μ s).toReal) :
      μ.real sᶜ ≤ b

      In a probability space, if 1 - b ≤ (μ s).toReal then μ.real sᶜ ≤ b.

      Used by

        Main theorem #

        theorem

        InformationTheory.Shannon.ChannelCoding.channel_coding_achievability

        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}) (hW_pos : ∀ (a : α) (b : β), 0 < (W a).real {b}) {R : ℝ} (hR_pos : 0 < R) (hR : R < (mutualInfoOfChannel p W).toReal) {ε' : ℝ} (hε' : 0 < ε') :
        ∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (c : Code M n α β), (c.averageErrorProb W).toReal < ε'

        Shannon's noisy channel coding theorem (achievability): for any rate R < I(p; W) and target error probability ε' > 0, there exists N such that for all n ≥ N there is a block code of length n with at least exp (n · R) messages whose average error probability is < ε'.

        Used by