InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.OuterN
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]with2 n δ_n < ε/2(so the TV bound contributes ≤ε/2); - build a code at the smooth channel
W_smooth δ_nwithmax-error < ε/2.
The construction:
- The uniform smooth-capacity bound gives
p_full := pSmooth p₀ δ_p(full support) withR < I_lb < I(p_full; W_smooth δ)for allδ ∈ (0, δ_B]. - Choose an interior rate
R' := (R + I_lb)/2 < I_lbfor the closed-form average-error code; we then upgrade to max-error at rateRvia the subcode trick (givingmax-error ≤ 2 · avg < ε/2). - Choose
δ_n := min(δ_B, ε/(16(n+1)))and check2 n δ_n < ε/4 < ε/2. - Bound
V_Y(δ_n), V_Z(δ_n) ≤ const + 2 · (log(n+1))²via the closed-form pmfLog bounds, using1/δ_n ≤ (1/δ_B + 16/ε)·(n+1)and(a+b)² ≤ 2a²+2b². - The closed-form
channelCodingSmoothMinNis thenO((log(n+1))²);exists_N_log_sq_plus_const_le_nproduces the outerN₀.
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)
:
Used by
InformationTheory.Shannon.ChannelCoding.pSmooth_ge
source{α : Type u_1}
[Fintype α]
{p₀ : α → ℝ}
(hp₀ : p₀ ∈ stdSimplex ℝ α)
{δ : ℝ}
(_hδ_pos : 0 < δ)
(hδ_le : δ ≤ 1)
(a : α)
:
Every entry of pSmooth p₀ δ is at least δ / |α|.
Used by
InformationTheory.Shannon.ChannelCoding.one_div_smooth_n_le
sourceFor δ_n := min(δ_B, ε/(16(n+1))), 1/δ_n ≤ (1/δ_B + 16/ε)·(n+1).
Used by
InformationTheory.Shannon.ChannelCoding.typicalSetMinN_le_div_add_two
sourceUsed by
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
InformationTheory.Shannon.ChannelCoding.two_mul_lt_half_of_le_div
sourceUsed by
InformationTheory.Shannon.ChannelCoding.sq_le_two_mul_sq_add_two_mul_sq_of_nonneg_of_le_add
sourceUsed by
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))
:
Used by
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)
:
Used by
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)
:
Used by
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)
{ε : ℝ}
(hε : 0 < ε)
:
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.