English
Let f be a finitely supported function f: α →₀ β into a pointed set with zero, and let g be a family g(a, b) of real numbers indexed by α and by b ∈ β, such that for every a, g(a, f(a)) = 0 implies f(a) = 0. Then the logarithm of the product ∏_{a} g(a, f(a)) equals the sum over a of the logarithms log(g(a, f(a))).
Русский
Пусть f = fакф данные с конечной опорой: f: α →₀ β, β с нулём, и пусть g задаёт семейство числовых значений g(a, b) ∈ ℝ, индексированное по a ∈ α и b ∈ β, такое что для каждого a верно: g(a, f(a)) = 0 влечёт f(a) = 0. Тогда логарифм произведения ∘ по всем a даёт равенство: log(∏_{a} g(a, f(a))) = ∑_{a} log(g(a, f(a))).
LaTeX
$$$\\log\\bigl(f \\prod g\\bigr) = f \\sum (\\lambda a\, b.\ \log(g(a,b))).$$$
Lean4
protected theorem _root_.Finsupp.log_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ)
(hg : ∀ a, g a (f a) = 0 → f a = 0) : log (f.prod g) = f.sum fun a b ↦ log (g a b) :=
log_prod _ _ fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀
