English
Let s be a finite set and f: s → ℝ. Then log⁺(∑_{t∈s} f(t)) ≤ log(|s|) + ∑_{t∈s} log⁺(f(t)).
Русский
Пусть s конечное; тогда log⁺(∑_{t∈s} f(t)) ≤ log(|s|) + ∑_{t∈s} log⁺(f(t)).
LaTeX
$$$\log^{+}\left(\sum_{t \in s} f(t)\right) \le \log(|s|) + \sum_{t \in s} \log^{+}(f(t))$$$
Lean4
/-- Estimate for `log⁺` of a sum. See `Real.posLog_add` for a variant involving
just two summands. -/
theorem posLog_sum {α : Type*} (s : Finset α) (f : α → ℝ) : log⁺ (∑ t ∈ s, f t) ≤ log (s.card) + ∑ t ∈ s, log⁺ (f t) :=
by
-- Trivial case: empty sum
by_cases hs : s = ∅
·
simp [hs, posLog]
-- Nontrivial case: Obtain maximal element…
obtain ⟨t_max, ht_max⟩ :=
s.exists_max_image (fun t ↦ |f t|)
(Finset.nonempty_iff_ne_empty.mpr hs)
-- …then calculate
calc
log⁺ (∑ t ∈ s, f t)
_ = log⁺ |∑ t ∈ s, f t| := by rw [Real.posLog_abs]
_ ≤ log⁺ (∑ t ∈ s, |f t|) :=
by
apply monotoneOn_posLog (by simp) (by simp [Finset.sum_nonneg])
simp [Finset.abs_sum_le_sum_abs]
_ ≤ log⁺ (∑ t ∈ s, |f t_max|) :=
by
apply monotoneOn_posLog (by simp [Finset.sum_nonneg]) (by simp; positivity)
apply Finset.sum_le_sum (fun i ih ↦ ht_max.2 i ih)
_ = log⁺ (s.card * |f t_max|) := by simp [Finset.sum_const]
_ ≤ log s.card + log⁺ |f t_max| := posLog_nat_mul
_ ≤ log s.card + ∑ t ∈ s, log⁺ (f t) := by
gcongr
rw [posLog_abs]
apply Finset.single_le_sum (fun _ _ ↦ posLog_nonneg) ht_max.1
