map_sum — Mathlib

English

Let f be continuous multilinear, then the sum identity holds: f(∑_i m_i) equals the sum over all coordinate selections r of f(m_i(r_i)).

Русский

Пусть f непрерывно мультилинейно; тогда выполняется тождение: f(∑ m_i) = ∑ f(m_i(r_i)) по всем выборкам координат r.

LaTeX

$$$f(\sum_i m_i) = \sum_{r: \forall i, \alpha_i} f(m_i(r_i)).$$$

Lean4

/-- If `f` is continuous multilinear, then `f (Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is the sum of
`f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions `r`. This follows from
multilinearity by expanding successively with respect to each coordinate. -/
theorem map_sum [DecidableEq ι] [∀ i, Fintype (α i)] : (f fun i => ∑ j, g i j) = ∑ r : ∀ i, α i, f fun i => g i (r i) :=
  f.toMultilinearMap.map_sum _

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