InformationTheory.Shannon.KLDivContinuous

Imports 5

KL divergence in vector form and its continuity #

klDivSumForm_ofVec p q := ∑ a, p a * (log (p a) - log (q a)) and its continuity in p under the Pi topology on α → ℝ (finite α).

klDivSumForm_ofVec_continuous — continuous in p when q a > 0 for all a.
klDivIndex_eq_ofVec — klDivIndex c n Q = klDivSumForm_ofVec (c/n) (Q.real ∘ singleton).

noncomputable def

{α : Type u_1} [Fintype α] (p q : α → ℝ) :

KL divergence in finite-alphabet vector form taking α → ℝ inputs: klDivSumForm_ofVec p q := ∑ a, p a * (log (p a) - log (q a)).

This variant is designed for continuity arguments in the Pi topology on α → ℝ, complementing the Measure α-based klDiv.

Equations

Instances For

Used by

theorem

{α : Type u_1} [Fintype α] (q : α → ℝ) (_hq_pos : ∀ (a : α), 0 < q a) :

p ↦ klDivSumForm_ofVec p q is continuous when q a > 0 for all a.

Used by

theorem

{α : Type u_1} [Fintype α] [MeasurableSpace α] (c : α → ℕ) (n : ℕ) (Q : MeasureTheory.Measure α) :

klDivIndex c n Q = klDivSumForm_ofVec (fun (a : α) => ↑(c a) / ↑n) fun (a : α) => Q.real {a}

Used by