English
For finite index set, f(x+h) equals f(x) plus the derivative term plus a finite sum of higher order terms.
Русский
Для конечного множества индексов f(x+h) равно f(x) плюс линейный вклад производной и конечная сумма высших порядков.
LaTeX
$$$$f(x+h) = f(x) + f.linearDeriv x(h) + \sum_{s:\, 2 \le |s|} f(s.piecewise(h,x)).$$$$
Lean4
theorem map_add_eq_map_add_linearDeriv_add [DecidableEq ι] [Fintype ι] (x h : (i : ι) → M₁ i) :
f (x + h) = f x + f.linearDeriv x h + ∑ s with 2 ≤ #s, f (s.piecewise h x) :=
by
rw [add_comm, map_add_univ, ← Finset.powerset_univ, ← sum_filter_add_sum_filter_not _ (2 ≤ #·)]
simp_rw [not_le, Nat.lt_succ, le_iff_lt_or_eq (b := 1), Nat.lt_one_iff, filter_or, ← powersetCard_eq_filter,
sum_union (univ.pairwise_disjoint_powersetCard zero_ne_one), powersetCard_zero, powersetCard_one, sum_singleton,
Finset.piecewise_empty, sum_map, Function.Embedding.coeFn_mk, Finset.piecewise_singleton, linearDeriv_apply,
add_comm]
