logb_prod — Mathlib

English

A generalized product rule for logb holds for finitely supported functions with a suitable nonzero condition.

Русский

Обобщённое правило произведения для log_b справедливо для функции с конечной поддержкой при заданном условии ненулевости.

LaTeX

$$$\text{logb}_b (f \ prod g) = \sum a, (f a) \cdot \log_b b (g a)$ under suitable hg$$

Lean4

protected theorem _root_.Finsupp.logb_prod {α β : Type*} [Zero β] (f : α →₀ β) (g : α → β → ℝ)
    (hg : ∀ a, g a (f a) = 0 → f a = 0) : logb b (f.prod g) = f.sum fun a c ↦ logb b (g a c) :=
  logb_prod _ _ fun _x hx h₀ ↦ Finsupp.mem_support_iff.1 hx <| hg _ h₀

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