logb_prod — Mathlib

English

The log of a finite product equals the sum of logs of the factors, provided all factors are nonzero.

Русский

Логарифм произведения конечного числа множителей равен сумме логарифмов этих множителей при условии их ненулевости.

LaTeX

$$$\log_b b\ (\prod_{i\in s} f_i) = \sum_{i\in s} \log_b b (f_i)$$$

Lean4

theorem logb_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) :
    logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i) := by
  induction s using Finset.cons_induction_on with
  | empty => simp
  | cons => simp_all [logb_mul, Finset.prod_ne_zero_iff]

Похожие утверждения