English
If the index set ι is arbitrary and the family {f_i} of functions is such that logDeriv of each f_i is summable at x and the locally uniform product exists, then the log-derivative of the infinite product equals the sum of the log-derivatives.
Русский
Если множество индексов ι произвольно, семейство функций {f_i} обладает суммируемостью logDeriv f_i в точке x и существует локально равномерный произведение, то логарифмическая производная бесконечного произведения равна сумме логарифмических производных.
LaTeX
$$$\displaystyle \logDeriv\Bigl(\prod_{i}^{\prime} f_i\cdot\Bigr)(x) = \sum_{i}^{\prime} \logDeriv\bigl(f_i\bigr)(x)$$$
Lean4
theorem logDeriv_tprod_eq_tsum {ι : Type*} {s : Set ℂ} (hs : IsOpen s) {x : s} {f : ι → ℂ → ℂ} (hf : ∀ i, f i x ≠ 0)
(hd : ∀ i, DifferentiableOn ℂ (f i) s) (hm : Summable fun i ↦ logDeriv (f i) x)
(htend : MultipliableLocallyUniformlyOn f s) (hnez : ∏' i, f i x ≠ 0) :
logDeriv (∏' i, f i ·) x = ∑' i, logDeriv (f i) x :=
by
rw [Eq.comm, ← hm.hasSum_iff]
refine logDeriv_tendsto hs x htend.hasProdLocallyUniformlyOn (.of_forall <| by fun_prop) hnez |>.congr fun b ↦ ?_
rw [logDeriv_prod _ _ _ (fun i _ ↦ hf i) (fun i _ ↦ (hd i x x.2).differentiableAt (hs.mem_nhds x.2))]
