expSeries — Mathlib

English

The exponential series is the ofScalars series: the nth term is inv(n!) and the nth multilinear map is scaled accordingly.

Русский

Серия экспоненты образует последовательность через скаляры: n-я часть равна 1/n!, и соответствующая линейная карта масштабируется.

LaTeX

$$$\expSeries 𝕂 𝔸 = \mathrm{ofScalars}_{\mathbb{A}}\; (n \mapsto (n!)^{-1})$$$

Lean4

/-- `expSeries 𝕂 𝔸` is the `FormalMultilinearSeries` whose `n`-th term is the map
`(xᵢ) : 𝔸ⁿ ↦ (1/n! : 𝕂) • ∏ xᵢ`. Its sum is the exponential map `NormedSpace.exp 𝕂 : 𝔸 → 𝔸`. -/
def expSeries : FormalMultilinearSeries 𝕂 𝔸 𝔸 := fun n => (n !⁻¹ : 𝕂) • ContinuousMultilinearMap.mkPiAlgebraFin 𝕂 n 𝔸

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