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 $f : A \to \mathbb{R}^m$, 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 $n \ge 1$ all norms on $\mathbb{R}^n$ are equivalent
- Equivalent norms, and the dictionary with equivalent metrics
- The derivative $f'(c) = \lim_{x \to c} \frac{f(x) - f(c)}{x - c}$ of $f : A \to \mathbb{R}$ at a point $c \in A$ that is a limit point of $A$, and differentiability on a set
- The lower and upper Darboux integrals of a bounded $f$ on $[a,b]$ as $\sup_P L(f,P)$ and $\inf_P U(f,P)$, Darboux integrability as their equality, and the notation $\int_a^b f$
- The integral with oriented limits: $\int_a^a f := 0$ and $\int_b^a f := -\int_a^b f$
- Integrable functions on $[a,b]$ form a set closed under sums and scalar multiples, and $\int_a^b(\lambda f+\mu g) = \lambda\int_a^b f + \mu\int_a^b g$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- A sequence in a metric space has at most one limit
- The $\varepsilon$-$\delta$ limit $\lim_{x \to c} f(x) = L$ of $f : A \to \mathbb{R}$ at a limit point $c$ of $A$
- At a limit point of the domain a function has at most one limit
- The vector space $F^{X}$ of all functions $X \to F$ with pointwise operations, and $F^{n}$ as the case $X = n = \{0, 1, \dots, n-1\}$
- The standard list $e : n \to F^{n}$ with $e_i(i) = 1_F$ and $e_i(j) = 0_F$ for $j \ne i$ is an ordered basis of $F^{n}$; hence $\dim_F F^{n} = n$, and $F^{0}$ is the zero space with basis $\varnothing$ and dimension $0$
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- A function integrable on $[a,b]$ is integrable on every closed subinterval
- For $a<c<b$: $f$ is integrable on $[a,b]$ if and only if it is integrable on $[a,c]$ and on $[c,b]$, and then $\int_a^b f = \int_a^c f + \int_c^b f$; with the oriented form for arbitrary $a,b,c$
- Limit point, isolated point, adherent point, derived set, and dense subset of $\mathbb{R}$
- The $p$-norms $\lVert x\rVert_p$ for rational $p \ge 1$, and $\lVert x\rVert_\infty$
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Lower bound, bounded below, bounded set
Used by
- If f : [a,b] → ℝᵐ is differentiable with integrable f' then ∫ₐᵇ f' = f(b)-f(a); and a bounded derivative makes f Lipschitz Corollary
- A curve for which the mean value inequality is an equality, showing the constant cannot be improved Counterexample
- f(t) = (t², t³) on [0,1]: no ξ satisfies f(1)-f(0) = f'(ξ) Counterexample
- x²y/(x⁴+y²) tends to zero on every line through the origin but not along y=x² Counterexample
- Directional derivatives and partial derivatives of a map U⊆ℝᵐ→ℝⁿ Definition
- A convergent sequence in ℝ³ and the integral ∫₀¹ (1, t, t²), computed componentwise Example
- Conventions of this page, the standing n ≥ 1 hypothesis, and what is taken up elsewhere in the reading order Remark
- For a ≤ b and f : [a,b] → ℝᵐ integrable when a<b, ‖∫ₐᵇ f‖₂ ≤ ∫ₐᵇ ‖ f‖₂; for a<b, ‖ f‖₂ is integrable Theorem
- The mean value inequality: if f : [a,b] → ℝᵐ is continuous and differentiable on (a,b) with ‖ f'‖₂ ≤ M, then ‖ f(b)-f(a)‖₂ ≤ M(b-a) Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 214 results over 35 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
- Vector-valued function (Wikipedia) (standard reference, not scraped)
- Riemann integral (Wikipedia) (standard reference, not scraped)
- J. Lebl, Basic Analysis I, Section 8.4 (standard reference, not scraped)