Theorems · Theorem · real analysis

logDeriv_tprod_eq_tsum

∀ {ι : Type u_1} {s : Set ℂ},
  IsOpen s →
    ∀ {x : ℂ},
      x ∈ s →
        ∀ {f : ι → ℂ → ℂ},
          (∀ (i : ι), f i x ≠ 0) →
            (∀ (i : ι), DifferentiableOn ℂ (f i) s) →
              (Summable fun i => logDeriv (f i) x) →
                MultipliableLocallyUniformlyOn f s →
                  ∏' (i : ι), f i x ≠ 0 → logDeriv (fun x => ∏' (i : ι), f i x) x = ∑' (i : ι), logDeriv (f i) x

Defined in

Mathlib.Analysis.Calculus.LogDerivUniformlyOn

Cited by

1 results in Mathlib

Foundations

Depth 293 from the axioms · uses propext, Classical.choice, Quot.sound