English
If f is continuous multilinear, then summing inputs pointwise over i with indices in α_i yields equality with summing over all choice functions r: ∀ i, α_i.
Русский
Если f непрерывно мультилинейно, то сумма по входам в точке по индексам α_i эквивалентна сумме по всем функциям r: ∀ i, α_i.
LaTeX
$$$\sum_i f\bigl(\sum_j g(i,j)\bigr) = \sum_{r: \forall i, \alpha_i} f\bigl(g(i,r(i))\bigr).$$$
Lean4
/-- If `f` is continuous multilinear, then `f (Σ_{j₁ ∈ A₁} g₁ j₁, ..., Σ_{jₙ ∈ Aₙ} gₙ jₙ)` is the
sum of `f (g₁ (r 1), ..., gₙ (r n))` where `r` ranges over all functions with `r 1 ∈ A₁`, ...,
`r n ∈ Aₙ`. This follows from multilinearity by expanding successively with respect to each
coordinate. -/
theorem map_sum_finset [DecidableEq ι] : (f fun i => ∑ j ∈ A i, g i j) = ∑ r ∈ piFinset A, f fun i => g i (r i) :=
f.toMultilinearMap.map_sum_finset _ _
