LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-09 (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.

If $m \le f \le M$ on $[a,b]$ then $m(b-a) \le L(f,P) \le \underline{\int_a^b} f \le \overline{\int_a^b} f \le U(f,P) \le M(b-a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_a^b c = c(b-a)$

Statement

Let $a < b$ be reals and let $f : [a,b] \to \mathbb{R}$ satisfy

$m \;\le\; f(x) \;\le\; M \qquad \text{for every } x \in [a,b],$

with $m, M$ real. Then $f$ is bounded (Lower bound, bounded below, bounded set), so its Darboux sums and integrals are defined (For bounded $f$ on $[a,b]$ and a partition $P$ : the infimum $m_i$ and supremum $M_i$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L(f,P) = \sum_i m_i \Delta_i$ and $U(f,P) = \sum_i M_i \Delta_i$ , 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$ ), and for every partition $P$ of $[a,b]$ (Partition of $[a,b]$ as a finite strictly increasing list $a = t_0 < t_1 < \dots < t_n = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions)

$m(b-a) \;\le\; L(f,P) \;\le\; \underline{\int_a^b} f \;\le\; \overline{\int_a^b} f \;\le\; U(f,P) \;\le\; M(b-a) .$

In particular, taking $f$ to be the constant function with value $c$ :

$\int_a^b c \;=\; c\,(b-a) ,$

the constant function being integrable, with $L(f,P) = U(f,P) = c(b-a)$ for every partition $P$ .

Facts & Assumptions

Given: Reals $a < b$ , reals $m \le M$ , and $f : [a,b] \to \mathbb{R}$ with $m \le f(x) \le M$ for every $x \in [a,b]$ . Let $P = (n,t)$ be a partition of $[a,b]$ , with subintervals $I_i$ and lengths $\Delta_i$ for $i < n$ .

[L1]

$\sum_{i<n}\Delta_i = b - a$ , every $\Delta_i > 0$ , and $n \ge 1$ ; each $I_i$ is a nonempty subset of $[a,b]$ (Partition of $[a,b]$ as a finite strictly increasing list $a = t_0 < t_1 < \dots < t_n = b$ , its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions, Intervals of $\mathbb{R}$ : the nine order-convex forms, nondegeneracy, and length).

[L2]

$m_i = \inf f[I_i]$ and $M_i = \sup f[I_i]$ exist, $L(f,P) = \sum_{i<n}m_i\Delta_i$ and $U(f,P) = \sum_{i<n}M_i\Delta_i$ , and $m_i \le f(x) \le M_i$ for $x \in I_i$ (For bounded $f$ on $[a,b]$ and a partition $P$ : the infimum $m_i$ and supremum $M_i$ of $f$ on the $i$ -th subinterval, and the lower and upper Darboux sums $L(f,P) = \sum_i m_i \Delta_i$ and $U(f,P) = \sum_i M_i \Delta_i$ ).

[L3]

$L(f,P) \le \underline{\int_a^b} f \le \overline{\int_a^b} f \le U(f,P)$ for every partition $P$ ; $f$ is integrable exactly when the two integrals are equal, and then $\int_a^b f$ is their common value (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$ ).

[L4]

An infimum is the greatest lower bound and a supremum the least upper bound; a set with a single element has that element as both (Greatest lower bound (infimum), Complete ordered field (least-upper-bound property), Maximum and minimum of a set).

[L5]

Finite sums: scaling, monotonicity in the terms, and $\sum_{i<n}\lambda\,\Delta_i = \lambda\sum_{i<n}\Delta_i$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L6]

Ordered-field arithmetic: multiplying an inequality by a positive quantity preserves it, adding a constant preserves it, and the order is transitive; $|x| \le \max\{|m|,|M|\}$ whenever $m \le x \le M$ (Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Basic properties of the absolute value, Ordered field, Complete ordered field (least-upper-bound property)). These order-arithmetic facts are stated by their sources for the strict order only; the nonstrict forms used below follow by adjoining the equality case, in which the two sides coincide.

Proof

technique · direct

1.1

$f$ is bounded: $|f(x)| \le \max\{|m|,|M|\}$ for every $x \in [a,b]$ by [L6], so the Darboux sums and integrals of [L2] and [L3] are defined.

givenL6

1.2

For every $i < n$ : $m$ is a lower bound of $f[I_i]$ and $M$ an upper bound, since $I_i \subseteq [a,b]$ ; the set $f[I_i]$ is nonempty by [L1]. Hence $m \le m_i$ and $M_i \le M$ by [L4].

givenL1L2L4

1.3

The constant case, treated on its own. Suppose in addition that $f$ is the constant function with value $c$ , that is $f(x) = c$ for every $x \in [a,b]$ ; the general argument below does not use this supposition. Then $f[I_i] = \{c\}$ for every $i < n$ by [L1], so $m_i = M_i = c$ by [L4], and $L(f,P) = U(f,P) = \sum_{i<n} c\,\Delta_i = c(b-a)$ by [L5] and [L1].

L1L2L4L5

2.1

$L(f,P) \ge m(b-a)$ : by step 1.2 and $\Delta_i > 0$ one has $m_i\Delta_i \ge m\Delta_i$ for every $i < n$ , so monotonicity and scaling in [L5] give $L(f,P) \ge \sum_{i<n} m\,\Delta_i = m\sum_{i<n}\Delta_i = m(b-a)$ by [L1].

step 1.2L1L5L6

2.2

$U(f,P) \le M(b-a)$ : the same argument with $M_i \le M$ gives $U(f,P) \le \sum_{i<n}M\,\Delta_i = M(b-a)$ .

step 1.2L1L5L6

3.1

Combining steps 2.1 and 2.2 with the chain of [L3] gives the displayed five-term inequality for every partition $P$ .

step 2.1step 2.2L3

4.1

Hence, still under the supposition of step 1.3 that $f$ is constant with value $c$ , the set of lower sums and the set of upper sums are both $\{c(b-a)\}$ , so $\underline{\int_a^b} f = \overline{\int_a^b} f = c(b-a)$ by [L4], $f$ is integrable, and $\int_a^b c = c(b-a)$ by [L3].

step 1.3L3L4∎

Remarks

The five-term chain is the only estimate most of this page needs. Every integrability proof below produces one partition and controls $U(f,P) - L(f,P)$ ; the chain then locates both integrals inside an interval of that length, and Riemann's criterion: a bounded $f$ on $[a,b]$ is Darboux integrable if and only if for every real $\varepsilon > 0$ there is a partition $P$ with $U(f,P) - L(f,P) < \varepsilon$ turns the observation into an equivalence.
The bounds are sharp, but equality does not characterize constants. Constant functions show that neither outer coefficient can be improved. Nonconstant functions can also attain equality: for the Dirichlet indicator on $[0,1]$ , every partition has $L(f,P) = 0$ and $U(f,P) = 1$ , so both outer bounds are equalities.
Nonnegativity, as a special case. If $f \ge 0$ on $[a,b]$ then $m$ may be taken to be $0$ , so $\int_a^b f \ge 0$ whenever the integral exists. A nonnegative integrand with vanishing integral need not vanish, however; that is FALSE: a nonnegative Riemann integrable function on $[a,b]$ with $\int_a^b f = 0$ is identically zero.

Depends on

Used by

Dependency tree · next 3 levels

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

Darboux integral (Wikipedia) (standard reference, not scraped)
W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 6 (standard reference, not scraped)
J. Lebl, Basic Analysis I, The Riemann Integral (standard reference, not scraped)
J. Hunter, Chapter 11: The Riemann Integral (standard reference, not scraped)