theorem Oseledets.OperatorEntropy.klein_scalar {K : Type u_1} {M : Type u_2} [Fintype K] [Fintype M] (p : K → ℝ) (s : M → ℝ) (D : K → M → ℝ) (hp : ∀ (k : K), 0 ≤ p k) (hs : ∀ (m : M), 0 ≤ s m) (hD : ∀ (k : K) (m : M), 0 ≤ D k m) (hrow : ∀ (k : K), ∑ m : M, D k m = 1) (hcol : ∀ (m : M), ∑ k : K, D k m = 1) (hsum : ∑ k : K, p k = ∑ m : M, s m) (hsupp : ∀ (m : M) (k : K), s m = 0 → D k m * p k = 0) : ∑ m : M, (∑ k : K, D k m * p k) * Real.log (s m) ≤ ∑ k : K, p k * Real.log (p k)

Scalar Klein / Peierls inequality. Let D be a doubly stochastic K × M matrix (row sums hrow and column sums hcol equal 1), p ≥ 0 a probability-like vector on K and s ≥ 0 one on M with equal total mass (hsum). Writing a m = ∑ k, D k m * p k for the column marginal, the support hypothesis hsupp (s m = 0 ⟹ D k m * p k = 0) handles the columns where s m = 0 (there a m = 0). Then ∑ m, a m * log (s m) ≤ ∑ k, p k * log (p k).

This is the finite, scalar analogue powering the matrix/operator Klein inequality (Carlen, Trace Inequalities and Quantum Entropy, Thm 2.11 / Peierls Thm 2.9).