InformationTheory

InformationTheory.Shannon.AWGN.AchievabilityExpurgation

source

Imports 12

Expurgation, power-constraint witness, and code extraction #

The expurgation and feasibility apparatus for AWGN achievability (Cover–Thomas): worst-half expurgation, the power-constraint slack witness producing a strictly smaller variance, and the bridge from a deterministic codebook to the AwgnCode type.

Main statements #

Expurgation #

theorem

InformationTheory.Shannon.AWGN.awgn_exists_codebook_le_avg

source
{M n : ℕ} (σsq : NNReal) (Pe : (Fin M → Fin n → ℝ) → ENNReal) (hPe_aemeas : AEMeasurable Pe (gaussianCodebook M n σsq)) {B : ENNReal} (h_avg : ∫⁻ (c : Fin M → Fin n → ℝ), Pe c ∂gaussianCodebook M n σsq ≤ B) :
∃ (c_specific : Fin M → Fin n → ℝ), Pe c_specific ≤ B

If the codebook-average of Pe is at most B, then some specific codebook achieves Pe ≤ B.

Used by
    theorem

    InformationTheory.Shannon.AWGN.awgn_expurgate_worst_half

    source
    {M : ℕ} (hM : 2 ≤ M) (Pe : Fin M → ℝ) (hPe_nn : ∀ (m : Fin M), 0 ≤ Pe m) {ε : ℝ} (hε : 0 < ε) (h_avg : ∑ m : Fin M, Pe m ≤ ↑M * (2 * ε)) :
    ∃ (S : Finset (Fin M)), M / 2 ≤ S.card ∧ ∀ m ∈ S, Pe m ≤ 4 * ε

    Worst-half expurgation: if the sum of Pe m is bounded by M · (2ε), then at least M/2 indices m satisfy Pe m ≤ 4ε.

    Used by

      Power constraint and feasibility witness #

      The per-codeword power-constraint bound awgnPowerConstraintPerCodeword_holds lives in InformationTheory/Shannon/AWGN/PerCodewordPowerConstraint.lean. The achievability assembly also needs a shared slack witness ∃ P' ∈ (0, P) with R < capacity(P'), supplied by awgnPowerWitness_exists below, which returns a strict P' < P (the variance-level slack (P'.toNNReal : ℝ) < P required by the per-codeword bound).

      theorem

      InformationTheory.Shannon.AWGN.awgnPowerWitness_exists

      source
      (P : ℝ) (hP : 0 < P) (N : NNReal) (hN : ↑N ≠ 0) {R : ℝ} (hR_pos : 0 < R) (hR : R < 1 / 2 * Real.log (1 + P / ↑N)) :
      ∃ (P' : ℝ), 0 < P' ∧ P' < P ∧ R < 1 / 2 * Real.log (1 + P' / ↑N)

      The power-constraint slack witness.

      Given R < capacity(P) = (1/2) log(1 + P/N), produce a strictly smaller variance P' ∈ (0, P) for which the rate R is still below capacity(P'). The strict P' < P is genuinely required by awgnPowerConstraintPerCodeword_holds (its (P_cb.toNNReal : ℝ) < P_target slack argument); the witness must therefore deliver a true strict inequality, never a non-strict one fabricated from ≤.

      Construction: capacity is continuous and strictly increasing in the variance; R < capacity(P) lies strictly below the value at P, so by continuity there is a left neighbourhood of P on which the capacity still exceeds R. Picking any P' in that neighbourhood with 0 < P' < P works. @audit:ok

      Used by
        theorem

        InformationTheory.Shannon.AWGN.awgn_extract_AwgnCode

        source
        {P : ℝ} {N : NNReal} (h_meas : IsAwgnChannelMeasurable N) {n M : ℕ} [NeZero M] {ε : ℝ} (hε : 0 < ε) {A : Set ((Fin n → ℝ) × (Fin n → ℝ))} (hA_meas : MeasurableSet A) (codebook : Fin M → Fin n → ℝ) (h_max_Pe : ∀ (m : Fin M), (MeasureTheory.Measure.pi fun (i : Fin n) => (awgnChannel N h_meas) (codebook m i)) ({ encoder := codebook, decoder := jointTypicalDecoder A codebook }.errorEvent m) ≤ ENNReal.ofReal (4 * ε)) (h_power : ∀ (m : Fin M), ∑ i : Fin n, codebook m i ^ 2 ≤ ↑n * P) :
        ∃ (c : AwgnCode M n P), ∀ (m : Fin M), (c.toCode.errorProbAt (awgnChannel N h_meas) m).toReal < 5 * ε

        Bridge to the AwgnCode type from a deterministic codebook satisfying both the per-message error bound and the per-message power constraint, using jointTypicalDecoder as the decoder and converting the ℝ≥0∞-valued error bound to the < 5ε real-valued slack.

        Used by
          theorem

          InformationTheory.Shannon.AWGN.exists_two_mul_ceil_exp_le_ceil_exp_of_lt

          source
          {R R'' : ℝ} (hR_nonneg : 0 ≤ R) (hR_lt_R'' : R < R'') :
          ∃ (N₀ : ℕ), ∀ (n : ℕ), N₀ ≤ n → 2 * ⌈Real.exp (↑n * R)⌉₊ ≤ ⌈Real.exp (↑n * R'')⌉₊
          Used by