InformationTheory.Shannon.RateDistortion.AchievabilityStrongTypicality.FailureTendstoZero

Imports 8

Rate-distortion achievability (strong-typicality variant) — failure probability tends to zero #

The main probabilistic content codebookAvgFailureStrong_tendsto_zero. Carries the codebook-averaged random-coding failure probability to zero; the final assembly lives in AchievabilityStrongTypicality.lean.

theorem

InformationTheory.Shannon.measureReal_prod_eq_measureReal_prod_swap_image

source

{γ₁ : Type u_4} {γ₂ : Type u_5} [MeasurableSpace γ₁] [MeasurableSpace γ₂] (μ : MeasureTheory.Measure γ₁) (ν : MeasureTheory.Measure γ₂) [MeasureTheory.SFinite μ] [MeasureTheory.SFinite ν] {S : Set (γ₁ × γ₂)} (hS : MeasurableSet S) :

(μ.prod ν).real S = (ν.prod μ).real (Prod.swap '' S)

Used by

theorem

InformationTheory.Shannon.sum_weighted_le_const_add_sum_weighted_of_le_add

source

{ι : Type u_4} [Fintype ι] (w f g : ι → ℝ) (A : ℝ) (hw_nonneg : ∀ (i : ι), 0 ≤ w i) (hw_sum : ∑ i : ι, w i = 1) (h_le : ∀ (i : ι), f i ≤ A + g i) :

∑ i : ι, w i * f i ≤ A + ∑ i : ι, w i * g i

Used by

theorem

InformationTheory.Shannon.measureReal_le_add_measureReal_of_subset_union

source

{γ : Type u_4} [MeasurableSpace γ] (μ : MeasureTheory.Measure γ) [MeasureTheory.IsFiniteMeasure μ] {S A B : Set γ} (hS : S ⊆ A ∪ B) :

μ.real S ≤ μ.real A + μ.real B

Used by

theorem

InformationTheory.Shannon.measureReal_prod_eq_sum_measureReal_singleton_mul_measureReal_section

source

{ι : Type u_4} {γ : Type u_5} [MeasurableSpace ι] [Fintype ι] [MeasurableSingletonClass ι] [MeasurableSpace γ] (μ : MeasureTheory.Measure ι) (ν : MeasureTheory.Measure γ) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {R : Set (ι × γ)} (hR : MeasurableSet R) :

(μ.prod ν).real R = ∑ c : ι, μ.real {c} * ν.real (Prod.mk c ⁻¹' R)

Used by

theorem

InformationTheory.Shannon.measureReal_prod_le_of_measure_section_le_ofReal

source

{γ₁ : Type u_4} {γ₂ : Type u_5} [MeasurableSpace γ₁] [MeasurableSpace γ₂] (μ : MeasureTheory.Measure γ₁) (ν : MeasureTheory.Measure γ₂) [MeasureTheory.IsProbabilityMeasure μ] [MeasureTheory.SFinite ν] {R : Set (γ₁ × γ₂)} (hR : MeasurableSet R) (b : ℝ) (hb : 0 ≤ b) (h_section : ∀ (x : γ₁), ν (Prod.mk x ⁻¹' R) ≤ ENNReal.ofReal b) :

(μ.prod ν).real R ≤ b

Used by

theorem

InformationTheory.Shannon.tendsto_measureReal_compl_zero_of_tendsto_measure_one

source

{Ω : Type u_4} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (E : ℕ → Set Ω) (hE_meas : ∀ (n : ℕ), MeasurableSet (E n)) (hE : Filter.Tendsto (fun (n : ℕ) => μ (E n)) Filter.atTop (nhds 1)) :

Filter.Tendsto (fun (n : ℕ) => (μ (E n)ᶜ).toReal) Filter.atTop (nhds 0)

Used by

theorem

InformationTheory.Shannon.weightedSum_section_pred_le_of_section_measure_le

source

{κ : Type u_4} {ι : Type u_5} [MeasurableSpace κ] [Fintype κ] [MeasurableSingletonClass κ] [MeasurableSpace ι] (W : MeasureTheory.Measure κ) [MeasureTheory.IsProbabilityMeasure W] (Q : MeasureTheory.Measure ι) [MeasureTheory.IsProbabilityMeasure Q] (Pred : κ → ι → Prop) (hPred_meas_x : ∀ (c : κ), MeasurableSet {x : ι | Pred c x}) (hPred_meas_prod : MeasurableSet {p : κ × ι | Pred p.1 p.2}) (b : ℝ) (hb : 0 ≤ b) (h_section_bound : ∀ (x : ι), W {c : κ | Pred c x} ≤ ENNReal.ofReal b) :

∑ c : κ, W.real {c} * Q.real {x : ι | Pred c x} ≤ b

Used by

theorem

InformationTheory.Shannon.piMeasure_section_no_match_le_of_typical

source

{ιx : Type u_4} {M : Type u_5} [MeasurableSpace ιx] [Fintype M] {γ : Type u_6} [MeasurableSpace γ] [MeasurableSingletonClass γ] (p : MeasureTheory.Measure γ) [MeasureTheory.IsProbabilityMeasure p] (Match : (M → γ) → ιx → Prop) [(c : M → γ) → DecidablePred fun (x : ιx) => Match c x] (T_X : Set ιx) (b : ℝ) (hb : 0 ≤ b) (h_typical : ∀ x ∈ T_X, (MeasureTheory.Measure.pi fun (x : M) => p).real {c : M → γ | ¬Match c x} ≤ b) (x : ιx) :

(MeasureTheory.Measure.pi fun (x : M) => p) {c : M → γ | x ∈ T_X ∧ ¬Match c x} ≤ ENNReal.ofReal b

Used by

theorem

InformationTheory.Shannon.encoderFailure_subset_notTypical_union_noMatch

source

{ιx : Type u_4} {ιy : Type u_5} (T_X : Set ιx) (DTS JSTS : Set (ιx × ιy)) {M : Type u_6} (c : M → ιy) (enc : ιx → M) (hJTS_subset : ∀ x ∈ T_X, ∀ (y : ιy), (x, y) ∈ JSTS → (x, y) ∈ DTS) (hEnc_spec : ∀ (x : ιx), (∃ (m : M), (x, c m) ∈ JSTS) → (x, c (enc x)) ∈ JSTS) :

{x : ιx | (x, c (enc x)) ∉ DTS} ⊆ {x : ιx | x ∉ T_X} ∪ {x : ιx | x ∈ T_X ∧ ¬∃ (m : M), (x, c m) ∈ JSTS}

Used by

theorem

InformationTheory.Shannon.tendsto_measureReal_map_notMem_zero_of_tendsto_prob_one

source

{Ω : Type u_4} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {ιx : ℕ → Type u_5} [(n : ℕ) → MeasurableSpace (ιx n)] (jr : (n : ℕ) → Ω → ιx n) (hjr : ∀ (n : ℕ), Measurable (jr n)) (S : (n : ℕ) → Set (ιx n)) (hS : ∀ (n : ℕ), MeasurableSet (S n)) (Pn : (n : ℕ) → MeasureTheory.Measure (ιx n)) (hPn : ∀ (n : ℕ), MeasureTheory.Measure.map (jr n) μ = Pn n) (h_aep : Filter.Tendsto (fun (n : ℕ) => μ {ω : Ω | jr n ω ∈ S n}) Filter.atTop (nhds 1)) :

Filter.Tendsto (fun (n : ℕ) => (Pn n).real {x : ιx n | x ∉ S n}) Filter.atTop (nhds 0)

Used by

theorem

InformationTheory.Shannon.weightedSum_fail_le_const_add_of_per_index_and_sum_bound

source

{κ : Type u_4} [MeasurableSpace κ] [Fintype κ] [MeasurableSingletonClass κ] (W : MeasureTheory.Measure κ) [MeasureTheory.IsProbabilityMeasure W] (fail g : κ → ℝ) (A bound : ℝ) (h_per : ∀ (c : κ), fail c ≤ A + g c) (h_sum_g : ∑ c : κ, W.real {c} * g c ≤ bound) :

∑ c : κ, W.real {c} * fail c ≤ A + bound

Used by

theorem

InformationTheory.Shannon.measureReal_encoderFailure_le_notTypical_add_noMatch

source

{ιx : Type u_4} {ιy : Type u_5} [MeasurableSpace ιx] (Q : MeasureTheory.Measure ιx) [MeasureTheory.IsFiniteMeasure Q] (T_X : Set ιx) (DTS JSTS : Set (ιx × ιy)) {M : Type u_6} (c : M → ιy) (enc : ιx → M) (hJTS_subset : ∀ x ∈ T_X, ∀ (y : ιy), (x, y) ∈ JSTS → (x, y) ∈ DTS) (hEnc_spec : ∀ (x : ιx), (∃ (m : M), (x, c m) ∈ JSTS) → (x, c (enc x)) ∈ JSTS) :

Q.real {x : ιx | (x, c (enc x)) ∉ DTS} ≤ Q.real {x : ιx | x ∉ T_X} + Q.real {x : ιx | x ∈ T_X ∧ ¬∃ (m : M), (x, c m) ∈ JSTS}

Used by

theorem

InformationTheory.Shannon.weightedSum_noMatch_le_of_typical

source

{ιx : Type u_4} {M : Type u_5} [MeasurableSpace ιx] [Fintype M] [DecidableEq M] [MeasurableSpace M] {γ : Type u_6} [Fintype γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (p : MeasureTheory.Measure γ) [MeasureTheory.IsProbabilityMeasure p] (Q : MeasureTheory.Measure ιx) [MeasureTheory.IsProbabilityMeasure Q] (T_X : Set ιx) (Match : (M → γ) → ιx → Prop) [(c : M → γ) → DecidablePred fun (x : ιx) => Match c x] (hMeas_x : ∀ (c : M → γ), MeasurableSet {x : ιx | x ∈ T_X ∧ ¬Match c x}) (hMeas_prod : MeasurableSet {q : (M → γ) × ιx | q.2 ∈ T_X ∧ ¬Match q.1 q.2}) (b : ℝ) (hb : 0 ≤ b) (h_typical : ∀ x ∈ T_X, (MeasureTheory.Measure.pi fun (x : M) => p).real {c : M → γ | ¬Match c x} ≤ b) :

∑ c : M → γ, (MeasureTheory.Measure.pi fun (x : M) => p).real {c} * Q.real {x : ιx | x ∈ T_X ∧ ¬Match c x} ≤ b

Used by

theorem

InformationTheory.Shannon.encoder_strong_failure_prob_le_rdAmbient

source

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (M : ℕ), ∀ x ∈ stronglyTypicalSet (rdAmbient qStar) ChannelCoding.iidXs n ε_X, (MeasureTheory.Measure.pi fun (x : Fin M) => MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.Measure.map (ChannelCoding.iidYs 0) (rdAmbient qStar)).real {c : Fin M → Fin n → β | ∀ (m : Fin M), (x, c m) ∉ jointStronglyTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs n ε_join} ≤ Real.exp (-↑M * Real.exp (-↑n * (entropy (rdAmbient qStar) (ChannelCoding.iidXs 0) + entropy (rdAmbient qStar) (ChannelCoding.iidYs 0) - entropy (rdAmbient qStar) (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs 0) + (↑(Fintype.card α) * ε_X * logSumAbs (rdAmbient qStar) ChannelCoding.iidYs + ε_X * logSumAbs (rdAmbient qStar) ChannelCoding.iidXs + ε_X * logSumAbs (rdAmbient qStar) (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs) + δ_kl))))

Used by

theorem

InformationTheory.Shannon.weightedSum_encoderFailure_le_notTypical_add_bound

source

{ιx : Type u_4} {M : Type u_5} [MeasurableSpace ιx] [Fintype M] [DecidableEq M] [MeasurableSpace M] {γ : Type u_6} [Fintype γ] [MeasurableSpace γ] [MeasurableSingletonClass γ] (Q : MeasureTheory.Measure ιx) [MeasureTheory.IsProbabilityMeasure Q] (p : MeasureTheory.Measure γ) [MeasureTheory.IsProbabilityMeasure p] (T_X : Set ιx) (DTS JSTS : Set (ιx × γ)) (enc : (M → γ) → ιx → M) (b : ℝ) (hb : 0 ≤ b) (hMeas_x : ∀ (c : M → γ), MeasurableSet {x : ιx | x ∈ T_X ∧ ¬∃ (m : M), (x, c m) ∈ JSTS}) (hMeas_prod : MeasurableSet {q : (M → γ) × ιx | q.2 ∈ T_X ∧ ¬∃ (m : M), (q.2, q.1 m) ∈ JSTS}) (hJTS_subset : ∀ x ∈ T_X, ∀ (y : γ), (x, y) ∈ JSTS → (x, y) ∈ DTS) (hEnc_spec : ∀ (c : M → γ) (x : ιx), (∃ (m : M), (x, c m) ∈ JSTS) → (x, c (enc c x)) ∈ JSTS) (h_typical : ∀ x ∈ T_X, (MeasureTheory.Measure.pi fun (x : M) => p).real {c : M → γ | ¬∃ (m : M), (x, c m) ∈ JSTS} ≤ b) :

∑ c : M → γ, (MeasureTheory.Measure.pi fun (x : M) => p).real {c} * Q.real {x : ιx | (x, c (enc c x)) ∉ DTS} ≤ Q.real {x : ιx | x ∉ T_X} + b

Used by

theorem

InformationTheory.Shannon.exp_neg_ceilExp_mul_tendsto_zero_of_lt

source

(target : ℕ → ℝ) (R θ : ℝ) (hθ_lt : θ < R) (h_target_eq : ∀ (n : ℕ), target n = Real.exp (-↑n * θ)) :

Filter.Tendsto (fun (n : ℕ) => Real.exp (-(↑⌈Real.exp (↑n * R)⌉₊ * target n))) Filter.atTop (nhds 0)

Used by

Main probabilistic content: `codebookAvgFailureStrong → 0` #

theorem

InformationTheory.Shannon.codebookAvgFailureStrong_tendsto_zero

source

{α : Type u_2} {β : Type u_3} [MeasurableSpace α] [MeasurableSpace β] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSingletonClass α] [Fintype β] [DecidableEq β] [Nonempty β] [MeasurableSingletonClass β] (qStar : α × β → ℝ) (hqStar_simp : qStar ∈ stdSimplex ℝ (α × β)) (hqStar_pos : ∀ (p : α × β), 0 < qStar p) (d : DistortionFn α β) {R : ℝ} (hI_lt_R : mutualInfoPmf qStar < R) (ε_dist δ_typ : ℝ) (hε_dist_pos : 0 < ε_dist) (hδ_typ_nn : 0 ≤ δ_typ) (ε_X ε_join δ_kl : ℝ) (hε_X_pos : 0 < ε_X) (hε_join_pos : 0 < ε_join) (hδ_kl_pos : 0 < δ_kl) (hε_X_lt_ε_join : ε_X < ε_join) (h_rate_gap : mutualInfoPmf qStar + (↑(Fintype.card α) * ε_X * logSumAbs (rdAmbient qStar) ChannelCoding.iidYs + ε_X * logSumAbs (rdAmbient qStar) ChannelCoding.iidXs + ε_X * logSumAbs (rdAmbient qStar) (ChannelCoding.jointSequence ChannelCoding.iidXs ChannelCoding.iidYs) + δ_kl) < R) (h_dist_slack : ε_join * ∑ p : α × β, ↑(d p.1 p.2) ≤ δ_typ) (h_jts_subset_dts : ∀ {n : ℕ}, 0 < n → ∀ (x : Fin n → α) (y : Fin n → β), (x, y) ∈ jointStronglyTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs n ε_join → (x, y) ∈ distortionTypicalSet (rdAmbient qStar) ChannelCoding.iidXs ChannelCoding.iidYs d n ε_dist δ_typ) (qZ_min : ℝ) (hqZ_min_pos : 0 < qZ_min) (hqZ_min_le : ∀ (p : α × β), qZ_min ≤ (ChannelCoding.pmfToMeasure qStar).real {p}) (hδ_kl_dominates : 8 * ↑(Fintype.card α) * ↑(Fintype.card β) * ε_X ^ 2 ≤ δ_kl * qZ_min) :

Filter.Tendsto (fun (n : ℕ) => codebookAvgFailureStrong qStar d R n ε_join ε_dist δ_typ) Filter.atTop (nhds 0)

Main tendsto_zero for the strong-encoder failure sequence.

Hypotheses:

hqStar_pos : ∀ p, 0 < qStar p — strict positivity of qStar on α × β, required by conditionalStronglyTypicalSlice_mass_ge.
Slack parameters ε_X, ε_join, δ_kl and the slack-budget hypotheses h_rate_gap (strict rate over mutualInfoPmf + slacks) and the bridge slacks for jointStronglyTypicalSet ⊆ distortionTypicalSet.

The proof is a conditional method-of-types AEP combined with joint strong typicality.

Used by

InformationTheory.Shannon.RateDistortion.AchievabilityStrongTypicality.FailureTendstoZero

Rate-distortion achievability (strong-typicality variant) — failure probability tends to zero #

Main probabilistic content: codebookAvgFailureStrong → 0 #

Main probabilistic content: `codebookAvgFailureStrong → 0` #