Finite log-sum inequality

This opt-in scalar module develops the finite log-sum inequality independently of probability-mass functions and Shannon information measures.

Guarded Real proof infrastructure

Extended log-sum terms

noncomputable def LeanInfoTheory.Shannon.logSumTerm (a b : NNReal) : EReal

The zero-safe extended-real scalar term in the finite log-sum inequality.

The conventions are 0 * log (0 / b) = 0 for every b, including b = 0, and a * log (a / 0) = top when a is positive.

theorem LeanInfoTheory.Shannon.logSumTerm_zero_left (b : NNReal) : logSumTerm 0 b = 0

A zero numerator contributes zero to the extended log-sum.

theorem LeanInfoTheory.Shannon.logSumTerm_pos_zero {a : NNReal} (ha : a ≠ 0) : logSumTerm a 0 = ⊤

A positive numerator over a zero denominator contributes top.

theorem LeanInfoTheory.Shannon.logSumTerm_ne_bot (a b : NNReal) : logSumTerm a b ≠ ⊥

An extended log-sum term is never bottom.

theorem LeanInfoTheory.Shannon.sum_logSumTerm_ne_bot {ι : Type u} (s : Finset ι) (a b : ι → NNReal) : ∑ i ∈ s, logSumTerm (a i) (b i) ≠ ⊥

Every finite selected sum of extended log-sum terms is never bottom.

theorem LeanInfoTheory.Shannon.logSum_inequality {ι : Type u} (s : Finset ι) (a b : ι → NNReal) : logSumTerm (∑ i ∈ s, a i) (∑ i ∈ s, b i) ≤ ∑ i ∈ s, logSumTerm (a i) (b i)

Finite log-sum inequality with the zero-safe conventions of logSumTerm.

In particular, a selected positive numerator over a zero denominator makes the right-hand side top; no support or positivity guard is required.

theorem LeanInfoTheory.Shannon.logSum_eq_iff_exists_constant_ratio {ι : Type u} (s : Finset ι) (a b : ι → NNReal) : logSumTerm (∑ i ∈ s, a i) (∑ i ∈ s, b i) = ∑ i ∈ s, logSumTerm (a i) (b i) ↔ ∃ (c : ENNReal), ∀ i ∈ s, a i ≠ 0 ∨ b i ≠ 0 → ↑(a i) / ↑(b i) = c

Equality in the zero-safe finite log-sum inequality.

Equality holds exactly when all active selected pairs have one common ENNReal numerator-to-denominator ratio. Selected (0, 0) pairs are inactive; the common ratio may be finite or top.

theorem LeanInfoTheory.Shannon.real_logSum_inequality_of_support {ι : Type u} (s : Finset ι) (a b : ι → NNReal) (h_support : ∀ i ∈ s, a i ≠ 0 → b i ≠ 0) : ↑(∑ i ∈ s, a i) * Real.log (↑(∑ i ∈ s, a i) / ↑(∑ i ∈ s, b i)) ≤ ∑ i ∈ s, ↑(a i) * Real.log (↑(a i) / ↑(b i))

Guarded Real finite log-sum inequality.

The support guard excludes positive-over-zero selected pairs while permitting selected (0, 0) pairs.

theorem LeanInfoTheory.Shannon.real_logSum_eq_iff_exists_constant_ratio_of_support {ι : Type u} (s : Finset ι) (a b : ι → NNReal) (h_support : ∀ i ∈ s, a i ≠ 0 → b i ≠ 0) : ↑(∑ i ∈ s, a i) * Real.log (↑(∑ i ∈ s, a i) / ↑(∑ i ∈ s, b i)) = ∑ i ∈ s, ↑(a i) * Real.log (↑(a i) / ↑(b i)) ↔ ∃ (c : ℝ), ∀ i ∈ s, a i ≠ 0 ∨ b i ≠ 0 → ↑(a i) / ↑(b i) = c

Equality in the guarded Real finite log-sum inequality holds exactly when all active selected pairs have one common finite ratio.