InformationTheory

InformationTheory.Shannon.ChannelCoding.StrongConverse

source

Imports 5

Channel coding strong converse — Verdú-Han single-shot lower bound #

Single-shot Verdú-Han lower bound for the channel coding strong converse. For any code c, reference output law Q^n, and γ > 0, with threshold := log M + γ:

1 - (c.averageErrorProb W).toReal
  ≤ exp γ + (1 / M) * ∑ m, P_m^n (highLLRSet W c Q^n threshold m)

where P_m^n := Measure.pi (fun i => W (c.encoder m i)) and highLLRSet W c Q^n t m := { y | P_m^n.real {y} > exp(t) · Q^n.real {y} }.

The asymptotic Pe → 1 conclusion (for log M / n > I + δ) requires a WLLN step handled in a separate file.

Implementation notes #

The reference measure Q^n is an arbitrary probability measure (not necessarily i.i.d. (outputDistribution p W)^n), following Verdú-Han's deterministic formulation and separating the input-distribution dependence to the caller.

Per-codeword information-density lower bound #

noncomputable def

InformationTheory.Shannon.ChannelCoding.highLLRSet

source
{α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M n : ℕ} (W : Channel α β) (c : Code M n α β) (Q : MeasureTheory.Measure (Fin n → β)) (threshold : ℝ) (m : Fin M) :
Set (Fin n → β)

High-LLR set for codeword m: those y where the channel output law at codeword m exceeds the reference Q by more than exp(threshold).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Used by
      theorem

      InformationTheory.Shannon.ChannelCoding.measurableSet_highLLRSet

      source
      {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M n : ℕ} (W : Channel α β) (c : Code M n α β) (Q : MeasureTheory.Measure (Fin n → β)) (threshold : ℝ) (m : Fin M) :
      MeasurableSet (highLLRSet W c Q threshold m)
      Used by
        theorem

        InformationTheory.Shannon.ChannelCoding.channelCoding_per_codeword_markov_bound

        source
        {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M n : ℕ} (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (c : Code M n α β) (Q : MeasureTheory.Measure (Fin n → β)) [MeasureTheory.IsFiniteMeasure Q] (threshold : ℝ) (m : Fin M) (s : Set (Fin n → β)) (_hs : MeasurableSet s) :
        (MeasureTheory.Measure.pi fun (i : Fin n) => W (c.encoder m i)).real (s \ highLLRSet W c Q threshold m) ≤ Real.exp threshold * Q.real s

        Per-codeword Markov-style bound: For each codeword m, the channel output mass on s \ highLLR_m is bounded by exp(threshold) · Q(s).

        Used by
          theorem

          InformationTheory.Shannon.ChannelCoding.channelCoding_per_codeword_decomposition

          source
          {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M n : ℕ} (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (c : Code M n α β) (Q : MeasureTheory.Measure (Fin n → β)) [MeasureTheory.IsFiniteMeasure Q] (threshold : ℝ) (m : Fin M) (s : Set (Fin n → β)) (hs : MeasurableSet s) :
          (MeasureTheory.Measure.pi fun (i : Fin n) => W (c.encoder m i)).real s ≤ Real.exp threshold * Q.real s + (MeasureTheory.Measure.pi fun (i : Fin n) => W (c.encoder m i)).real (highLLRSet W c Q threshold m)

          Verdú-Han single-shot strong-converse decomposition (per-codeword): For any codeword m, any measurable s,

          P_m^n(s) ≤ exp(threshold) · Q(s) + P_m^n(highLLR_m)

          The "good" (low-LLR) part is absorbed into the Q-mass term; the "bad" (high-LLR) part is the explicit tail term. Channel-coding analogue of steinTypicalSet_Q_prob_ge.

          Used by

            Codeword-average Verdú-Han lower bound #

            theorem

            InformationTheory.Shannon.ChannelCoding.channelCoding_one_sub_avgErr_eq

            source
            {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M : ℕ} (hM : 0 < M) {n : ℕ} (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (c : Code M n α β) :
            1 - (c.averageErrorProb W).toReal = 1 / ↑M * ∑ m : Fin M, (MeasureTheory.Measure.pi fun (i : Fin n) => W (c.encoder m i)).real (c.decodingRegion m)

            Algebraic identity: 1 - avgErrorProb = (1/M) · ∑_m Pm(decodingRegion m), where Pm = Measure.pi (fun i => W (encoder m i)).

            Used by
              theorem

              InformationTheory.Shannon.ChannelCoding.channelCoding_average_success_le

              source
              {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [Fintype β] [MeasurableSpace β] [MeasurableSingletonClass β] {M : ℕ} (hM : 0 < M) {n : ℕ} (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (c : Code M n α β) (Q : MeasureTheory.Measure (Fin n → β)) [MeasureTheory.IsProbabilityMeasure Q] (threshold : ℝ) :
              1 - (c.averageErrorProb W).toReal ≤ Real.exp threshold / ↑M + 1 / ↑M * ∑ m : Fin M, (MeasureTheory.Measure.pi fun (i : Fin n) => W (c.encoder m i)).real (highLLRSet W c Q threshold m)

              Average-codeword Verdú-Han bound: Average the per-codeword decomposition over the uniform message distribution to get the strong-converse-style lower bound on success probability 1 - avgPe:

              1 - avgPe ≤ exp(threshold) / M + (1 / M) · ∑_m P_m^n(highLLR_m)

              The decoding regions form a measurable partition of Fin n → β, so summing Q.real (decodingRegion m) gives Q.real univ ≤ 1 (since Q is a probability measure), and the first term collapses to exp(threshold)/M.

              Used by

                Main form with threshold := log M + γ #