Channel Capacity and Capacity-Achieving Priors

@cite{cover-thomas-2006} @cite{zaslavsky-etal-2019}

The maximum mutual information C* = sup_{p(c)} I(W;C) for a CommChannel, plus the capacity-achieving prior (CAP) condition p(c) ∝ exp(-S(c)) and its central consequence: at a CAP, -log p(c) = S(c) + log Z (paper eq. 6).

Channel structure and per-channel quantities (marginalWord, posterior, commPrecision, mutualInfo) live in the sibling Channel.lean. This file is capacity-specific.

Main definitions

• IsCAP: capacity-achieving prior predicate p(c) ∝ exp(-S(c))
• channelCapacity: sup_{p(c)} I(W;C)

Main results

• cap_linear: at a CAP, -log p(c) = S(c) + log Z
• mutualInfo_eq_log_Z_of_cap: at a CAP, I(W;C) = log Z
• mutualInfo_le_log_card: I(W;C) ≤ log |W|
• channelCapacity_le_log_card: C* ≤ log |W|

(KL non-negativity / Gibbs' inequality is 0 ≤ (P.klDiv Q).toReal by ENNReal.toReal_nonneg on the PMF API, or Core.InformationTheory.kl_nonneg on the (ι→ℝ) form. Bridge: PMF.toReal_klDiv_eq_sum_log_div.)

def Pragmatics.InformationTheory.IsCAP {C W : Type} [Fintype C] [Fintype W] (nc : CommChannel C W) (prior : C → ℝ) : Prop

A prior is capacity-achieving iff p(c) ∝ exp(-S(c)). Necessary and sufficient for p(c) to maximize I(W;C) over all priors on C. From @cite{zaslavsky-etal-2019}; derived from the Blahut-Arimoto algorithm (@cite{cover-thomas-2006}).

Equations

• Pragmatics.InformationTheory.IsCAP nc prior = ∃ Z > 0, ∀ (c : C), prior c > 0 → prior c = Real.exp (-Pragmatics.InformationTheory.commPrecision nc prior c) / Z

theorem Pragmatics.InformationTheory.cap_linear {C W : Type} [Fintype C] [Fintype W] (nc : CommChannel C W) (prior : C → ℝ) {Z : ℝ} (hZ : Z > 0) (hCAP : ∀ (c : C), prior c > 0 → prior c = Real.exp (-commPrecision nc prior c) / Z) {c : C} (hc : prior c > 0) : -Real.log (prior c) = commPrecision nc prior c + Real.log Z

The CAP linear relation: at a capacity-achieving prior, -log p(c) = S(c) + log Z. From @cite{zaslavsky-etal-2019}.

theorem Pragmatics.InformationTheory.cap_linear' {C W : Type} [Fintype C] [Fintype W] (nc : CommChannel C W) (prior : C → ℝ) (hCAP : IsCAP nc prior) {c : C} (hc : prior c > 0) : ∃ Z > 0, -Real.log (prior c) = commPrecision nc prior c + Real.log Z

Variant of cap_linear taking an existential IsCAP witness.

theorem Pragmatics.InformationTheory.mutualInfo_eq_log_Z_of_cap {C W : Type} [Fintype C] [Fintype W] (nc : CommChannel C W) (prior : C → ℝ) {Z : ℝ} (hZ : Z > 0) (hCAP : ∀ (c : C), prior c > 0 → prior c = Real.exp (-commPrecision nc prior c) / Z) (hprior_nonneg : ∀ (c : C), 0 ≤ prior c) (hprior_sum : ∑ c : C, prior c = 1) (hprior_pos : ∀ (c : C), prior c > 0) : mutualInfo nc prior = Real.log Z

At a CAP, mutual information equals log Z. The normalization constant Z in the CAP condition determines the channel capacity.

theorem Pragmatics.InformationTheory.mutualInfo_le_log_card {C W : Type} [Fintype C] [Fintype W] (nc : CommChannel C W) (prior : C → ℝ) (hprior_nonneg : ∀ (c : C), 0 ≤ prior c) (hprior_sum : ∑ c : C, prior c = 1) : mutualInfo nc prior ≤ Real.log ↑(Fintype.card W)

Mutual information is bounded by the log of the vocabulary size: I(W;C) ≤ log |W|.

noncomputable def Pragmatics.InformationTheory.channelCapacity {C W : Type} [Fintype C] [Fintype W] (nc : CommChannel C W) : ℝ

Channel capacity: the supremum of mutual information over all valid priors. C* = sup_{p(c)} I(W;C) (eq. 3 of @cite{zaslavsky-etal-2019}).

Equations

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

theorem Pragmatics.InformationTheory.channelCapacity_le_log_card {C W : Type} [Fintype C] [Fintype W] (nc : CommChannel C W) [Nonempty C] : channelCapacity nc ≤ Real.log ↑(Fintype.card W)

Channel capacity is bounded by log of the vocabulary size.

theorem Pragmatics.InformationTheory.mutualInfo_le_log_fin {C : Type} [Fintype C] {k : ℕ} (nc : CommChannel C (Fin k)) (prior : C → ℝ) (hp : ∀ (c : C), 0 ≤ prior c) (hsum : ∑ c : C, prior c = 1) : mutualInfo nc prior ≤ Real.log ↑k

Mutual information bound for a Fin k vocabulary: I(W;C) ≤ log k.