InformationTheory.Shannon.BroadcastChannel.Marton.MarkovCore.Receiver2

Imports 4

Marton's inner bound — the conditional AEP for receiver 2 #

The receiver-2 mirror of the conditional AEP: for whatever auxiliary and input blocks the encoder ends up transmitting, as long as their empirical type is close to the ambient (V₂, X)-law, the channel output makes the pair (V₂, Y₂) weakly jointly typical with probability close to one, and an input drawn letterwise from a type-pinned auxiliary pair inherits that pin. The broadcast channel is not degraded here, so the second receiver is an exact mirror of the first rather than a second tier.

The two receivers carry separate band constants, because the bands each of them pins are the entropies of its own output, so the radii they induce are unrelated. An assembly consuming both pins its blocks at the minimum of the two radii, which jointStronglyTypicalSet_mono_radius turns back into either pin.

Main definitions #

martonBandConst₂ — the Lipschitz factor of the three receiver-2 band pins.
martonStrongRadius₂ — the type radius at which the transmitted blocks must be pinned.
martonCoveringRadius₂ — the radius at which the selected auxiliary pair must be pinned.

Main statements #

marton_condAEP_jointlyTypical₂ — the conditional AEP: the channel output of a type-pinned (V₂, X)-block is jointly typical with the auxiliary word with probability ≥ 1 - tol.
marton_transmitted_stronglyTypical₂_le — the input drawn from a type-pinned auxiliary pair inherits the pin.
marton_condAEP_selected_avg₂_le — the two combined: the receiver-2 error term of a selected auxiliary pair, averaged over the input tier, is below any prescribed tolerance.

Coordinate laws of the Marton ambient measure — receiver 2 #

The Markov identity `V₂ — X — Y₂` #

The radius separation — receiver 2 #

noncomputable def

InformationTheory.Shannon.BroadcastChannel.Marton.martonBandConst₂

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [MeasurableSpace V₁] [Fintype V₂] [MeasurableSpace V₂] [Fintype α] [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) (K : ProbabilityTheory.Kernel (V₁ × V₂) α) (W : BCChannel α β₁ β₂) :

ℝ

The Lipschitz factor relating the type radius of the transmitted (V₂, X)-block to the width of the three entropy bands it has to pin. It is a separate constant from martonBandConst, since the bands it controls are the entropies of the second output.

@audit:ok

Equations

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

Instances For

Used by

noncomputable def

InformationTheory.Shannon.BroadcastChannel.Marton.martonStrongRadius₂

source

ℝ

The type radius at which the transmitted (V₂, X)-block has to be pinned for the second receiver's output bands to hold at radius ε. Like martonStrongRadius it is a computed term of ε, so the signatures downstream carry one radius only.

@audit:ok

Equations

InformationTheory.Shannon.BroadcastChannel.Marton.martonStrongRadius₂ pV K W ε = ε / (2 * (1 + InformationTheory.Shannon.BroadcastChannel.Marton.martonBandConst₂ pV K W))

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.martonStrongRadius₂_pos

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [DecidableEq V₁] [Nonempty V₁] [MeasurableSpace V₁] [MeasurableSingletonClass V₁] [Fintype V₂] [DecidableEq V₂] [Nonempty V₂] [MeasurableSpace V₂] [MeasurableSingletonClass V₂] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) (K : ProbabilityTheory.Kernel (V₁ × V₂) α) (W : BCChannel α β₁ β₂) {ε : ℝ} (hε : 0 < ε) :

0 < martonStrongRadius₂ pV K W ε

Used by

The three bands — receiver 2 #

The conditional AEP — receiver 2 #

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.marton_condAEP_jointlyTypical₂

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [DecidableEq V₁] [Nonempty V₁] [MeasurableSpace V₁] [MeasurableSingletonClass V₁] [Fintype V₂] [DecidableEq V₂] [Nonempty V₂] [MeasurableSpace V₂] [MeasurableSingletonClass V₂] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) [MeasureTheory.IsProbabilityMeasure pV] (K : ProbabilityTheory.Kernel (V₁ × V₂) α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] {ε tol : ℝ} (hε : 0 < ε) (htol : 0 < tol) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (v₂ : Fin n → V₂) (x : Fin n → α), (fun (i : Fin n) => (v₂ i, x i)) ∈ stronglyTypicalSet (martonAmbientMeasure pV K W) (ChannelCoding.jointSequence martonV₂s martonXs) n (martonStrongRadius₂ pV K W ε) → (MeasureTheory.Measure.pi fun (i : Fin n) => W (x i)).real {y : Fin n → β₁ × β₂ | (v₂, fun (i : Fin n) => (y i).2) ∉ ChannelCoding.jointlyTypicalSet (martonAmbientMeasure pV K W) martonV₂s martonY₂s n ε} ≤ tol

Whatever auxiliary word v₂ and input word x the encoder transmits, as long as their empirical type is pinned to the ambient (V₂, X)-law at radius martonStrongRadius₂, the channel output leaves the pair (v₂, y₂) outside the weakly jointly typical set with probability at most tol, for every block length past a threshold depending on ε and tol alone.

This is the receiver-2 mirror of marton_condAEP_jointlyTypical; the channel is not degraded, so the two receivers are related by exchanging the auxiliary and output coordinates alone.

@audit:ok

Used by

From a type-pinned auxiliary pair to a type-pinned transmitted pair — receiver 2 #

noncomputable def

InformationTheory.Shannon.BroadcastChannel.Marton.martonCoveringRadius₂

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [MeasurableSpace V₁] [Fintype V₂] [MeasurableSpace V₂] [Fintype α] [MeasurableSpace α] [MeasurableSpace β₁] [MeasurableSpace β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) (K : ProbabilityTheory.Kernel (V₁ × V₂) α) (W : BCChannel α β₁ β₂) (ε : ℝ) :

ℝ

The type radius at which the selected auxiliary pair has to be pinned for the transmitted (V₂, X) block to be pinned at martonStrongRadius₂. It mirrors martonCoveringRadius with the receiver-2 band constant; an assembly that needs both pins at once takes the minimum of the two radii and reopens each of them with jointStronglyTypicalSet_mono_radius.

@audit:ok

Equations

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

Instances For

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.martonCoveringRadius₂_pos

source

0 < martonCoveringRadius₂ pV K W ε

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.marton_transmitted_stronglyTypical₂_le

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [DecidableEq V₁] [Nonempty V₁] [MeasurableSpace V₁] [MeasurableSingletonClass V₁] [Fintype V₂] [DecidableEq V₂] [Nonempty V₂] [MeasurableSpace V₂] [MeasurableSingletonClass V₂] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) [MeasureTheory.IsProbabilityMeasure pV] (K : ProbabilityTheory.Kernel (V₁ × V₂) α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] {ε tol : ℝ} (hε : 0 < ε) (htol : 0 < tol) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (v₁ : Fin n → V₁) (v₂ : Fin n → V₂), (v₁, v₂) ∈ jointStronglyTypicalSet (martonAmbientMeasure pV K W) martonV₁s martonV₂s n (martonCoveringRadius₂ pV K W ε) → (MeasureTheory.Measure.pi fun (i : Fin n) => K (v₁ i, v₂ i)).real {x : Fin n → α | (fun (i : Fin n) => (v₂ i, x i)) ∉ stronglyTypicalSet (martonAmbientMeasure pV K W) (ChannelCoding.jointSequence martonV₂s martonXs) n (martonStrongRadius₂ pV K W ε)} ≤ tol

The transmitted (V₂, X) block inherits the type pin of the selected auxiliary pair: drawing the input word letterwise from K applied to a pair whose joint type is pinned at martonCoveringRadius₂ leaves the pair (v₂, x) outside the strongly typical set of radius martonStrongRadius₂ with probability at most tol, uniformly in the selected pair.

@audit:ok

Used by

theorem

InformationTheory.Shannon.BroadcastChannel.Marton.marton_condAEP_selected_avg₂_le

source

{V₁ : Type u_1} {V₂ : Type u_2} {α : Type u_3} {β₁ : Type u_4} {β₂ : Type u_5} [Fintype V₁] [DecidableEq V₁] [Nonempty V₁] [MeasurableSpace V₁] [MeasurableSingletonClass V₁] [Fintype V₂] [DecidableEq V₂] [Nonempty V₂] [MeasurableSpace V₂] [MeasurableSingletonClass V₂] [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] [Fintype β₁] [DecidableEq β₁] [Nonempty β₁] [MeasurableSpace β₁] [MeasurableSingletonClass β₁] [Fintype β₂] [DecidableEq β₂] [Nonempty β₂] [MeasurableSpace β₂] [MeasurableSingletonClass β₂] (pV : MeasureTheory.Measure (V₁ × V₂)) [MeasureTheory.IsProbabilityMeasure pV] (K : ProbabilityTheory.Kernel (V₁ × V₂) α) [ProbabilityTheory.IsMarkovKernel K] (W : BCChannel α β₁ β₂) [ProbabilityTheory.IsMarkovKernel W] {ε tol : ℝ} (hε : 0 < ε) (htol : 0 < tol) :

∃ (N : ℕ), ∀ (n : ℕ), N ≤ n → ∀ (v₁ : Fin n → V₁) (v₂ : Fin n → V₂), (v₁, v₂) ∈ jointStronglyTypicalSet (martonAmbientMeasure pV K W) martonV₁s martonV₂s n (martonCoveringRadius₂ pV K W ε) → ∑ x : Fin n → α, (MeasureTheory.Measure.pi fun (i : Fin n) => K (v₁ i, v₂ i)).real {x} * (MeasureTheory.Measure.pi fun (i : Fin n) => W (x i)).real {y : Fin n → β₁ × β₂ | (v₂, fun (i : Fin n) => (y i).2) ∉ ChannelCoding.jointlyTypicalSet (martonAmbientMeasure pV K W) martonV₂s martonY₂s n ε} ≤ tol

The receiver-2 error term of a selected auxiliary pair, averaged over the input tier: whatever type-pinned pair the encoder selects, drawing the input word from K and passing it through the channel leaves (v₂, y₂) outside the weakly jointly typical set with probability at most tol.

This is the form the error decomposition of Marton.ErrorAnalysis consumes, since the threshold is uniform in the selected pair and hence in the code.

@audit:ok

Used by

InformationTheory.Shannon.BroadcastChannel.Marton.MarkovCore.Receiver2

Marton's inner bound — the conditional AEP for receiver 2 #

Main definitions #

Main statements #

Coordinate laws of the Marton ambient measure — receiver 2 #

The Markov identity V₂ — X — Y₂ #

The radius separation — receiver 2 #

The three bands — receiver 2 #

The conditional AEP — receiver 2 #

From a type-pinned auxiliary pair to a type-pinned transmitted pair — receiver 2 #

The Markov identity `V₂ — X — Y₂` #