English
For any k,l and s with card s = l, the term p.changeOriginSeriesTerm k l s hs applied to x and y equals p(k+l) evaluated at the s-pieced combination of x and y.
Русский
Для любых k,l и s с card s = l, терм p.changeOriginSeriesTerm k l s hs, приложенный к x и y, равен p(k+l) на разбиении x и y по s.
LaTeX
$$p.changeOriginSeriesTerm k l s hs (x) (y) = p (k+l) (s.piecewise (fun _ => x) (fun _ => y))$$
Lean4
/-- A term of `FormalMultilinearSeries.changeOriginSeries`.
Given a formal multilinear series `p` and a point `x` in its ball of convergence,
`p.changeOrigin x` is a formal multilinear series such that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense. Each term of `p.changeOrigin x`
is itself an analytic function of `x` given by the series `p.changeOriginSeries`. Each term in
`changeOriginSeries` is the sum of `changeOriginSeriesTerm`'s over all `s` of cardinality `l`.
The definition is such that `p.changeOriginSeriesTerm k l s hs (fun _ ↦ x) (fun _ ↦ y) =
p (k + l) (s.piecewise (fun _ ↦ x) (fun _ ↦ y))`
-/
def changeOriginSeriesTerm (k l : ℕ) (s : Finset (Fin (k + l))) (hs : s.card = l) : E [×l]→L[𝕜] E [×k]→L[𝕜] F :=
let a :=
ContinuousMultilinearMap.curryFinFinset 𝕜 E F hs
(by rw [Finset.card_compl, Fintype.card_fin, hs, add_tsub_cancel_right])
a (p (k + l))
