InformationTheory.Shannon.ChannelCoding.ShannonTheoremMaxError.SmoothInstantiation

Imports 9

Achievability at the smooth channel — closed-form N #

Part file split from ShannonTheoremMaxError. Instantiates channel_coding_achievability at the smooth channel with an explicit N formula.

Smooth achievability with closed-form N #

channel_coding_achievability instantiated at p := pmfToMeasure (pSmooth p₀ δ_p) and W := Channel.smooth W δ. The instances hp_pos/hW_pos are derived internally via pSmooth_pos and Channel.smooth_pos. The existential ∃ N is collapsed to the closed-form channelCodingSmoothMinN V_X V_Y V_Z I_lb R ε' using the AEPRate lemmas.

noncomputable def

InformationTheory.Shannon.ChannelCoding.channelCodingSmoothMinN

source

(V_X V_Y V_Z I_lb R ε' : ℝ) :

ℕ

Closed-form N(V_X, V_Y, V_Z, I_lb, R, ε') for the smooth achievability theorem.

max (max N₁ N₂) 1 where N₁ = jointlyTypicalSetMinN V_X V_Y V_Z (ε'/2) ((I_lb - R)/6) and N₂ = expNegMulMinN ((I_lb - R)/2) (ε'/2). Uses a mutual information lower bound I_lb so that N₂ is a safe upper bound.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.ChannelCoding.jointlyTypicalSetMinN_le_channelCodingSmoothMinN

source

(V_X V_Y V_Z I_lb R ε' : ℝ) :

jointlyTypicalSetMinN V_X V_Y V_Z (ε' / 2) ((I_lb - R) / 6) ≤ channelCodingSmoothMinN V_X V_Y V_Z I_lb R ε'

Used by

theorem

InformationTheory.Shannon.ChannelCoding.expNegMulMinN_le_channelCodingSmoothMinN

source

(V_X V_Y V_Z I_lb R ε' : ℝ) :

expNegMulMinN ((I_lb - R) / 2) (ε' / 2) ≤ channelCodingSmoothMinN V_X V_Y V_Z I_lb R ε'

Used by

theorem

InformationTheory.Shannon.ChannelCoding.one_le_channelCodingSmoothMinN

source

(V_X V_Y V_Z I_lb R ε' : ℝ) :

1 ≤ channelCodingSmoothMinN V_X V_Y V_Z I_lb R ε'

Used by

theorem

InformationTheory.Shannon.ChannelCoding.iidAmbient_entropy_exponent_eq

source

entropy (iidAmbientMeasure p Wδ) (jointSequence iidXs iidYs 0) - entropy (iidAmbientMeasure p Wδ) (iidXs 0) - entropy (iidAmbientMeasure p Wδ) (iidYs 0) = -(mutualInfoOfChannel p Wδ).toReal

Used by

theorem

InformationTheory.Shannon.ChannelCoding.channel_coding_achievability_smooth_at_N_le

source

{α : Type u_1} {β : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (W : Channel α β) [ProbabilityTheory.IsMarkovKernel W] (p₀ : α → ℝ) (hp₀_mem : p₀ ∈ stdSimplex ℝ α) {δ_p : ℝ} (hδ_p_pos : 0 < δ_p) (hδ_p_le : δ_p ≤ 1) {δ : ℝ} (hδ_pos : 0 < δ) (hδ_le : δ ≤ 1) {R I_lb : ℝ} (hR_pos : 0 < R) (hR_lt_I_lb : R < I_lb) (hI_lb_le_I : I_lb ≤ (mutualInfoOfChannel (pmfToMeasure (pSmooth p₀ δ_p)) (W.smooth δ)).toReal) (V_X V_Y V_Z : ℝ) (hV_X : pmfLogVariance (iidAmbientMeasure (pmfToMeasure (pSmooth p₀ δ_p)) (W.smooth δ)) iidXs ≤ V_X) (hV_Y : pmfLogVariance (iidAmbientMeasure (pmfToMeasure (pSmooth p₀ δ_p)) (W.smooth δ)) iidYs ≤ V_Y) (hV_Z : pmfLogVariance (iidAmbientMeasure (pmfToMeasure (pSmooth p₀ δ_p)) (W.smooth δ)) (jointSequence iidXs iidYs) ≤ V_Z) {ε' : ℝ} (hε' : 0 < ε') (n : ℕ) :

channelCodingSmoothMinN V_X V_Y V_Z I_lb R ε' ≤ n → ∃ (M : ℕ) (_ : ⌈Real.exp (↑n * R)⌉₊ ≤ M) (c : Code M n α β), (c.averageErrorProb (W.smooth δ)).toReal < ε'

Smooth achievability with closed-form N: channel_coding_achievability with the existential N replaced by channelCodingSmoothMinN V_X V_Y V_Z I_lb R ε'.

The caller supplies axis-wise variance upper bounds V_X, V_Y, V_Z and a mutual-information lower bound I_lb.

Used by