InformationTheory

InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.OuterN

source

Outer N construction — max-error closed form #

Part file split from ShannonTheoremMaxError. Constructs the outer N₀ that simultaneously controls the TV smoothing error and the smooth-channel achievability.

Outer N construction #

For any R < capacity W and ε > 0, we build an N₀ such that for every n ≥ N₀ we can simultaneously:

  • pick δ_n ∈ (0, δ_B] with 2 n δ_n < ε/2 (so the TV bound contributes ≤ ε/2);
  • build a code at the smooth channel W_smooth δ_n with max-error < ε/2.

The construction:

  1. The uniform smooth-capacity bound gives p_full := pSmooth p₀ δ_p (full support) with R < I_lb < I(p_full; W_smooth δ) for all δ ∈ (0, δ_B].
  2. Choose an interior rate R' := (R + I_lb)/2 < I_lb for the closed-form average-error code; we then upgrade to max-error at rate R via the subcode trick (giving max-error ≤ 2 · avg < ε/2).
  3. Choose δ_n := min(δ_B, ε/(16(n+1))) and check 2 n δ_n < ε/4 < ε/2.
  4. Bound V_Y(δ_n), V_Z(δ_n) ≤ const + 2 · (log(n+1))² via the closed-form pmfLog bounds, using 1/δ_n ≤ (1/δ_B + 16/ε)·(n+1) and (a+b)² ≤ 2a²+2b².
  5. The closed-form channelCodingSmoothMinN is then O((log(n+1))²); exists_N_log_sq_plus_const_le_n produces the outer N₀.
theorem

InformationTheory.Shannon.ChannelCoding.one_le_mul_div_mul_of_le_one

source
{a b p d : } (ha : 1 a) (hb : 1 b) (hp_pos : 0 < p) (hp_le : p 1) (hd_pos : 0 < d) (hd_le : d 1) :
1 a * b / (p * d)
Used by
    theorem

    InformationTheory.Shannon.ChannelCoding.pSmooth_ge

    source
    {α : Type u_1} [Fintype α] {p₀ : α} (hp₀ : p₀ stdSimplex α) {δ : } (_hδ_pos : 0 < δ) (hδ_le : δ 1) (a : α) :
    δ / (Fintype.card α) pSmooth p₀ δ a

    Every entry of pSmooth p₀ δ is at least δ / |α|.

    Used by
      theorem

      InformationTheory.Shannon.ChannelCoding.one_div_smooth_n_le

      source
      {δ_B ε : } (hδ_B_pos : 0 < δ_B) (hε_pos : 0 < ε) (n : ) :
      have δ_n := min δ_B (ε / (16 * (n + 1))); 1 / δ_n (1 / δ_B + 16 / ε) * (n + 1)

      For δ_n := min(δ_B, ε/(16(n+1))), 1/δ_n ≤ (1/δ_B + 16/ε)·(n+1).

      Used by
        theorem

        InformationTheory.Shannon.ChannelCoding.typicalSetMinN_le_div_add_two

        source
        {η ε : } (hηε : 0 < η * ε ^ 2) {V : } (hV : 0 V) :
        (typicalSetMinN V η ε) V / (η * ε ^ 2) + 2
        Used by
          theorem

          InformationTheory.Shannon.ChannelCoding.log_div_le_log_add_log_add_log_succ

          source
          {c s δ m : } (hc_pos : 0 < c) (hs_pos : 0 < s) (hδ_pos : 0 < δ) (hm1_pos : 0 < m + 1) (h_one_div_le : 1 / δ s * (m + 1)) :
          Used by
            theorem

            InformationTheory.Shannon.ChannelCoding.two_mul_lt_half_of_le_div

            source
            {ε δ : } ( : 0 < ε) (n : ) (hn1_pos : 0 < n + 1) (hδ_le : δ ε / (16 * (n + 1))) :
            2 * n * δ < ε / 2
            Used by
              theorem

              InformationTheory.Shannon.ChannelCoding.sq_le_two_mul_sq_add_two_mul_sq_of_nonneg_of_le_add

              source
              {x K y : } (hx : 0 x) (hxle : x K + y) :
              x ^ 2 2 * K ^ 2 + 2 * y ^ 2
              Used by
                theorem

                InformationTheory.Shannon.ChannelCoding.logSq_div_le_two_sq_add_two_logSq

                source
                {c s δ m : } (hc : 1 c) (hs_pos : 0 < s) (hδ_pos : 0 < δ) (hδ_le : δ 1) (hm1_pos : 0 < m + 1) (h_one_div_le : 1 / δ s * (m + 1)) :
                Real.log (c / δ) ^ 2 2 * (Real.log c + Real.log s) ^ 2 + 2 * Real.log (m + 1) ^ 2
                Used by
                  theorem

                  InformationTheory.Shannon.ChannelCoding.typicalSetMinN_real_le_two_coef_logSq_add

                  source
                  {V A Lsq C D η3 εg : } (hs : 0 < η3 * εg ^ 2) (hV : 0 V) (hVA : V A + 2 * Lsq) (hLsq : 0 Lsq) (hC : C = 2 / (η3 * εg ^ 2)) (hD : A / (η3 * εg ^ 2) + 2 D) :
                  (typicalSetMinN V η3 εg) 2 * C * Lsq + D
                  Used by
                    theorem

                    InformationTheory.Shannon.ChannelCoding.channelCodingSmoothMinN_real_le_two_coef_logSq_add

                    source
                    {V_X V_Y V_Z A_Y A_Z Lsq C D η3 εg I_lb R' ε' : } (hη3 : η3 = ε' / 2 / 3) (hεg : εg = (I_lb - R') / 6) (hs : 0 < η3 * εg ^ 2) (hVX : 0 V_X) (hVY : V_Y A_Y + 2 * Lsq) (hVZ : V_Z A_Z + 2 * Lsq) (hLsq : 0 Lsq) (hVY_nn : 0 V_Y) (hVZ_nn : 0 V_Z) (hC : C = 2 / (η3 * εg ^ 2)) (hDX : V_X / (η3 * εg ^ 2) + 2 D) (hDY : A_Y / (η3 * εg ^ 2) + 2 D) (hDZ : A_Z / (η3 * εg ^ 2) + 2 D) (hDexp : (expNegMulMinN ((I_lb - R') / 2) (ε' / 2)) D) (hD1 : 1 D) (hCLsq : 0 2 * C * Lsq) :
                    (channelCodingSmoothMinN V_X V_Y V_Z I_lb R' ε') 2 * C * Lsq + D
                    Used by
                      theorem

                      InformationTheory.Shannon.ChannelCoding.exists_N_for_smooth_achievability_uniform

                      source
                      {α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {R : } (hR_pos : 0 < R) (hR : R < capacity W) {ε : } ( : 0 < ε) :
                      ∃ (N : ), ∀ (n : ), N n∃ (δ : ) (_ : 0 < δ) (_ : δ 1), 2 * n * δ < ε / 2 ∃ (M : ) (_ : Real.exp (n * R)⌉₊ M) (c : Code M n α β), ∀ (m : Fin M), (c.errorProbAt (W.smooth δ) m).toReal < ε / 2

                      For any R < capacity W and ε > 0, there exists N₀ such that for all n ≥ N₀ one can pick δ_n with 2 n δ_n < ε/2 and a code at the smooth channel Channel.smooth W δ_n achieving max-error less than ε/2.

                      Used by