rexp_tsum_eq_tprod — Mathlib

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

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