TheoremStatement: AI-adaptedProof: AI-generated

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.

Sums and scalar multiples of totally differentiable maps are totally differentiable with the expected derivatives

Statement

If $f, g : U \to R^{n}$ are totally differentiable at $a$ and $c \in R$ , then $f + g$ and $c f$ are totally differentiable at $a$ , with

$D (f + g) (a) = D f (a) + D g (a), D (c f) (a) = c D f (a) .$

Facts & Assumptions

Given: Total first-order expansions for $f$ and $g$ at $a$ .

[L1]

The total-derivative definition supplies the normwise remainder estimate for every $ε > 0$ ; in positive source dimension this is equivalently the normalized remainder tending to zero as $h$ tends to zero (The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder).

[L2]

A norm satisfies the triangle inequality and $∥ c w ∥ = ∣ c ∣ ∥ w ∥$ (A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

Proof

technique · direct

1.1givenL1L2algebra

If the source dimension is zero, each derivative is the unique map from the zero space and the remainder condition holds on its sole increment. If $n = 0$ , both functions and all candidate derivatives take only the zero value. In either case the displayed sum and scalar-multiple identities hold for these unique zero linear maps. For the remainder assume that both source and target dimensions are positive.

1.2L1L2

Add the two expansions and multiply the first by $c$ to obtain remainders $r_{f} + r_{g}$ for $f + g$ and $c r_{f}$ for $c f$ , with the displayed candidate linear maps.

2.1step 1.2L2algebra

By [L2], $∥ r_{f} (h) + r_{g} (h) ∥_{2} / ∥ h ∥_{2}$ is bounded by the sum of two quantities tending to zero, and $∥ c r_{f} (h) ∥_{2} / ∥ h ∥_{2} = ∣ c ∣ ∥ r_{f} (h) ∥_{2} / ∥ h ∥_{2}$ tends to zero (also when $c = 0$ ).

3.1step 1.2step 2.1∎

Sums and scalar multiples of linear maps are linear, so step 2.1 verifies the definition with exactly the two stated derivatives.

Depends on

Dependency tree · 2 levels

Sources

J. Lebl, Basic Analysis I, §8.3