English
The exponential of a convergent sum of real logs equals the corresponding finite 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 real logs is the corresponding infinite product. -/
theorem rexp_tsum_eq_tprod (hfn : ∀ i, 0 < f i) (hf : Summable fun i ↦ log (f i)) :
rexp (∑' i, log (f i)) = ∏' i, f i :=
(hasProd_of_hasSum_log hfn hf.hasSum).tprod_eq.symm