hasProd_of_hasSum_log — Mathlib

English

The exponential of a convergent sum of complex logs equals the corresponding infinite product: exp(∑ log f_i) = ∏ f_i, under f_i ≠ 0 and convergence of the sum.

Русский

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

LaTeX

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

Lean4

theorem hasProd_of_hasSum_log (hfn : ∀ i, f i ≠ 0) (hf : HasSum (fun i ↦ log (f i)) a) : HasProd f (exp a) :=
  hf.cexp.congr (by simp [exp_log, hfn])

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