TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)

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.

For $a \le b$ and $f : [a,b] \to \mathbb{R}^m$ integrable when $a<b$ , $\bigl\lVert\int_a^b f\bigr\rVert_2 \le \int_a^b \lVert f\rVert_2$ ; for $a<b$ , $\lVert f\rVert_2$ is integrable

Statement

Let $m \in \mathbb{N}$ with $m \ge 1$ , let $a, b \in \mathbb{R}$ with $a \le b$ and let $f : [a,b] \to \mathbb{R}^{m}$ . If $a<b$ , assume that $f$ is integrable (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral). Then:

if $a < b$ , the real-valued function $t \mapsto \lVert f(t)\rVert_2$ is integrable on $[a,b]$ (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 $p$ -norms $\lVert x\rVert_p$ for rational $p \ge 1$ , and $\lVert x\rVert_\infty$ );
$\Bigl\lVert \int_a^b f \Bigr\rVert_2 \;\le\; \int_a^b \lVert f\rVert_2 .$

The hypothesis $a \le b$ is not decoration. With the orientation convention of The integral with oriented limits: $\int_a^a f := 0$ and $\int_b^a f := -\int_a^b f$ and The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, interchanging the limits changes the sign of the right-hand side but not of the left, so for $b < a$ the correct statement is $\bigl\lVert\int_a^b f\bigr\rVert_2 \le \bigl|\int_a^b \lVert f\rVert_2\bigr|$ ; the displayed inequality as written is false in that case. This is the same trap the scalar inequality of If $f,g$ are integrable on $[a,b]$ then so are $\lvert f\rvert$ , $f^{2}$ , $fg$ , $\max(f,g)$ and $\min(f,g)$ , and $\bigl\lvert\int_a^b f\bigr\rvert \le \int_a^b\lvert f\rvert$ carries.

Clause 1 is a genuine obligation and is discharged before the estimate. That each $f_i$ is integrable does not by itself say that $\sqrt{\sum_{i<m} f_i^{2}}$ is; the square root has to be brought in through If $f$ is integrable on $[a,b]$ with values in $[m,M]$ and $\varphi$ is continuous on $[m,M]$ , then $\varphi \circ f$ is integrable.

Facts & Assumptions

Given: A natural $m \ge 1$ , reals $a \le b$ , a function $f : [a,b] \to \mathbb{R}^{m}$ that is integrable when $a<b$ , with components $f_0,\dots,f_{m-1}$ , and the vector $v := \int_a^b f \in \mathbb{R}^{m}$ ; write $g(t) := \sum_{i<m} f_i(t)^{2}$ , so that $\lVert f(t)\rVert_2 = \sqrt{g(t)}$ (The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$ , The $p$ -norms $\lVert x\rVert_p$ for rational $p \ge 1$ , and $\lVert x\rVert_\infty$ ).

[L1]

The vector-valued integral is componentwise: when $a<b$ , $f$ is integrable exactly when every $f_i$ is bounded and Darboux integrable, and then $\bigl(\int_a^b f\bigr)_i = \int_a^b f_i$ ; $\int_a^a f = 0$ (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, 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$ , Lower bound, bounded below, bounded set).

[L2]

Linearity of the integral: integrable functions on $[a,b]$ are closed under sums and scalar multiples, and $\int_a^b(\lambda u + \mu w) = \lambda\int_a^b u + \mu\int_a^b w$ (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$ ).

[L3]

Monotonicity of the integral: for $a<b$ and integrable $u \le w$ on $[a,b]$ , $\int_a^b u \le \int_a^b w$ ; and an integrable $u \ge 0$ has $\int_a^b u \ge 0$ (If $f \le g$ on $[a,b]$ and both are integrable then $\int_a^b f \le \int_a^b g$ ; and $m(b-a) \le \int_a^b f \le M(b-a)$ ).

[L4]

Products and squares: if $u,w$ are integrable on $[a,b]$ then so are $|u|$ , $u^{2}$ and $uw$ (If $f,g$ are integrable on $[a,b]$ then so are $\lvert f\rvert$ , $f^{2}$ , $fg$ , $\max(f,g)$ and $\min(f,g)$ , and $\bigl\lvert\int_a^b f\bigr\rvert \le \int_a^b\lvert f\rvert$ ).

[L5]

Composition: if $u$ is integrable on $[a,b]$ with values in $[\alpha,\beta]$ and $\varphi$ is continuous on $[\alpha,\beta]$ , then $\varphi\circ u$ is integrable on $[a,b]$ (If $f$ is integrable on $[a,b]$ with values in $[m,M]$ and $\varphi$ is continuous on $[m,M]$ , then $\varphi \circ f$ is integrable, Continuity of $f : A \to \mathbb{R}$ at a point of $A$ and on $A$ : the $\varepsilon$ - $\delta$ condition, its agreement with $\lim_{x \to c} f(x) = f(c)$ at a limit point, and continuity at an isolated point).

[L6]

Square roots (Square roots exist: a unique $\sqrt{a} \ge 0$ with $(\sqrt{a})^2 = a$ ; the positives are $\{x^2 : x \neq 0\}$ , Squaring is monotone on the nonnegatives): every $c \ge 0$ has a unique $\sqrt{c} \ge 0$ with $(\sqrt c)^{2} = c$ , and $s \mapsto s^{2}$ is strictly increasing on the nonnegatives, hence injective there.

[L7]

Continuous inverse theorem: a continuous injective function on an order-convex subset of $\mathbb{R}$ is a bijection onto its order-convex image, whose inverse is continuous (Continuous inverse theorem: a continuous injective $f$ on an interval $I$ is a bijection onto the order-convex set $f[I]$ , and the inverse $g : f[I] \to I$ is continuous and strictly monotone in the same sense as $f$ , Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length); and $s \mapsto s^{2}$ is continuous (Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function).

[L8]

Cauchy-Schwarz and the inner product: $\langle u,w\rangle = \sum_{i<m}u_iw_i$ is bilinear and symmetric, $\lVert u\rVert_2 = \sqrt{\langle u,u\rangle}$ , $\lVert u\rVert_2 \ge 0$ , and $|\langle u,w\rangle| \le \lVert u\rVert_2\lVert w\rVert_2$ (The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$ , Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$ , the parallelogram law and polarisation, A norm on a real vector space, the induced metric, and the dictionary with the metric axioms).

[L9]

Laws of finite sums and induction (Laws of finite sums and finite products, Finite sums and finite products, by recursion, The principle of mathematical induction).

[L10]

Order arithmetic: $u > 0$ gives $u^{-1} > 0$ , a product of nonnegatives is nonnegative, and $t \le |t|$ (Inverses of positives are positive, and reciprocation reverses order, Basic properties of the absolute value).

Proof

technique · direct

1.1

If $a = b$ then $\int_a^b f = 0$ and $\int_a^b\lVert f\rVert_2 = 0$ by the oriented convention, so clause 2 reads $0 \le 0$ and holds, while clause 1 says nothing in that case; assume $a < b$ from here on.

1.2

Each component $f_i$ is bounded and integrable on $[a,b]$ , so each $f_i^{2}$ is integrable.

L1L4

1.3

Pointwise, $\langle v, f(t)\rangle \le \bigl|\langle v,f(t)\rangle\bigr| \le \lVert v\rVert_2\,\lVert f(t)\rVert_2$ by Cauchy-Schwarz.

L8L10

2.1

By induction on $p \le m$ , every finite sum $\sum_{i<p} f_i^{2}$ is integrable, the empty sum being the constant $0$ and each successor step adding one integrable function. Hence $g = \sum_{i<m}f_i^{2}$ is integrable.

step 1.2L2L9

2.2

The real-valued function $t \mapsto \langle v, f(t)\rangle = \sum_{i<m}v_i f_i(t)$ is integrable, being a finite sum of scalar multiples of the integrable $f_i$ , and by linearity applied $m$ times $\int_a^b \langle v,f\rangle = \sum_{i<m} v_i\int_a^b f_i = \sum_{i<m}v_i\,v_i = \langle v,v\rangle = \lVert v\rVert_2^{2}$ .

step 1.2L1L2L8L9

3.1

$g(t) \ge 0$ for every $t$ , being a finite sum of squares, and $g$ is bounded above: each $|f_i|$ is bounded by some $B_i$ , so $g(t) \le \sum_{i<m}B_i^{2} =: K$ . Thus $g$ takes its values in $[0,K]$ .

step 2.1L1L9L10

4.1

The map $s \mapsto s^{2}$ is continuous and injective on the order-convex set $[0,\sqrt K]$ , with image $[0,K]$ ; by the continuous inverse theorem its inverse $\varphi : [0,K] \to [0,\sqrt K]$ , $\varphi(u) = \sqrt u$ , is continuous on $[0,K]$ .

step 3.1L6L7

5.1

$\lVert f(t)\rVert_2 = \sqrt{g(t)} = \varphi(g(t))$ for every $t \in [a,b]$ , so $\lVert f\rVert_2 = \varphi \circ g$ is integrable on $[a,b]$ ; this is clause 1.

step 2.1step 3.1step 4.1L5L8

6.1

Both sides of step 1.3 are integrable on $[a,b]$ , so monotonicity and linearity give $\lVert v\rVert_2^{2} = \int_a^b\langle v,f\rangle \le \int_a^b \lVert v\rVert_2\lVert f\rVert_2 = \lVert v\rVert_2\int_a^b\lVert f\rVert_2$ .

step 5.1step 2.2step 1.3L2L3

6.2

If $v = 0$ then $\lVert v\rVert_2 = 0$ , while $\int_a^b\lVert f\rVert_2 \ge 0$ because $\lVert f\rVert_2 \ge 0$ pointwise and $a<b$ ; so clause 2 holds in this case.

step 5.1L3L8

7.1

If $v \ne 0$ then $\lVert v\rVert_2 > 0$ , so multiplying the inequality of step 6.1 by the positive $1/\lVert v\rVert_2$ gives $\lVert v\rVert_2 \le \int_a^b\lVert f\rVert_2$ , which is clause 2 in this case.

step 6.1L8L10

8.1

The two cases of steps 6.2 and 7.1 exhaust the possibilities for $v$ , so clause 2 holds; with step 5.1 both clauses are proved.

step 5.1step 6.2step 7.1∎

Remarks

The case split at $v = 0$ is mandatory. Step 6.1 delivers only $\lVert v\rVert_2^{2} \le \lVert v\rVert_2 \int_a^b\lVert f\rVert_2$ , and dividing by $\lVert v\rVert_2$ is illegitimate when that number is $0$ . Many textbook presentations divide without comment; the missing case is genuinely separate, and it is the one where the right-hand side has to be shown nonnegative on its own.
Why the inner-product route rather than a componentwise estimate. Bounding each coordinate of $\int_a^b f$ separately and reassembling gives a constant depending on $m$ ; the argument above gives the sharp inequality with no constant, and it uses only bilinearity, Cauchy-Schwarz and monotonicity of the integral. The companion page checks the inequality numerically on an explicit curve and shows it is strict there.
Clause 1 is where the hypotheses of If $f$ is integrable on $[a,b]$ with values in $[m,M]$ and $\varphi$ is continuous on $[m,M]$ , then $\varphi \circ f$ is integrable are checked, one by one: $g$ is integrable, its values lie in a closed bounded interval, and the outer function is continuous on that interval. The order of that theorem's hypotheses matters — continuous after integrable — and it is respected here.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 217 results over 34 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

Riemann integral (Wikipedia) (standard reference, not scraped)
Cauchy-Schwarz inequality (Wikipedia) (standard reference, not scraped)
Stephen Semmes, Some Basic Topics in Analysis, Sections 8.1.2–8.1.3 (standard reference, not scraped)
Robert Gressman, Advanced Analysis, Integrating Vector-Valued Functions; Jensen's Inequality (standard reference, not scraped)