LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-02

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Repeated derivatives along a line expand by the multinomial formula

Statement

Let $k\in\mathbb N$ , let $U\subseteq\mathbb R^m$ be open, $f\in C^k(U)$ , and let $I\subseteq\mathbb R$ be an open interval such that $a+th\in U$ for every $t\in I$ . Write $\iota:\mathbb N\to\mathbb R$ for the canonical-natural map of The canonical natural $\iota(n) = n \cdot 1_F$ of a field. For $g(t)=f(a+th)$ and every $0\le r\le k$ ,

$g^{(r)}(t)=\sum_{|\alpha|=r}\frac{\iota(r!)}{\iota(\alpha!)}D^\alpha f(a+th)h^\alpha\qquad(t\in I).$

Facts & Assumptions

Given: The stated open-domain, open-interval, $C^k$ , and direction hypotheses.

[L1]

A function with continuous first partial derivatives near a point is totally differentiable there, and the total chain rule then applies to the affine line map $t\mapsto a+th$ (If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$ ).

[L2]

Ordered mixed derivatives through order $k$ commute under permutation (Continuous mixed partials of order $k$ are invariant under permutations).

[L3]

The multi-index conventions $|\alpha|$ , $\alpha!$ , $h^\alpha$ , and the canonical derivative $D^\alpha f$ are those of $C^k$ maps and multi-index derivative notation in Euclidean space.

[L4]

The canonical-natural map carries finite natural sums and products to the corresponding real sums and products (The canonical natural $\iota(n) = n \cdot 1_F$ of a field, Laws of finite sums and products in $\mathbb{N}$ , and $\iota\big(\sum_{k<n} a_k\big) = \sum_{k<n} \iota(a_k)$ ).

Proof

technique · induction

1.1

For $r=0$ the displayed sum consists of the zero multi-index and equals $f(a+th)=g(t)$ .

baseL3

1.2

Fix $r<k$ and assume the formula at order $r$ .

1.3

Each $D^\alpha f$ with $|\alpha|=r$ has continuous first partials, so [L1] differentiates its composition with the affine line. By [L3], we use the canonical multi-index notation for the resulting derivatives. When $r=0$ the resulting first derivatives are already canonical; when $r\ge1$ , [L2] permits the resulting derivatives to be written as $D^{\alpha+e_i}f$ . By [L4], collecting the coefficient of a fixed $\beta$ with $|\beta|=r+1$ gives

$\sum_{i:\,\beta_i>0}\frac{\iota(r!)}{\iota((\beta-e_i)!)}=\frac{\iota(r!)}{\iota(\beta!)}\sum_{i<m}\iota(\beta_i)=\frac{\iota((r+1)!)}{\iota(\beta!)}.$

Thus the formula at order $r+1$ follows. [step 1.2, L1, L2, L3, L4, algebra]

2.1

Steps 1.1--2.1 prove the formula successively for every $r\le k$ .

step 1.1step 1.2step 1.3discharge-induction∎

Depends on

Used by

Multivariable Taylor formula with a Lagrange remainder along a line segment Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 102 results over 28 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

MAT237 notes: Taylor's theorem in several variables (standard reference, not scraped)