cexp_tsum_eq_tprod — Mathlib

English

The exponential of a convergent sum of complex logs equals the corresponding product: exp(∑ log f_i) = ∏ f_i.

Русский

Экспонента сходящейся суммы логарифмов равна соответствующему произведению: exp(∑ log f_i) = ∏ f_i.

LaTeX

$$$\exp\left(\sum_{i} \log(f_i)\right) = \prod_{i} f_i$$$

Lean4

/-- The exponential of a convergent sum of complex logs is the corresponding infinite product. -/
theorem cexp_tsum_eq_tprod (hfn : ∀ i, f i ≠ 0) (hf : Summable fun i ↦ log (f i)) :
    cexp (∑' i, log (f i)) = ∏' i, f i :=
  (hasProd_of_hasSum_log hfn hf.hasSum).tprod_eq.symm

Похожие утверждения