English
For a finite index set s and nonzero values f(i), log of the product equals the sum of logs: log(∏ i∈s f(i)) = ∑ i∈s log(f(i)).
Русский
Для конечного множества индексов s и непустых значений f(i) верно log(произведение f(i)) = сумма log(f(i)).
LaTeX
$$$\\\\forall s : Finset\\\\alpha, \\\\forall f : \\\\alpha \\\\to \\\\mathbb{R}, \\\\forall hf : \\\\forall x \\\\in s, f x \\\\ne 0, \\\\log (\\\\prod i \\\\in s, f i) = \\\\sum i \\\\in s, \\\\log (f i)$$$
Lean4
theorem log_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) :
log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i) := by
induction s using Finset.cons_induction_on with
| empty => simp
| cons a s ha ih =>
rw [Finset.forall_mem_cons] at hf
simp [ih hf.2, log_mul hf.1 (Finset.prod_ne_zero_iff.2 hf.2)]
