English
For a multiset s and a map f: s → R with nonzero values, the log derivative of the product equals the sum of the log derivatives of the factors.
Русский
Для многосета s и отображения f: s → R при не нулевых значениях аргументов логарифмический дериватив произведения равен сумме логарифмических деривативов факторов.
LaTeX
$$$\\logDeriv\\big(\\mathrm{prod}\\; (s.map\\, f)\\big) = \\big(\\mathrm{map}\\; (\\lambda x. \\logDeriv (f x))\\; s\\big).sum$$$
Lean4
theorem logDeriv_multisetProd {ι : Type*} (s : Multiset ι) {f : ι → R} (h : ∀ x ∈ s, f x ≠ 0) :
logDeriv (s.map f).prod = (s.map fun x ↦ logDeriv (f x)).sum :=
by
induction s using Multiset.induction_on
· simp
· rename_i h₂
simp only [Multiset.map_cons, Multiset.sum_cons, Multiset.prod_cons]
rw [← h₂]
· apply logDeriv_mul
· simp [h]
· simp_all
· simp_all
