Entropy function #
The purpose of this file is to record basic analytic properties of the function
Main results #
sum_negMulLog_le
: a Jensen inequality fornegMulLog
sum_negMulLog_eq
: the equality case of this inequality
theorem
Real.sum_mul_log_div_leq
{ι : Type u_1}
{s : Finset ι}
{a b : ι → ℝ}
(ha : ∀ i ∈ s, 0 ≤ a i)
(hb : ∀ i ∈ s, 0 ≤ b i)
(habs : ∀ i ∈ s, b i = 0 → a i = 0)
:
If
theorem
Real.sum_mul_log_div_eq_iff_aux
{ι : Type u_1}
{s : Finset ι}
{a b : ι → ℝ}
(ha : ∀ i ∈ s, 0 ≤ a i)
(hb : ∀ i ∈ s, 0 < b i)
(heq : ∑ i ∈ s, a i * log (a i / b i) = (∑ i ∈ s, a i) * log ((∑ i ∈ s, a i) / ∑ i ∈ s, b i))
:
If equality holds in the previous bound, then b i
are positive.
theorem
Real.sum_mul_log_div_eq_iff
{ι : Type u_1}
{s : Finset ι}
{a b : ι → ℝ}
(ha : ∀ i ∈ s, 0 ≤ a i)
(hb : ∀ i ∈ s, 0 ≤ b i)
(habs : ∀ i ∈ s, b i = 0 → a i = 0)
(heq : ∑ i ∈ s, a i * log (a i / b i) = (∑ i ∈ s, a i) * log ((∑ i ∈ s, a i) / ∑ i ∈ s, b i))
:
If equality holds in the previous bound, then