Skip to content

InformationTheory.Shannon.Chernoff.Converse

Imports 12

The pmf-level variational identity #

The divergence of the Chernoff mediator T_λ = P₁^{1-λ}P₂^λ / Z(λ) against P₁ has the closed form λ · E_{T_λ}[log(P₂/P₁)] - log Z(λ). At the optimal λ* (interior, where the mean log-likelihood-ratio vanishes — the first-order condition of the chernoffInfo inf) the first term drops, giving klDivPmf (T_λ*) P₁ = -log Z(λ*) = chernoffInfo P₁ P₂.

theorem

InformationTheory.Shannon.Chernoff.chernoffMediator_klDiv_eq

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) [Nonempty α] (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (lam : ℝ) :

CsiszarProjection.klDivPmf (chernoffMediator P₁ P₂ lam) P₁ = lam * ∑ a : α, chernoffMediator P₁ P₂ lam a * Real.log (P₂ a / P₁ a) - Real.log (chernoffZSum P₁ P₂ lam)

Closed form for the mediator divergence: klDivPmf (chernoffMediator P₁ P₂ λ) P₁ = λ · (∑ a, T_λ(a)·log(P₂ a/P₁ a)) - log Z(λ).

Used by

Per-term log identity, the `log Z` derivative, and the balance (FOC) #

chernoffMediator_log_sub is the per-term identity already implicit in the atom; chernoffLogZ_hasDerivAt differentiates log Z (the analytic core), and chernoffMediator_balance reads off the first-order condition at an interior minimizer.

theorem

InformationTheory.Shannon.Chernoff.chernoffMediator_log_sub

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) [Nonempty α] (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) (a : α) :

Real.log (chernoffMediator P₁ P₂ lam a) - Real.log (P₁ a) = lam * Real.log (P₂ a / P₁ a) - Real.log (chernoffZSum P₁ P₂ lam)

Per-term log identity: log(T_λ a) - log(P₁ a) = λ·log(P₂ a/P₁ a) - log Z(λ).

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoffLogZ_hasDerivAt

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) [Nonempty α] (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) :

HasDerivAt (fun (l : ℝ) => Real.log (chernoffZSum P₁ P₂ l)) (∑ a : α, chernoffMediator P₁ P₂ lam a * Real.log (P₂ a / P₁ a)) lam

The derivative of λ ↦ log Z(λ) is the mediator-weighted mean log-likelihood-ratio: d/dλ log Z(λ) = ∑ a, T_λ(a)·log(P₂ a/P₁ a).

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoffMediator_balance

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) [Nonempty α] (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (lam : ℝ) (hlam_min : IsMinOn (fun (l : ℝ) => Real.log (chernoffZSum P₁ P₂ l)) (Set.Icc 0 1) lam) (hlam_io : lam ∈ Set.Ioo 0 1) :

∑ a : α, chernoffMediator P₁ P₂ lam a * Real.log (P₂ a / P₁ a) = 0

Balance / first-order condition at an interior minimizer λ* ∈ (0,1) of log Z: ∑ a, T_λ*(a)·log(P₂ a/P₁ a) = 0 (Fermat: the derivative vanishes at an interior min).

Used by

The half-space `K` and the I-projection identities #

def

InformationTheory.Shannon.Chernoff.chernoffHalfSpace

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) :

Set (α → ℝ)

The Chernoff half-space K = {p : full-support pmf with ∑ p_a log(P₂ a/P₁ a) ≥ 0}, onto which chernoffMediator P₁ P₂ λ* is the Csiszár I-projection of P₁.

Equations

InformationTheory.Shannon.Chernoff.chernoffHalfSpace P₁ P₂ = {p : α → ℝ | (∀ (a : α), 0 < p a) ∧ ∑ a : α, p a = 1 ∧ 0 ≤ ∑ a : α, p a * Real.log (P₂ a / P₁ a)}

Instances For

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoffInfo_eq_neg_logZ_of_isMinOn

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) (lam : ℝ) (hlam_min : IsMinOn (fun (l : ℝ) => Real.log (chernoffZSum P₁ P₂ l)) (Set.Icc 0 1) lam) (hlam_mem : lam ∈ Set.Icc 0 1) :

chernoffInfo P₁ P₂ = -Real.log (chernoffZSum P₁ P₂ lam)

At a minimizer λ* of log Z over [0,1], the Chernoff information equals -log Z(λ*). This recovers the defining -sInf identity from the minimizer condition, so callers carrying an IsMinOn witness need not pass chernoffInfo = -log Z(λ*) as a separate hypothesis.

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoffInfo_eq_mediator_div

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) [Nonempty α] (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (lam : ℝ) (hlam_min : IsMinOn (fun (l : ℝ) => Real.log (chernoffZSum P₁ P₂ l)) (Set.Icc 0 1) lam) (hlam_io : lam ∈ Set.Ioo 0 1) :

chernoffInfo P₁ P₂ = CsiszarProjection.klDivPmf (chernoffMediator P₁ P₂ lam) P₁

At an interior minimizer λ* of log Z, the mediator divergence equals the Chernoff information: chernoffInfo P₁ P₂ = klDivPmf (T_λ*) P₁.

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoffMediator_isMinOn

{α : Type u_1} [Fintype α] (P₁ P₂ : α → ℝ) [Nonempty α] (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (lam : ℝ) (hlam_min : IsMinOn (fun (l : ℝ) => Real.log (chernoffZSum P₁ P₂ l)) (Set.Icc 0 1) lam) (hlam_io : lam ∈ Set.Ioo 0 1) :

IsMinOn (fun (p : α → ℝ) => CsiszarProjection.klDivPmf p P₁) (chernoffHalfSpace P₁ P₂) (chernoffMediator P₁ P₂ lam)

The Chernoff mediator at an interior minimizer λ* is the Csiszár I-projection of P₁ onto the half-space K: it minimizes klDivPmf · P₁ over K.

Used by

Sanov lower bound and assembly #

The headline of this section is

chernoff_converse : limsup_n -(1/n) log (bayesErrorMinPmf P₁ P₂ n) ≤ chernoffInfo P₁ P₂.

Route: chernoffMediator P₁ P₂ λ* is the I-projection of P₁ onto the half-space {p : ∑ p_a log(P₂ a/P₁ a) ≥ 0}; csiszar_pythagoras_inequality identifies ⨅_{p∈K} klDivPmf p P₁ with klDivPmf (T_λ*) P₁ = chernoffInfo (the variational identity above). The error region {x : P₁ⁿ(x) ≤ P₂ⁿ(x)} is that half-space lifted to empirical type classes, so sanov_ldp_equality supplies (1/n) log P₁ⁿ(region) → -chernoffInfo, and bayesErrorMinPmf ≥ (1/2)·P₁ⁿ(region) closes the converse.

noncomputable def

InformationTheory.Shannon.Chernoff.chernoffErrorCounts

{α : Type u_1} [Fintype α] [DecidableEq α] (P₁ P₂ : α → ℝ) (n : ℕ) :

Finset (TypeCountIndex α n)

Discretized error region: count vectors c (with ∑ c = n) whose type class lands in the likelihood-ratio test region {x | ∏ P₁(x_i) ≤ ∏ P₂(x_i)}. (Clone of Hoeffding.E_r.)

Equations

InformationTheory.Shannon.Chernoff.chernoffErrorCounts P₁ P₂ n = {c : InformationTheory.Shannon.TypeCountIndex α n | ∑ a : α, ↑(c a) = n ∧ ∏ a : α, P₁ a ^ ↑(c a) ≤ ∏ a : α, P₂ a ^ ↑(c a)}

Instances For

Used by

theorem

InformationTheory.Shannon.Chernoff.mem_chernoffErrorCounts_iff

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (n : ℕ) (c : TypeCountIndex α n) :

c ∈ chernoffErrorCounts P₁ P₂ n ↔ ∑ a : α, ↑(c a) = n ∧ ∏ a : α, P₁ a ^ ↑(c a) ≤ ∏ a : α, P₂ a ^ ↑(c a)

Used by

theorem

InformationTheory.Shannon.Chernoff.prod_aggr_of_mem_typeClassByCount

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {n : ℕ} {c : α → ℕ} {x : Fin n → α} (hx : x ∈ typeClassByCount c) (f : α → ℝ) :

∏ i : Fin n, f (x i) = ∏ a : α, f a ^ c a

Product aggregation by counts: for x ∈ typeClassByCount c, ∏ i, f (x i) = ∏ a, (f a)^(c a). (Multiplicative analogue of sum_const_aggr_of_mem_typeClassByCount.)

Used by

theorem

InformationTheory.Shannon.Chernoff.typeCount_le

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {n : ℕ} (x : Fin n → α) (a : α) :

typeCount x a ≤ n

Every count typeCount x a is at most n.

Used by

theorem

InformationTheory.Shannon.Chernoff.typeCount_sum_eq

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {n : ℕ} (x : Fin n → α) :

∑ a : α, typeCount x a = n

The empirical counts of x sum to n.

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoffErrorRegion_eq_union

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (n : ℕ) :

{x : Fin n → α | ∏ i : Fin n, P₁ (x i) ≤ ∏ i : Fin n, P₂ (x i)} = ⋃ c ∈ chernoffErrorCounts P₁ P₂ n, typeClassByCount fun (a : α) => ↑(c a)

The likelihood-ratio error region equals the union of the error type classes.

Used by

theorem

InformationTheory.Shannon.Chernoff.measurePi_toReal_eq_sum

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] {n : ℕ} (S : Finset (Fin n → α)) :

((MeasureTheory.Measure.pi fun (x : Fin n) => Q) ↑S).toReal = ∑ x ∈ S, ∏ i : Fin n, Q.real {x i}

The Measure.pi Q mass of a finite set of sequences as a finite real sum of products of singleton masses. (Extracted from the inline block in typeClass_Qn_le.)

Used by

theorem

InformationTheory.Shannon.Chernoff.bayesErrorMinPmf_ge_half_sum

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_nn : ∀ (a : α), 0 ≤ P₁ a) (hP₂_nn : ∀ (a : α), 0 ≤ P₂ a) (n : ℕ) (S : Finset (Fin n → α)) (hS : ∀ x ∈ S, ∏ i : Fin n, P₁ (x i) ≤ ∏ i : Fin n, P₂ (x i)) :

1 / 2 * ∑ x ∈ S, ∏ i : Fin n, P₁ (x i) ≤ bayesErrorMinPmf P₁ P₂ n

The Bayes error dominates half the P₁-mass of any sub-region of the error region.

Used by

Perturbation membership and degenerate handling #

theorem

InformationTheory.Shannon.Chernoff.prod_pow_le_iff_sum_log

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (c : α → ℕ) :

∏ a : α, P₁ a ^ c a ≤ ∏ a : α, P₂ a ^ c a ↔ 0 ≤ ∑ a : α, ↑(c a) * Real.log (P₂ a / P₁ a)

The likelihood-ratio membership ∏ P₁^c ≤ ∏ P₂^c is equivalent to the log-form 0 ≤ ∑ a, (c a)·log(P₂ a/P₁ a) (both products positive under full support).

Used by

theorem

InformationTheory.Shannon.Chernoff.klDivSumForm_ofVec_eq_klDivPmf_left

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (Q : MeasureTheory.Measure α) (hQ_real : ∀ (a : α), Q.real {a} = P₁ a) {p : α → ℝ} (hp_nn : ∀ (a : α), 0 ≤ p a) (hp_sum : ∑ a : α, p a = 1) :

(klDivSumForm_ofVec p fun (a : α) => Q.real {a}) = CsiszarProjection.klDivPmf p P₁

Generic rate bridge: for any pmf p and a measure Q whose singleton masses recover P₁, klDivSumForm_ofVec p (Q.real ∘ singleton) = klDivPmf p P₁.

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoffMediator_perturb_llr_pos

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) (lam : ℝ) (hlam_min : IsMinOn (fun (l : ℝ) => Real.log (chernoffZSum P₁ P₂ l)) (Set.Icc 0 1) lam) (hlam_io : lam ∈ Set.Ioo 0 1) (h_nondeg : 0 < CsiszarProjection.klDivPmf P₂ P₁) {ε : ℝ} (hε0 : 0 < ε) (_hε1 : ε ≤ 1) :

0 < ∑ a : α, HoeffdingTradeoffExp.Qstar_perturb (chernoffMediator P₁ P₂ lam) P₂ ε a * Real.log (P₂ a / P₁ a)

H7b: the perturbed mediator T_ε = (1-ε)·T_λ* + ε·P₂ has strictly positive mean log-likelihood-ratio when P₁ ≠ P₂ (0 < klDivPmf P₂ P₁).

Used by

theorem

InformationTheory.Shannon.Chernoff.roundedType_mem_chernoffErrorCounts_eventually

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) {T : α → ℝ} (hT_sum : ∑ a : α, T a = 1) (hT_nn : ∀ (a : α), 0 ≤ T a) (h_llr_pos : 0 < ∑ a : α, T a * Real.log (P₂ a / P₁ a)) :

∀ᶠ (n : ℕ) in Filter.atTop , roundedTypeIndex T n ∈ chernoffErrorCounts P₁ P₂ n

H7c: a full-support pmf T strictly inside the error half-space (0 < ∑ T·log(P₂/P₁)) has its rounded type eventually in the error region.

Used by

theorem

InformationTheory.Shannon.Chernoff.bayesErrorMinPmf_ge_half_measurePi

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_nn : ∀ (a : α), 0 ≤ P₁ a) (hP₂_nn : ∀ (a : α), 0 ≤ P₂ a) (Q : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure Q] (hQ_real : ∀ (a : α), Q.real {a} = P₁ a) (n : ℕ) :

1 / 2 * ((MeasureTheory.Measure.pi fun (x : Fin n) => Q) (⋃ c ∈ chernoffErrorCounts P₁ P₂ n, typeClassByCount fun (a : α) => ↑(c a))).toReal ≤ bayesErrorMinPmf P₁ P₂ n

The Bayes error dominates half the P₁-measure of the error region.

Used by

theorem

InformationTheory.Shannon.Chernoff.chernoff_converse

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] (P₁ P₂ : α → ℝ) (hP₁_pos : ∀ (a : α), 0 < P₁ a) (hP₂_pos : ∀ (a : α), 0 < P₂ a) (hP₁_sum : ∑ a : α, P₁ a = 1) (hP₂_sum : ∑ a : α, P₂ a = 1) (lam : ℝ) (hlam_min : IsMinOn (fun (l : ℝ) => Real.log (chernoffZSum P₁ P₂ l)) (Set.Icc 0 1) lam) (hlam_io : lam ∈ Set.Ioo 0 1) :

Filter.limsup (fun (n : ℕ) => -(1 / ↑n) * Real.log (bayesErrorMinPmf P₁ P₂ n)) Filter.atTop ≤ chernoffInfo P₁ P₂

The optimal Bayes error exponent cannot exceed the Chernoff information (Cover–Thomas, converse half). Proved on the interior 0 < λ* < 1 (the overlapping-support / non-degenerate case; hlam_io is a non-degeneracy precondition, not load-bearing). @audit:ok

Used by