English
The logarithmic derivative of a finite product equals the sum of the logarithmic derivatives of the factors.
Русский
Логарифмическая производная конечного произведения равна сумме логарифмических производных множителей.
LaTeX
$$$\logDeriv\left(\prod_{i\in s} f_i\right)(x) = \sum_{i\in s} \logDeriv(f_i)(x)$$$
Lean4
/-- The logarithmic derivative of a finite product is the sum of the logarithmic derivatives. -/
theorem logDeriv_prod {ι : Type*} (s : Finset ι) (f : ι → 𝕜 → 𝕜') (x : 𝕜) (hf : ∀ i ∈ s, f i x ≠ 0)
(hd : ∀ i ∈ s, DifferentiableAt 𝕜 (f i) x) : logDeriv (∏ i ∈ s, f i ·) x = ∑ i ∈ s, logDeriv (f i) x := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha ih =>
rw [Finset.forall_mem_cons] at hf hd
simp_rw [Finset.prod_cons, Finset.sum_cons]
rw [logDeriv_mul, ih hf.2 hd.2]
· exact hf.1
· simpa [Finset.prod_eq_zero_iff] using hf.2
· exact hd.1
· exact .fun_finset_prod hd.2
