The Logarithmic derivative of an infinite product #
We show that if we have an infinite product of functions f that is locally uniformly convergent,
then the logarithmic derivative of the product is the sum of the logarithmic derivatives of the
individual functions.
theorem
logDeriv_tprod_eq_tsum
{ι : Type u_1}
{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)
: