Source indexedlemma · leanprover/lean4:v4.33.0-rc1

Real.sum_mul_log_div_leq

PFR.Mathlib.Analysis.SpecialFunctions.NegMulLog · PFR/Mathlib/Analysis/SpecialFunctions/NegMulLog.lean:32 to 67

Source documentation

If $S$ is a finite set, and $a_s$ , $b_s$ are non-negative for $s\in S$ , then

\left(\sum_{s\in S}a_s\right)\log\frac{\sum_{s\in S} a_s}{\sum_{s\in S} b_s}$$. We require additionally that, if $b_s=0$, then $s_s=0$ as otherwise the right hand side should morally be infinite, which it can't be in the formalization using real numbers.

Exact Lean statement

lemma sum_mul_log_div_leq {a b : ι → ℝ} (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i)
    (habs : ∀ i ∈ s, b i = 0 → a i = 0) :
    (∑ i ∈ s, a i) * log ((∑ i ∈ s, a i) / (∑ i ∈ s, b i)) ≤ ∑ i ∈ s, a i * log (a i / b i)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma sum_mul_log_div_leq {a b : ι → ℝ} (ha : ∀ i ∈ s, 0 ≤ a i) (hb : ∀ i ∈ s, 0 ≤ b i)    (habs : ∀ i ∈ s, b i = 0 → a i = 0) :    (∑ i ∈ s, a i) * log ((∑ i ∈ s, a i) / (∑ i ∈ s, b i)) ≤ ∑ i ∈ s, a i * log (a i / b i) := by  by_cases h : ∀ i ∈ s, b i = 0  · have A : ∑ i ∈ s, b i = ∑ i ∈ s, 0 := Finset.sum_congr rfl (fun i hi ↦ h i hi)    have B : ∑ i ∈ s, a i * log (a i / b i) = ∑ i ∈ s, a i * log (a i / 0) := by      apply Finset.sum_congr rfl (fun i hi ↦ by simp [h i hi])    simp [A, B]  let B := ∑ i ∈ s, b i  have B_pos : 0 < B := by    apply Finset.sum_pos' hb    simp only [not_forall] at h    rcases h with ⟨i, hi, h'i⟩    exact ⟨i, hi, lt_of_le_of_ne (hb i hi) (Ne.symm h'i)⟩  suffices - (∑ i ∈ s, a i * log (a i / b i)) / B ≤        - ((∑ i ∈ s, a i) * log ((∑ i ∈ s, a i) / (∑ i ∈ s, b i))) / B by    rwa [div_le_div_iff_of_pos_right B_pos, neg_le_neg_iff] at this  have A : ∑ i ∈ s, b i / B = 1 := by simp [← Finset.sum_div, B, div_self B_pos.ne']  have A' : ∀ i ∈ s, 0 ≤ b i / B := fun i hi ↦ div_nonneg (hb i hi) B_pos.le  have A'' : ∀ i ∈ s, 0 ≤ a i / b i := fun i hi ↦ div_nonneg (ha i hi) (hb i hi)  convert! ConcaveOn.le_map_sum Real.concaveOn_negMulLog A' A (p := fun i ↦ a i / b i) A'' using 1  · simp only [negMulLog, neg_mul, smul_eq_mul, mul_neg, Finset.sum_neg_distrib]    rw [neg_div, Finset.sum_div]    congr 1    apply Finset.sum_congr rfl (fun i hi ↦ ?_)    rcases eq_or_lt_of_le (hb i hi) with h'i | h'i    · simp [← h'i, habs i hi h'i.symm]    · field_simp  · have : ∑ x ∈ s, b x / B * (a x / b x) = (∑ x ∈ s, a x) / B := by      rw [Finset.sum_div]      apply Finset.sum_congr rfl (fun i hi ↦ ?_)      rcases eq_or_lt_of_le (hb i hi) with h'i | h'i      · simp [← h'i, habs i hi h'i.symm]      · field_simp    simp only [negMulLog, smul_eq_mul, neg_mul, this]    ring