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.
The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral
Definition
Throughout, with , and vector-valued functions, their components and their limits are as in Vector-valued functions , their limits and continuity, with the dictionary to the metric notions.
The derivative
Let , let and let be a limit point of (Limit point, isolated point, adherent point, derived set, and dense subset of ). The difference quotient of at is the vector-valued function
the scalar multiple being that of the vector space (The vector space of all functions with pointwise operations, and as the case ); the division is legitimate because gives . As in The derivative of at a point that is a limit point of , and differentiability on a set, is a limit point of as well, since a punctured neighbourhood of omits .
is differentiable at when exists in , and then the derivative is
The notation denotes a single vector. At most one satisfies the limit condition, as proved in Vector-valued functions , their limits and continuity, with the dictionary to the metric notions; this is the vector-valued form of the obligation At a limit point of the domain a function has at most one limit discharges for real-valued functions and A sequence in a metric space has at most one limit for sequences.
The intrinsic form is the definition; the componentwise form is a theorem. For the -th component of is , which is the real difference quotient of at (The derivative of at a point that is a limit point of , and differentiability on a set). So by A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions clause 2:
is differentiable at if and only if every is differentiable at , and then for every .
Nothing below reverses this order of presentation: the intrinsic limit is what is defined, and the coordinates are read off it.
Algebra of derivatives. If are differentiable at and , then and are differentiable at with and : read componentwise through the displayed equivalence, these are clauses 1 and 2 of the published Sums, scalar multiples, products and quotients: , , , and when .
The integral
Let with and let (Intervals of : the nine order-convex forms, nondegeneracy, and length). is integrable on when every component is bounded (Lower bound, bounded below, bounded set) and Darboux integrable in the sense of The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation , and then
That really is an element of . In this library is the set of functions (The vector space of all functions with pointwise operations, and as the case ), not a set of tuples, so the displayed assignment is literally an element of it; each value is a single real by The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation . In the standard basis (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ) the same object is .
Oriented limits. Following The integral with oriented limits: and componentwise, set
so that for all in an interval on which is integrable. The clauses do not overlap with the case , so nothing has to be checked for consistency, exactly as in The integral with oriented limits: and .
Linearity. If are integrable and then is integrable with
since each side has -th coordinate and respectively, and those agree by Integrable functions on form a set closed under sums and scalar multiples, and .
Restriction and splitting. If is integrable on then it is integrable on every nondegenerate closed subinterval with , and for , ; both are the componentwise readings of A function integrable on is integrable on every closed subinterval and For : is integrable on if and only if it is integrable on and on , and then ; with the oriented form for arbitrary , applied to each and reassembled coordinate by coordinate.
Remarks
-
The two halves are independent. The derivative clause needs no integral and the integral clause needs no derivative; they are collected in one item because they are the two constructions of the one-dimensional theory that transfer to by the same move, and because If is differentiable with integrable then ; and a bounded derivative makes Lipschitz is what joins them.
-
Why the intrinsic derivative is stated first. The componentwise formula is the one used in computations, but it is tied to the standard basis, whereas the limit of the difference quotient is not. The intrinsic form is the one that survives when the domain is enlarged from an interval to a subset of , which is a later page of this track.
-
No norm appears in either definition. The derivative is a limit in , and by For all norms on are equivalent the same limits are obtained from any other norm, so the notion does not depend on the choice (The -norms for rational , and , The Euclidean inner product on ). The integral is defined coordinatewise and mentions no metric at all.
-
Integrability of is a separate matter and is not part of this definition: it is proved, together with the inequality it belongs to, in For and integrable when , ; for , is integrable.
Depends on
Vector-valued functions , their limits and continuity, with the dictionary to the metric notions
A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
For all norms on are equivalent
Equivalent norms, and the dictionary with equivalent metrics
The derivative of at a point that is a limit point of , and differentiability on a set
The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation
The integral with oriented limits: and
Integrable functions on form a set closed under sums and scalar multiples, and
Sums, scalar multiples, products and quotients: , , , and when
A sequence in a metric space has at most one limit
The - limit of at a limit point of
At a limit point of the domain a function has at most one limit
The vector space of all functions with pointwise operations, and as the case
The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension
Intervals of : the nine order-convex forms, nondegeneracy, and length
A function integrable on is integrable on every closed subinterval
For : is integrable on if and only if it is integrable on and on , and then ; with the oriented form for arbitrary
Limit point, isolated point, adherent point, derived set, and dense subset of
The -norms for rational , and
The Euclidean inner product on
Lower bound, bounded below, bounded set