cexp — Mathlib

English

If a real-valued function f has sum a over an index type, then the product of exp(f(i)) over the index equals exp(a).

Русский

Если f имеет сумму a по индексу i, то произведение exp(f(i)) по индексу i равно exp(a).

LaTeX

$$$ \text{HasSum } f a \Rightarrow \text{HasProd } (\exp \circ f) (\exp a) $$$

Lean4

/-- If `f` has sum `a`, then `exp ∘ f` has product `exp a`. -/
theorem «cexp» {ι : Type*} {f : ι → ℂ} {a : ℂ} (h : HasSum f a) : HasProd (cexp ∘ f) (cexp a) :=
  Filter.Tendsto.congr (fun s ↦ exp_sum s f) <| Filter.Tendsto.cexp h

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