InformationTheory

InformationTheory.Shannon.CsiszarProjection

source

Imports 7

Csiszár I-projection and the Pythagorean inequality #

For a finite alphabet α, a full-support reference pmf Q : α → ℝ, and a closed convex set K ⊆ stdSimplex ℝ α:

  • Existence: there is Q* ∈ K minimizing klDivPmf · Q over K.
  • Uniqueness: the minimizer is unique.
  • The Pythagorean inequality (Cover-Thomas): for all P ∈ K, klDivPmf P Q ≥ klDivPmf P Q* + klDivPmf Q* Q.

Main definitions #

  • klDivPmf P Q := ∑ a, Q a * klFun (P a / Q a) — real-valued finite-alphabet KL divergence.

Main statements #

Implementation notes #

Proof strategy for the Pythagorean inequality: the first-order condition ∑ (P - Q*)(log Q* - log Q) ≥ 0 is derived from the right derivative of t ↦ klDivPmf ((1-t)Q* + tP) Q at t = 0 being non-negative (minimality of Q*). Combined with the algebraic identity klDivPmf P Q = klDivPmf P Q* + ∑ P·(log Q* - log Q) and the expansion of klDivPmf Q* Q, this gives the inequality.

References #

  • T. M. Cover and J. A. Thomas, Elements of Information Theory (2nd ed.), Wiley, 2006.

klDivPmf: definition, non-negativity, continuity, and strict convexity #

noncomputable def

InformationTheory.Shannon.CsiszarProjection.klDivPmf

source
{α : Type u_1} [Fintype α] (P Q : α → ℝ) :
ℝ

The real-valued finite-alphabet KL divergence as a pmf functional: klDivPmf P Q := ∑ a, Q a * klFun (P a / Q a) where klFun x = x * log x + 1 - x (Mathlib InformationTheory.klFun).

Equivalent to (klDiv P Q).toReal under support hypotheses (bridge in Sanov/Basic.lean), but we work Real-only here to leverage strictConvexOn_klFun + finite-sum API directly.

Equations
Instances For
    Used by
      theorem

      InformationTheory.Shannon.CsiszarProjection.klDivPmf_nonneg

      source
      {α : Type u_1} [Fintype α] (P Q : α → ℝ) (hP : ∀ (a : α), 0 ≤ P a) (hQ : ∀ (a : α), 0 ≤ Q a) :
      0 ≤ klDivPmf P Q

      klDivPmf is non-negative on the simplex when Q is a pmf (full support not required: each summand is Q a * klFun (P a / Q a) ≥ 0 whenever Q a ≥ 0, since klFun ≥ 0 on [0, ∞) and P a / Q a ≥ 0 follows from P a ≥ 0 and Q a ≥ 0).

      Used by
        theorem

        InformationTheory.Shannon.CsiszarProjection.continuous_klDivPmf_left

        source
        {α : Type u_1} [Fintype α] (Q : α → ℝ) (hQ_pos : ∀ (a : α), 0 < Q a) :
        Continuous fun (P : α → ℝ) => klDivPmf P Q

        klFun is continuous on [0, ∞) (Mathlib continuous_klFun). The composition fun P => klFun (P a / Q a) is continuous in P when Q a > 0.

        Used by
          theorem

          InformationTheory.Shannon.CsiszarProjection.klDivPmf_strictConvexOn_left

          source
          {α : Type u_1} [Fintype α] (Q : α → ℝ) (hQ_pos : ∀ (a : α), 0 < Q a) :
          StrictConvexOn ℝ (stdSimplex ℝ α) fun (P : α → ℝ) => klDivPmf P Q

          klDivPmf · Q is strictly convex on stdSimplex ℝ α (full support Q + Π ⊆ simplex).

          Per-coordinate: klFun is strictly convex on [0, ∞) (strictConvexOn_klFun). The map P ↦ P a / Q a is affine (when Q a > 0 is fixed), and Q a * (·) preserves strict convexity. Sum of strictly convex (in at least one coordinate where P ≠ P') gives strict convexity of the sum.

          (But care: if P = P' they agree in every coordinate; if P ≠ P' then there is at least one coordinate a where P a ≠ P' a, and at that coordinate klFun strict convexity fires.)

          Used by

            Existence via extreme value theorem #

            theorem

            InformationTheory.Shannon.CsiszarProjection.isCompact_of_subset_stdSimplex

            source
            {α : Type u_1} [Fintype α] {K : Set (α → ℝ)} (hK_closed : IsClosed K) (hK_sub : K ⊆ stdSimplex ℝ α) :
            IsCompact K
            Used by
              theorem

              InformationTheory.Shannon.CsiszarProjection.csiszar_projection_exists

              source
              {α : Type u_1} [Fintype α] {K : Set (α → ℝ)} {Q : α → ℝ} (hK_closed : IsClosed K) (hK_sub : K ⊆ stdSimplex ℝ α) (hK_ne : K.Nonempty) (hQ_pos : ∀ (a : α), 0 < Q a) :
              ∃ Qstar ∈ K, IsMinOn (fun (P : α → ℝ) => klDivPmf P Q) K Qstar

              Existence of the Csiszár I-projection: for a nonempty closed set K ⊆ stdSimplex ℝ α and full-support Q, there exists Q* ∈ K minimizing klDivPmf · Q over K.

              Used by

                Uniqueness via strict convexity #

                theorem

                InformationTheory.Shannon.CsiszarProjection.csiszar_projection_unique

                source
                {α : Type u_1} [Fintype α] {K : Set (α → ℝ)} {Q : α → ℝ} (hK_conv : Convex ℝ K) (hK_sub : K ⊆ stdSimplex ℝ α) (hQ_pos : ∀ (a : α), 0 < Q a) {Qstar Qstar' : α → ℝ} (hQs : Qstar ∈ K) (hQs' : Qstar' ∈ K) (hmin : IsMinOn (fun (P : α → ℝ) => klDivPmf P Q) K Qstar) (hmin' : IsMinOn (fun (P : α → ℝ) => klDivPmf P Q) K Qstar') :
                Qstar = Qstar'

                Uniqueness of the Csiszár I-projection: the minimizer of klDivPmf · Q on a convex K ⊆ stdSimplex ℝ α is unique.

                Used by

                  Pythagorean inequality #

                  theorem

                  InformationTheory.Shannon.CsiszarProjection.klDivPmf_eq_log_diff_sum

                  source
                  {α : Type u_1} [Fintype α] {P Q : α → ℝ} (hP_sum : ∑ a : α, P a = 1) (hQ_sum : ∑ a : α, Q a = 1) (hP_pos : ∀ (a : α), 0 < P a) (hQ_pos : ∀ (a : α), 0 < Q a) :
                  klDivPmf P Q = ∑ a : α, P a * (Real.log (P a) - Real.log (Q a))

                  The standard sum form of klDivPmf under probability measure hypotheses: klDivPmf P Q = ∑ a, P a * (log (P a) - log (Q a)) when ∑ P = ∑ Q = 1 and both positive. (klFun(t) = t log t + 1 - t ⟹ Q * klFun(P/Q) = P log(P/Q) + Q - P, sum collapses 1 - 1 = 0.)

                  Used by
                    theorem

                    InformationTheory.Shannon.CsiszarProjection.klDivPmf_decomp_via_intermediate

                    source
                    {α : Type u_1} [Fintype α] {P Qstar Q : α → ℝ} (hP_sum : ∑ a : α, P a = 1) (hQs_sum : ∑ a : α, Qstar a = 1) (hQ_sum : ∑ a : α, Q a = 1) (hP_pos : ∀ (a : α), 0 < P a) (hQs_pos : ∀ (a : α), 0 < Qstar a) (hQ_pos : ∀ (a : α), 0 < Q a) :
                    klDivPmf P Q = klDivPmf P Qstar + ∑ a : α, P a * (Real.log (Qstar a) - Real.log (Q a))

                    Algebraic identity: for full-support P, Q*, Q, klDivPmf P Q = klDivPmf P Q* + ∑ a, P a * (log (Q* a) - log (Q a)).

                    Used by
                      theorem

                      InformationTheory.Shannon.CsiszarProjection.klDivPmf_self_expand

                      source
                      {α : Type u_1} [Fintype α] {Qstar Q : α → ℝ} (hQs_sum : ∑ a : α, Qstar a = 1) (hQ_sum : ∑ a : α, Q a = 1) (hQs_pos : ∀ (a : α), 0 < Qstar a) (hQ_pos : ∀ (a : α), 0 < Q a) :
                      klDivPmf Qstar Q = ∑ a : α, Qstar a * (Real.log (Qstar a) - Real.log (Q a))

                      Expansion of klDivPmf Q* Q in log-ratio form: klDivPmf Q* Q = ∑ a, Q* a * (log (Q* a) - log (Q a)).

                      Used by
                        theorem

                        InformationTheory.Shannon.CsiszarProjection.csiszar_segment_hasDerivAt

                        source
                        {α : Type u_1} [Fintype α] {Q Qstar P : α → ℝ} (hQ_pos : ∀ (a : α), 0 < Q a) (hQs_pos : ∀ (a : α), 0 < Qstar a) :
                        HasDerivAt (fun (t : ℝ) => klDivPmf ((1 - t) • Qstar + t • P) Q) (∑ a : α, (P a - Qstar a) * (Real.log (Qstar a) - Real.log (Q a))) 0

                        Derivative of the segment functional t ↦ klDivPmf ((1-t) • Qstar + t • P) Q at t = 0, equal to ∑ a, (P a - Qstar a) * (log (Qstar a) - log (Q a)).

                        Used by
                          theorem

                          InformationTheory.Shannon.CsiszarProjection.csiszar_first_order_condition

                          source
                          {α : Type u_1} [Fintype α] {K : Set (α → ℝ)} {Q : α → ℝ} (hK_conv : Convex ℝ K) (hQ_pos : ∀ (a : α), 0 < Q a) {Qstar : α → ℝ} (hQs : Qstar ∈ K) (hQs_pos : ∀ (a : α), 0 < Qstar a) (hmin : IsMinOn (fun (P : α → ℝ) => klDivPmf P Q) K Qstar) {P : α → ℝ} (hP : P ∈ K) :
                          0 ≤ ∑ a : α, (P a - Qstar a) * (Real.log (Qstar a) - Real.log (Q a))

                          The first-order optimality condition: if Q* minimizes klDivPmf · Q over K, then for all P ∈ K, ∑ a, (P a - Q* a) * (log (Q* a) - log (Q a)) ≥ 0.

                          Proof: the right derivative of t ↦ klDivPmf ((1-t)Q* + tP) Q at t = 0 equals the sum, and non-negativity follows from minimality (φ(0) ≤ φ(t) for small t > 0).

                          Used by
                            theorem

                            InformationTheory.Shannon.CsiszarProjection.csiszar_pythagoras_inequality

                            source
                            {α : Type u_1} [Fintype α] {K : Set (α → ℝ)} {Q : α → ℝ} (hK_conv : Convex ℝ K) (hK_sub : K ⊆ stdSimplex ℝ α) (hQ_sum : ∑ a : α, Q a = 1) (hQ_pos : ∀ (a : α), 0 < Q a) {Qstar : α → ℝ} (hQs : Qstar ∈ K) (hQs_pos : ∀ (a : α), 0 < Qstar a) (hmin : IsMinOn (fun (P : α → ℝ) => klDivPmf P Q) K Qstar) {P : α → ℝ} (hP : P ∈ K) (hP_pos : ∀ (a : α), 0 < P a) :
                            klDivPmf P Q ≥ klDivPmf P Qstar + klDivPmf Qstar Q

                            Csiszár's Pythagorean inequality: for the I-projection Q* and any P ∈ K, klDivPmf P Q ≥ klDivPmf P Q* + klDivPmf Q* Q.

                            Used by