InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.SeedLemmas

Imports 9

Smooth input distribution and capacity lower bound construction #

Constructs, from R < capacity W, a full-support smooth input distribution pSmooth p₀ δ_p and a smoothing radius δ_B > 0 such that R < I(pSmooth p₀ δ_p; Channel.smooth W δ).toReal for all δ ∈ (0, δ_B].

Implementation notes #

Uses continuous_mutualInfoOfChannel_right_smooth (continuity in δ for fixed p) and continuous_mutualInfoOfChannel_left (continuity in p for fixed W). Joint (p, δ) continuity is not needed: first find δ_p making I(pSmooth p₀ δ_p; W) > R, then find δ_B keeping I(pSmooth p₀ δ_p; W_smooth δ) > R for δ ∈ (0, δ_B].

theorem

InformationTheory.Shannon.ChannelCoding.exists_smooth_capacity_gt_uniform

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] {R : ℝ} (hR : R < capacity W) :

∃ p₀ ∈ stdSimplex ℝ α, ∃ (δ_B : ℝ), 0 < δ_B ∧ δ_B ≤ 1 ∧ ∃ (R₁ : ℝ), R < R₁ ∧ ∀ δ ∈ Set.Ioc 0 δ_B, R₁ < (mutualInfoOfChannel (pmfToMeasure p₀) (W.smooth δ)).toReal

From R < capacity W, extracts p₀ ∈ stdSimplex, δ_B ∈ (0, 1], and R₁ > R such that R₁ < I(p₀; W_smooth δ).toReal for all δ ∈ (0, δ_B].

Used by

theorem

InformationTheory.Shannon.ChannelCoding.pSmooth_smooth_capacity_gt_uniform

source

∃ p₀ ∈ stdSimplex ℝ α, ∃ (δ_p : ℝ) (δ_B : ℝ), 0 < δ_p ∧ δ_p ≤ 1 ∧ 0 < δ_B ∧ δ_B ≤ 1 ∧ ∃ (I_lb : ℝ), R < I_lb ∧ (∀ (a : α), 0 < pSmooth p₀ δ_p a) ∧ pSmooth p₀ δ_p ∈ stdSimplex ℝ α ∧ ∀ δ ∈ Set.Ioc 0 δ_B, I_lb < (mutualInfoOfChannel (pmfToMeasure (pSmooth p₀ δ_p)) (W.smooth δ)).toReal

From R < capacity W, extracts p₀, δ_p, δ_B and I_lb > R such that pSmooth p₀ δ_p has full support and I_lb < I(pSmooth p₀ δ_p; W_smooth δ).toReal for all δ ∈ (0, δ_B].

Used by