English
For a finite index set s and a function f: s → ℝ, log⁺(∏_{t∈s} f(t)) ≤ ∑_{t∈s} log⁺(f(t)).
Русский
Для конечного множества индексов s и функции f: s → ℝ верно: log⁺(∏_{t∈s} f(t)) ≤ ∑_{t∈s} log⁺(f(t)).
LaTeX
$$$\log^{+}\left(\prod_{t \in s} f(t)\right) \le \sum_{t \in s} \log^{+}(f(t))$$$
Lean4
/-- Estimate for `log⁺` of a product. See `Real.posLog_mul` for a variant with
only two factors. -/
theorem posLog_prod {α : Type*} (s : Finset α) (f : α → ℝ) : log⁺ (∏ t ∈ s, f t) ≤ ∑ t ∈ s, log⁺ (f t) := by
classical
induction s using Finset.induction with
| empty => simp [posLog]
| insert a s ha hs =>
calc
log⁺ (∏ t ∈ insert a s, f t)
_ = log⁺ (f a * ∏ t ∈ s, f t) := by rw [Finset.prod_insert ha]
_ ≤ log⁺ (f a) + log⁺ (∏ t ∈ s, f t) := posLog_mul
_ ≤ log⁺ (f a) + ∑ t ∈ s, log⁺ (f t) := (add_le_add (by rfl) hs)
_ = ∑ t ∈ insert a s, log⁺ (f t) := by rw [Finset.sum_insert ha]
