Information Theory

Results named in Tau Ceti's TauCeti.InformationTheory modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremCsiszár's Pythagorean identity#

Let γ ≪ π ≪ R be finite measures such that llr π R is integrable against both γ and π, with the same integral. Then klDiv γ R = klDiv γ π + klDiv π R.

TauCeti.klDiv_eq_klDiv_add_klDiv.{u_1} {α : Type u_1} [MeasurableSpace α]
  {γ π R : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure γ]
  [MeasureTheory.IsFiniteMeasure π] [MeasureTheory.IsFiniteMeasure R]
  (hγπ : γ.AbsolutelyContinuous π) (hπR : π.AbsolutelyContinuous R)
  (hγ : MeasureTheory.Integrable (MeasureTheory.llr π R) γ)
  (hπ : MeasureTheory.Integrable (MeasureTheory.llr π R) π)
  (h : ∫ (x : α), MeasureTheory.llr π R x ∂γ = ∫ (x : α), MeasureTheory.llr π R x ∂π) :
  InformationTheory.klDiv γ R = InformationTheory.klDiv γ π + InformationTheory.klDiv π R

Lean

Formalized in Tau Ceti as TauCeti.klDiv_eq_klDiv_add_klDiv.

Sources

• Tau Ceti documentation: TauCeti.klDiv_eq_klDiv_add_klDiv
• Source of TauCeti.klDiv_eq_klDiv_add_klDiv in TauCeti/InformationTheory/KullbackLeibler/ChangeOfReference.lean

LeanTauCeti.klDiv_eq_klDiv_add_klDiv

Used by 1

Used byThe Pythagorean identity of the Schrödinger problem

TheoremPinsker's inequality#

Pinsker's inequality for probability measures, with natural logarithms and no absolute-continuity assumption. Mathlib's etvDist on the left is twice the usual distance dTV(μ, ν) = sup_s |μ s - ν s|, so the bound is equivalently 2 * dTV(μ, ν)² ≤ klDiv μ ν.

TauCeti.etvDist_sq_le_two_mul_klDiv.{u_1} {α : Type u_1} [MeasurableSpace α]
  {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] :
  MeasureTheory.etvDist μ ν ^ 2 ≤ 2 * InformationTheory.klDiv μ ν

Lean

Formalized in Tau Ceti as TauCeti.etvDist_sq_le_two_mul_klDiv.

Other forms

Pinsker's inequality. Formalized in Tau Ceti as TauCeti.etvDist_sq_le_two_mul_mass_mul_klDiv.

TauCeti.etvDist_sq_le_two_mul_mass_mul_klDiv.{u_1} {α : Type u_1} [MeasurableSpace α]
  {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν] (hmass : μ Set.univ = ν Set.univ) :
  MeasureTheory.etvDist μ ν ^ 2 ≤ 2 * μ Set.univ * InformationTheory.klDiv μ ν

Pinsker's inequality for events, with natural logarithms. Formalized in Tau Ceti as TauCeti.two_mul_sq_measureReal_sub_le_klDiv.

TauCeti.two_mul_sq_measureReal_sub_le_klDiv.{u_1} {α : Type u_1} [MeasurableSpace α]
  {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsProbabilityMeasure μ]
  [MeasureTheory.IsProbabilityMeasure ν] {s : Set α} (hs : MeasurableSet s) :
  ENNReal.ofReal (2 * (μ.real s - ν.real s) ^ 2) ≤ InformationTheory.klDiv μ ν

Sources

• Tau Ceti documentation: TauCeti.etvDist_sq_le_two_mul_klDiv
• Source of TauCeti.etvDist_sq_le_two_mul_klDiv in TauCeti/InformationTheory/KullbackLeibler/Pinsker.lean

LeanTauCeti.etvDist_sq_le_two_mul_klDiv · TauCeti.etvDist_sq_le_two_mul_mass_mul_klDiv · TauCeti.two_mul_sq_measureReal_sub_le_klDiv

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.