InformationTheory

InformationTheory.Shannon.AEP.Basic.Converse

source

Imports 16

Source-coding theorem, weak converse #

The source-coding converse (Cover-Thomas) is stated in Filter.liminf form. The block entropy identity H(X^n) = n · H(X) is not available from the Pairwise IndepFun hypothesis used elsewhere in this family, so the converse takes mutual independence (iIndepFun) as a hypothesis.

I.i.d. block entropy chain rule #

theorem

InformationTheory.Shannon.condEntropy_eq_entropy_of_indepFun

source
{Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {β : Type u_3} [MeasurableSpace β] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : Ω → α) (Y : Ω → β) (hX : Measurable X) (hY : Measurable Y) (hindep : ProbabilityTheory.IndepFun X Y μ) :
MeasureFano.condEntropy μ X Y = entropy μ X
Used by
    theorem

    InformationTheory.Shannon.entropy_eq_of_identDistrib

    source
    {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [MeasurableSpace α] {Ω' : Type u_3} [MeasurableSpace Ω'] (μ : MeasureTheory.Measure Ω) (ν : MeasureTheory.Measure Ω') (X : Ω → α) (Y : Ω' → α) (h : ProbabilityTheory.IdentDistrib X Y μ ν) :
    entropy μ X = entropy ν Y
    Used by
      theorem

      InformationTheory.Shannon.entropy_jointRV_eq_n_smul

      source
      {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (n : ℕ) :
      entropy μ (jointRV Xs n) = ↑n * entropy μ (Xs 0)

      Entropy chain rule for i.i.d. blocks: H(X^n) = n · H(X_0).

      Used by

        Per-block converse bound #

        theorem

        InformationTheory.Shannon.source_coding_per_n_bound

        source
        {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hcard : 2 ≤ Fintype.card α) (n : ℕ) (hn : 1 ≤ n) {M : ℕ} [NeZero M] (c : (Fin n → α) → Fin M) (d : Fin M → Fin n → α) :
        ↑n * entropy μ (Xs 0) ≤ Real.log ↑M + Real.binEntropy (MeasureFano.errorProb μ (jointRV Xs n) (fun (ω : Ω) => c (jointRV Xs n ω)) d) + MeasureFano.errorProb μ (jointRV Xs n) (fun (ω : Ω) => c (jointRV Xs n ω)) d * ↑n * Real.log ↑(Fintype.card α)

        Per-block source-coding converse bound: (n : ℝ) · H(Xs 0) ≤ log M + h(Pe_n) + Pe_n · n · log |α|.

        Used by

          Converse theorem in Filter.liminf form #

          theorem

          InformationTheory.Shannon.source_coding_converse

          source
          {Ω : Type u_1} [MeasurableSpace Ω] {α : Type u_2} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hcard : 2 ≤ Fintype.card α) (M : ℕ → ℕ) [hM_pos : ∀ (n : ℕ), NeZero (M n)] (c : (n : ℕ) → (Fin n → α) → Fin (M n)) (d : (n : ℕ) → Fin (M n) → Fin n → α) (hPe_to_zero : Filter.Tendsto (fun (n : ℕ) => MeasureFano.errorProb μ (jointRV Xs n) (fun (ω : Ω) => c n (jointRV Xs n ω)) (d n)) Filter.atTop (nhds 0)) (hM_bdd : ∃ (R : ℝ), ∀ (n : ℕ), Real.log ↑(M n) / ↑n ≤ R) :
          entropy μ (Xs 0) ≤ Filter.liminf (fun (n : ℕ) => Real.log ↑(M n) / ↑n) Filter.atTop

          Source coding theorem (weak converse): For any block code (c_n, d_n) with M_n codewords and i.i.d. discrete source, if the error probability vanishes then the rate is at least the entropy.

          The boundedness assumption hM_bdd (rate bounded above) captures the practical setting: it rules out the pathological case M n growing super-exponentially in n (where liminf log M_n / n would collapse to junk in the conditionally complete real lattice). For rate-bounded codes M n = 2^⌈n R⌉ this is automatic with R' any constant > R.

          Used by