Skip to content

InformationTheory.Shannon.SlepianWolf.FullRateRegion.AliasBound

Imports 6

Generic measure-theoretic plumbing #

theorem

InformationTheory.Shannon.ChannelCoding.integrable_of_nonneg_le_one_of_discrete

{γ : Type u_4} [MeasurableSpace γ] [DiscreteMeasurableSpace γ] (ν : MeasureTheory.Measure γ) [MeasureTheory.IsFiniteMeasure ν] (g : γ → ℝ) (h_nn : ∀ (x : γ), 0 ≤ g x) (h_le : ∀ (x : γ), g x ≤ 1) :

MeasureTheory.Integrable g ν

Used by

theorem

InformationTheory.Shannon.ChannelCoding.lintegral_measure_le_ofReal_of_measureReal_le

{Ω' : Type u_4} {γ : Type u_5} [MeasurableSpace Ω'] [MeasurableSpace γ] (ν : MeasureTheory.Measure γ) [MeasureTheory.IsFiniteMeasure ν] (μ : MeasureTheory.Measure Ω') [MeasureTheory.IsProbabilityMeasure μ] (s : Ω' → Set γ) {K : ℝ} (hbound : ∀ (ω : Ω'), ν.real (s ω) ≤ K) :

∫⁻ (ω : Ω'), ν (s ω) ∂μ ≤ ENNReal.ofReal K

Used by

theorem

InformationTheory.Shannon.ChannelCoding.lintegral_ofReal_measureReal_eq_lintegral_measure

{Ω' : Type u_4} {γ : Type u_5} [MeasurableSpace Ω'] [MeasurableSpace γ] (μ : MeasureTheory.Measure Ω') [MeasureTheory.IsFiniteMeasure μ] (ν : MeasureTheory.Measure γ) (s : γ → Set Ω') :

∫⁻ (x : γ), ENNReal.ofReal (μ.real (s x)) ∂ν = ∫⁻ (x : γ), μ (s x) ∂ν

Used by

theorem

InformationTheory.Shannon.ChannelCoding.lintegral_measure_swap_of_prod_measurableSet

{Ω' : Type u_4} {γ : Type u_5} [MeasurableSpace Ω'] [MeasurableSpace γ] (ν : MeasureTheory.Measure γ) [MeasureTheory.SFinite ν] (μ : MeasureTheory.Measure Ω') [MeasureTheory.SFinite μ] (s : γ → Set Ω') (hE : MeasurableSet {q : γ × Ω' | q.2 ∈ s q.1}) :

∫⁻ (g : γ), μ (s g) ∂ν = ∫⁻ (ω : Ω'), ν {g : γ | ω ∈ s g} ∂μ

Used by

theorem

InformationTheory.Shannon.ChannelCoding.le_exp_of_mul_exp_neg_le

(c : ℝ) (n : ℕ) (HZ HX ε : ℝ) (hchain : c * Real.exp (-↑n * (HZ + ε)) ≤ Real.exp (-↑n * (HX - ε))) :

c ≤ Real.exp (↑n * (HZ - HX + 2 * ε))

Used by

Alias expectation bound #

The `E_X` expectation bound under random binning #

The expected μ-mass of the E_X error event over the random binning hash f_X ∼ binningMeasure α n M_X is bounded by the conditional-typical fiber size on the X axis divided by the bin count, exp(n · (H(X,Y) - H(Y) + 2ε)) / M_X. The proof swaps the order of integration (Fubini over μ ⊗ binningMeasure), applies binning_alias_expectation_le_aux to the per-ω collision slice, and bounds the slice cardinality by conditionalTypicalSlice_card_le.

theorem

InformationTheory.Shannon.ChannelCoding.swError_EX_expectation_le

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepY_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Ys i) μ) (hidentY : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Ys i) (Ys 0) μ μ) (hindepZ_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => jointSequence Xs Ys i) μ) (hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (jointSequence Xs Ys i) (jointSequence Xs Ys 0) μ μ) (hposY : ∀ (y : β), 0 < (MeasureTheory.Measure.map (Ys 0) μ).real {y}) (hposZ : ∀ (p : α × β), 0 < (MeasureTheory.Measure.map (jointSequence Xs Ys 0) μ).real {p}) {n M_X : ℕ} [NeZero M_X] {ε : ℝ} (hε : 0 < ε) :

∫ (f_X : (Fin n → α) → Fin M_X), μ.real (swError_EX μ Xs Ys n ε f_X) ∂binningMeasure α n M_X ≤ Real.exp (↑n * (entropy μ (jointSequence Xs Ys 0) - entropy μ (Ys 0) + 2 * ε)) * (↑M_X)⁻¹

Used by

The `E_Y` expectation bound under random binning #

The X/Y-symmetric counterpart of swError_EX_expectation_le, working with the Y-fiber slice {y' | (x, y') ∈ jointlyTypicalSet}. The expected μ-mass of the E_Y error event over f_Y ∼ binningMeasure β n M_Y is bounded by exp(n · (H(X,Y) - H(X) + 2ε)) / M_Y.

Y-fiber slice utility #

theorem

InformationTheory.Shannon.ChannelCoding.measureReal_map_jointRV_proj_fst_eq

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (n : ℕ) (x : Fin n → α) :

(MeasureTheory.Measure.map (jointRV (jointSequence Xs Ys) n) μ).real ((fun (z : Fin n → α × β) (i : Fin n) => (z i).1) ⁻¹' {x}) = (MeasureTheory.Measure.map (jointRV Xs n) μ).real {x}

Used by

Main statement — `E_Y` expectation bound. #

theorem

InformationTheory.Shannon.ChannelCoding.swError_EY_expectation_le

{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [Fintype β] [Nonempty β] [MeasurableSpace β] [MeasurableSingletonClass β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (Ys : ℕ → Ω → β) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hYs : ∀ (i : ℕ), Measurable (Ys i)) (hindepX_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hidentX : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hindepZ_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => jointSequence Xs Ys i) μ) (hidentZ : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (jointSequence Xs Ys i) (jointSequence Xs Ys 0) μ μ) (hposX : ∀ (x : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {x}) (hposZ : ∀ (p : α × β), 0 < (MeasureTheory.Measure.map (jointSequence Xs Ys 0) μ).real {p}) {n M_Y : ℕ} [NeZero M_Y] {ε : ℝ} (hε : 0 < ε) :

∫ (f_Y : (Fin n → β) → Fin M_Y), μ.real (swError_EY μ Xs Ys n ε f_Y) ∂binningMeasure β n M_Y ≤ Real.exp (↑n * (entropy μ (jointSequence Xs Ys 0) - entropy μ (Xs 0) + 2 * ε)) * (↑M_Y)⁻¹

Used by