InformationTheory.Shannon.ChannelCoding.ConverseMemoryless
Channel coding converse — pure IsMemorylessChannel form #
Bridge lemmas deriving both IsMemorylessChannelStrong Markov axioms from
IsMemorylessChannel (γ-form: single Markov chain (X^{≠i}, Y^{≠i}) → X_i → Y_i).
Main definitions #
per_letter_markov_of_memoryless— derives per-letter Markov chain fromIsMemorylessChannel.outputs_cond_indep_of_memoryless— derives outputs conditional independence via the graphoid weak union lemmaisMarkovChain_weakUnion_left_to_conditionerand conditioner reshape.
Main statements #
channel_coding_converse_general_memoryless_pure— channel coding converse underIsMemorylessChannelalone (both axioms auto-derived).
Graphoid helper lemmas (file-scoped) #
InformationTheory.Shannon.ChannelCodingConverseGeneral.isMarkovChain_map_conditioner_measurableEquiv
source{Ω : Type u_1}
[MeasurableSpace Ω]
{Y : Type u_3}
[MeasurableSpace Y]
[StandardBorelSpace Y]
[Nonempty Y]
{X : Type u_5}
{Z : Type u_6}
{Z' : Type u_7}
[MeasurableSpace X]
[StandardBorelSpace X]
[Nonempty X]
[MeasurableSpace Z]
[StandardBorelSpace Z]
[Nonempty Z]
[MeasurableSpace Z']
[StandardBorelSpace Z']
[Nonempty Z']
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Ω → X)
(Zc' : Ω → Z')
(Yo : Ω → Y)
(hXs : Measurable Xs)
(hZc' : Measurable Zc')
(hYo : Measurable Yo)
(e : Z' ≃ᵐ Z)
(hmarkov : IsMarkovChain μ Xs (fun (ω : Ω) => e (Zc' ω)) Yo)
:
IsMarkovChain μ Xs Zc' Yo
Markov chain conditioner reshape via measurable equiv: if Markov μ Xs (e ∘ Z') Yo
and e : Z' ≃ᵐ Z, then Markov μ Xs Z' Yo.
Used by
Strong-axiom derivations from memoryless #
The per-letter Markov chain (per_letter_markov) is the simpler of the two
strong-axiom derivations; the harder outputs_cond_indep derivation requires the
graphoid weak union axiom.
InformationTheory.Shannon.ChannelCodingConverseGeneral.per_letter_markov_of_memoryless
source{Ω : Type u_1}
[MeasurableSpace Ω]
{n : ℕ}
{α : Type u_2}
[MeasurableSpace α]
[Nonempty α]
[StandardBorelSpace α]
{β : Type u_3}
[MeasurableSpace β]
[Nonempty β]
[StandardBorelSpace β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Fin n → Ω → α)
(Ys : Fin n → Ω → β)
(hXs : ∀ (i : Fin n), Measurable (Xs i))
(hYs : ∀ (i : Fin n), Measurable (Ys i))
(h_memo : IsMemorylessChannel μ Xs Ys)
(i : Fin n)
:
IsMarkovChain μ (fun (ω : Ω) (j : Fin n) => Xs j ω) (Xs i) (Ys i)
Per-letter Markov chain from memoryless: derive Markov μ (Xs full) (Xs i) (Ys i)
from IsMemorylessChannel.
Used by
InformationTheory.Shannon.ChannelCodingConverseGeneral.outputs_cond_indep_of_memoryless
source{Ω : Type u_1}
[MeasurableSpace Ω]
{n : ℕ}
{α : Type u_2}
[MeasurableSpace α]
[Nonempty α]
[StandardBorelSpace α]
{β : Type u_3}
[MeasurableSpace β]
[Nonempty β]
[StandardBorelSpace β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Xs : Fin n → Ω → α)
(Ys : Fin n → Ω → β)
(hXs : ∀ (i : Fin n), Measurable (Xs i))
(hYs : ∀ (i : Fin n), Measurable (Ys i))
(h_memo : IsMemorylessChannel μ Xs Ys)
(i : Fin n)
:
Outputs conditional independence from memoryless: derive
Markov μ Y^{≠i} (X^n) Y_i from IsMemorylessChannel.
Used by
Semi-pure main converse theorem #
InformationTheory.Shannon.ChannelCodingConverseGeneral.channel_coding_converse_general_memoryless_pure
source{Ω : Type u_1}
[MeasurableSpace Ω]
{n : ℕ}
{M : Type u_2}
[Fintype M]
[Nonempty M]
[MeasurableSpace M]
[MeasurableSingletonClass M]
[StandardBorelSpace M]
{α : Type u_3}
[Fintype α]
[Nonempty α]
[MeasurableSpace α]
[MeasurableSingletonClass α]
[StandardBorelSpace α]
{β : Type u_4}
[Fintype β]
[Nonempty β]
[MeasurableSpace β]
[MeasurableSingletonClass β]
[StandardBorelSpace β]
(μ : MeasureTheory.Measure Ω)
[MeasureTheory.IsProbabilityMeasure μ]
(Msg : Ω → M)
(encoder : M → Fin n → α)
(Ys : Fin n → Ω → β)
(decoder : (Fin n → β) → M)
(hMsg : Measurable Msg)
(hYs : ∀ (i : Fin n), Measurable (Ys i))
(hdecoder : Measurable decoder)
(hmarkov : IsMarkovChain μ Msg (fun (ω : Ω) => encoder (Msg ω)) fun (ω : Ω) (i : Fin n) => Ys i ω)
(h_memo : IsMemorylessChannel μ (fun (i : Fin n) (ω : Ω) => encoder (Msg ω) i) Ys)
(hMsg_uniform : MeasureTheory.Measure.map Msg μ = (↑(Fintype.card M))⁻¹ • MeasureTheory.Measure.count)
(hcard : 2 ≤ Fintype.card M)
(hMI_finite : (mutualInfo μ (fun (ω : Ω) => encoder (Msg ω)) fun (ω : Ω) (i : Fin n) => Ys i ω) ≠ ⊤)
:
Real.log ↑(Fintype.card M) ≤ ∑ i : Fin n, (mutualInfo μ (fun (ω : Ω) => encoder (Msg ω) i) (Ys i)).toReal + Real.binEntropy (MeasureFano.errorProb μ Msg (fun (ω : Ω) (i : Fin n) => Ys i ω) decoder) + MeasureFano.errorProb μ Msg (fun (ω : Ω) (i : Fin n) => Ys i ω) decoder * Real.log (↑(Fintype.card M) - 1)
Shannon's noisy channel coding theorem (converse, memoryless form):
the bound holds under h_memo : IsMemorylessChannel μ Xs Ys alone, with both Markov
axioms of the strong form (channel_coding_converse_general_memoryless_strong)
auto-derived from h_memo.