PFR/Mathlib/Analysis/SpecialFunctions/NegMulLog.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma Real.sum_mul_log_div_leq Documented declaration: sum_mul_log_div_leq line 32 source

   Source documentation

   If $S$ is a finite set, and $a_s$, $b_s$ are non-negative for $s\in S$, then $$\sum_{s\in S} a_s \log\frac{a_s}{b_s}\ge \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.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Real, Membership.mem, LE.le, OfNat.ofNat, Eq, HMul.hMul, Finset.sum, Real.log, HDiv.hDiv

   Proof uses: dite, Finset.sum_congr, rfl, of_eq_true, Eq.trans, True, congr, congrArg, div_zero, Real.log_zero, MulZeroClass.mul_zero, eq_self, Finset.sum_const_zero, Eq.refl, Not, LT.lt, Finset.sum_pos', Exists, And, Eq.mp and 117 more

   148 instances, coercions and auxiliary constants left out.

   Tactic trace: 41 steps

   Open to load the checked before-and-after goal states.

   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
   …

2. lemma Real.sum_mul_log_div_eq_iff_aux If equality holds in the previous bound, then $a_s=r\cdot b_s$ for every $s\in S$, for some constant $r\in \mathbb{R}$ line 71 source

   Source documentation

   If equality holds in the previous bound, then $a_s=r\cdot b_s$ for every $s\in S$, for some constant $r\in \mathbb{R}$. Auxiliary version assuming the b i are positive.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Real, Membership.mem, LE.le, OfNat.ofNat, LT.lt, Eq, Finset.sum, HMul.hMul, Real.log, HDiv.hDiv, Exists

   Proof uses: EmptyCollection.emptyCollection, Finset.Nonempty, Or, Finset.eq_empty_or_nonempty, of_eq_true, Eq.trans, True, congrArg, funext, forall_congr, False, implies_congr, Eq.refl, implies_true, Eq.symm, Finset.sum_pos, congrFun', Finset.sum_congr, div_self, LT.lt.ne' and 66 more

   125 instances, coercions and auxiliary constants left out.

   Tactic trace: 24 steps

   Open to load the checked before-and-after goal states.

   lemma sum_mul_log_div_eq_iff_aux {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)) :
       ∃ r, ∀ i ∈ s, a i = r * (b i) := by
   …

3. lemma Real.sum_mul_log_div_eq_iff If equality holds in the previous bound, then $a_s=r\cdot b_s$ for every $s\in S$, for some constant $r\in \mathbb{R}$ line 99 source

   Source documentation

   If equality holds in the previous bound, then $a_s=r\cdot b_s$ for every $s\in S$, for some constant $r\in \mathbb{R}$.

   standard axioms: Classical.choice, Quot.sound, propext what this means

   Statement uses: Finset, Real, Membership.mem, LE.le, OfNat.ofNat, Eq, Finset.sum, HMul.hMul, Real.log, HDiv.hDiv, Exists

   Proof uses: Finset.filter, LT.lt, Finset.sum_subset, Finset.filter_subset, Not, le_antisymm, Eq.mp, Eq.trans, congrArg, And, True, congrFun', eq_true, true_and, Eq.mpr, eq_of_heq, HEq, Eq.refl, HEq.refl, Eq.symm and 13 more

   51 instances, coercions and auxiliary constants left out.

   Tactic trace: 36 steps

   Open to load the checked before-and-after goal states.

   lemma sum_mul_log_div_eq_iff {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))) :
       ∃ r, ∀ i ∈ s, a i = r * (b i) := by
   …