InformationTheory

InformationTheory.Fano.BinaryJensen

source

Imports 4

Finite-Finset Jensen for Real.binEntropy, plus algebraic helpers #

M3 lemma: Jensen inequality on Real.binEntropy over a finite Finset (binEntropy_jensen_finset).

Plus two pure-ℝ algebraic identities used to recast a 2-branch sum of negMulLog as a binEntropy term, which feeds the M5 step H(E | Y) ≤ binEntropy Pe.

theorem

InformationTheory.binEntropy_jensen_finset

source
{ι : Type u_1} [Fintype ι] (w p : ι → ℝ) (hw_nn : ∀ (i : ι), 0 ≤ w i) (hw_sum : ∑ i : ι, w i = 1) (hp_mem : ∀ (i : ι), p i ∈ Set.Icc 0 1) :
∑ i : ι, w i * Real.binEntropy (p i) ≤ Real.binEntropy (∑ i : ι, w i * p i)

Finite-Finset Jensen specialization for Real.binEntropy.

If the weights w form a probability distribution on a finite type ι and each p i lies in the interval [0, 1], then the average of the binary entropies is bounded by the binary entropy of the average.

Used by
    theorem

    InformationTheory.mul_negMulLog_div

    source
    (m x : ℝ) (hm : m ≠ 0) :
    m * (x / m).negMulLog = x.negMulLog + x * Real.log m

    Algebraic identity used to relate sums of negMulLog to binEntropy: m * negMulLog (x / m) = negMulLog x + x * log m whenever m ≠ 0.

    Used by
      theorem

      InformationTheory.negMulLog_pair_sub_negMulLog_sum_eq_binEntropy

      source
      (p q : ℝ) (hp : 0 ≤ p) (hq : 0 ≤ q) :
      p.negMulLog + q.negMulLog - (p + q).negMulLog = (p + q) * Real.binEntropy (p / (p + q))

      Two-branch binEntropy collapse:

      negMulLog p + negMulLog q - negMulLog (p + q) = (p + q) * binEntropy (p / (p + q))

      for p, q ≥ 0. The boundary case p + q = 0 is handled via the convention negMulLog 0 = 0 and 0/0 = 0 (so binEntropy (0/0) = 0).

      Used by