English
The difference f(x+h) − f(x+h′) minus the derivative at x of (h−h′) equals a sum of second-order terms.
Русский
Разность f(x+h) − f(x+h′) минус производная f по (h−h′) равна сумме вторичных членов порядка.
LaTeX
$$$$f(x+h) - f(x+h') - f.linearDeriv x(h-h') = \sum_{s, 2 \le |s|} (f(s.piecewise(h,x) - f(s.piecewise(h',x))).$$$$
Lean4
/-- This expresses the difference between the values of a multilinear map
at two points "close to `x`" in terms of the "derivative" of the multilinear map at `x`
and of "second-order" terms. -/
theorem map_add_sub_map_add_sub_linearDeriv [DecidableEq ι] [Fintype ι] (x h h' : (i : ι) → M₁ i) :
f (x + h) - f (x + h') - f.linearDeriv x (h - h') = ∑ s with 2 ≤ #s, (f (s.piecewise h x) - f (s.piecewise h' x)) :=
by
simp_rw [map_add_eq_map_add_linearDeriv_add, add_assoc, add_sub_add_comm, sub_self, zero_add, ← LinearMap.map_sub,
add_sub_cancel_left, sum_sub_distrib]
