TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-29

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.

Bonnet's second mean value theorem: for $f$ monotone and $g$ integrable on $[a, b]$ there is $ξ \in [a, b]$ with $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g$

Statement

Let $a < b$ be reals, let $f : [a, b] \to R$ be monotone, that is nondecreasing or nonincreasing (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences), and let $g : [a, b] \to R$ be integrable (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$ ). Then $f g$ is integrable and there is $ξ \in [a, b]$ with

$\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g + f (b) \int_{ξ}^{b} g .$

No differentiability and no continuity of $f$ is assumed. A monotone function may be discontinuous at infinitely many points and is still integrable (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ ), and the proof below uses only that its increments over the subintervals of a partition all have the same sign. This is the general form; the version usually proved by integration by parts needs $f$ continuously differentiable, which is a strictly stronger hypothesis.

Facts & Assumptions

Given: Reals $a < b$ , a monotone $f : [a, b] \to R$ , an integrable $g : [a, b] \to R$ , and a real $ε > 0$ . Write $G (x) : = \int_{a}^{x} g$ for the integral function of $g$ , and fix a real $K \geq 0$ with $∣ g (t) ∣ \leq K$ for every $t \in [a, b]$ .

[L1]

A monotone function on $[a, b]$ is bounded and integrable there (A monotone function on $[a, b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $∣ f (b) - f (a) ∣ (b - a) / ι (N)$ , Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences, Lower bound, bounded below, bounded set); an integrable function is bounded, so $K$ exists (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} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ ).

[L2]

Products of integrable functions are integrable, as are absolute values, and $∣ \int_{p}^{q} u ∣ \leq \int_{p}^{q} ∣ u ∣$ for $p \leq q$ (If $f, g$ are integrable on $[a, b]$ then so are $∣ f ∣$ , $f^{2}$ , $f g$ , $\max (f, g)$ and $\min (f, g)$ , and $∣ \int_{a}^{b} f ∣ \leq \int_{a}^{b} ∣ f ∣$ ).

[L3]

$G$ is defined on $[a, b]$ , $G (a) = 0$ , $G (y) - G (x) = \int_{x}^{y} g$ for all $x, y \in [a, b]$ in either order, and $G$ is continuous on $[a, b]$ (The integral function $F (x) : = \int_{a}^{x} f$ of an integrable $f$ , The integral function of a bounded integrable $f$ is Lipschitz, hence uniformly continuous, 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$ , The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ , Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

[L4]

$[a, b]$ is compact and nonempty, so a continuous real function on it attains a minimum and a maximum, and its image is exactly the closed interval between them (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, Open cover, subcover, compact subset of $R$ (every open cover has a finite subcover), and sequentially compact subset, Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value, The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval, Maximum and minimum of a set, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L5]

Abel summation by parts: with $A_{j} = \sum_{k < j} α_{k}$ , for every $n \geq 1$ one has $\sum_{k < n} α_{k} β_{k} = A_{n} β_{n - 1} - \sum_{k < n - 1} A_{k + 1} (β_{k + 1} - β_{k})$ (Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ , Series, partial sums, convergence and the sum, divergence, and the tail series).

[L6]

Finite sums: additivity, scaling, splitting with the shift $\sum_{k = p}^{q - 1} x_{k} = \sum_{j < q - p} x_{p + j}$ , monotonicity in the terms, and telescoping $\sum_{k < n} (c_{k + 1} - c_{k}) = c_{n} - c_{0}$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L7]

For a partition $P = (n, t)$ of $[a, b]$ : $n \geq 1$ , $t_{0} = a$ , $t_{k} = b$ for $k \geq n$ , $Δ_{i} = t_{i + 1} - t_{i} > 0$ for $i < n$ , $I_{i} = [t_{i}, t_{i + 1}] \subseteq [a, b]$ , and $U (f, P) - L (f, P) = \sum_{i < n} (M_{i} - m_{i}) Δ_{i}$ with $m_{i} \leq f (x) \leq M_{i}$ for $x \in I_{i}$ (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, 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} Δ_{i}$ and $U (f, P) = \sum_{i} M_{i} Δ_{i}$ ).

[L8]

Riemann's criterion for the integrable $f$ : for every real $η > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < η$ (Riemann's criterion: a bounded $f$ on $[a, b]$ is Darboux integrable if and only if for every real $ε > 0$ there is a partition $P$ with $U (f, P) - L (f, P) < ε$ ).

[L9]

Linearity and monotonicity of the integral, and $\int_{p}^{q} c = c (q - p)$ for a constant (Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ , If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ ).

[L10]

Absolute value and ordered-field arithmetic: $- c \leq x \leq c$ is equivalent to $∣ x ∣ \leq c$ , multiplying an inequality by a positive real preserves it and by a negative real reverses it, the order is total and transitive, and a real that is $\leq M + η$ for every real $η > 0$ is $\leq M$ (Basic properties of the absolute value, Absolute value in an ordered field, Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct

1.1

$f$ is bounded and integrable by [L1], so $f g$ is integrable by [L2]; put $Ψ (x) : = \int_{a}^{x} f g$ , so $Ψ (b) = \int_{a}^{b} f g$ and $Ψ (y) - Ψ (x) = \int_{x}^{y} f g$ by [L3] applied to $f g$ .

givenL1L2L3

1.2

$G$ is continuous on $[a, b]$ , so by [L4] there are $m \leq M$ with $G [[a, b]] = [m, M]$ , $m = \min G [[a, b]]$ and $M = \max G [[a, b]]$ .

L3L4choose

1.3

Put $C : = f (b) - f (a)$ and, for a partition $P = (n, t)$ of $[a, b]$ , put $d_{j} : = f (t_{j + 1}) - f (t_{j})$ for $j < n$ . By [L6], $\sum_{j < n} d_{j} = f (t_{n}) - f (t_{0}) = C$ ; and all the $d_{j}$ are $\geq 0$ when $f$ is nondecreasing and all are $\leq 0$ when $f$ is nonincreasing, by [L7] and Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of $R$ , with the dictionary to monotone sequences.

givenL6L7construct

2.1

The case $C = 0$ . Then $f (a) = f (b)$ , and monotonicity forces $f (x) = f (a)$ for every $x \in [a, b]$ , since $f (x)$ lies between $f (a)$ and $f (b)$ ; so $\int_{a}^{b} f g = f (a) \int_{a}^{b} g$ by [L9], while the right-hand side at $ξ : = a$ is $f (a) \cdot 0 + f (b) \int_{a}^{b} g = f (a) \int_{a}^{b} g$ by [L3]. The theorem holds with $ξ = a$ .

step 1.1step 1.3L3L9L10

2.2

Abel summation on a partition. Let $P = (n, t)$ be any partition of $[a, b]$ . Apply [L5] with $α_{k} : = G (t_{k + 1}) - G (t_{k})$ and $β_{k} : = f (t_{k + 1})$ , noting $t_{k} \in [a, b]$ for every $k \in N$ by [L7]. By [L6], $A_{j} = \sum_{k < j} (G (t_{k + 1}) - G (t_{k})) = G (t_{j}) - G (t_{0}) = G (t_{j})$ , since $G (a) = 0$ .

step 1.2L3L5L6L7

2.3

$S (P)$ approximates $\int_{a}^{b} f g$ . For $k < n$ one has $G (t_{k + 1}) - G (t_{k}) = \int_{t_{k}}^{t_{k + 1}} g$ by [L3], so by [L9] the $k$ -th term of $Ψ (t_{k + 1}) - Ψ (t_{k}) - f (t_{k + 1}) (G (t_{k + 1}) - G (t_{k}))$ equals $\int_{t_{k}}^{t_{k + 1}} (f - f (t_{k + 1})) g$ .

step 1.1L3L9

3.1

So, writing $S (P) : = \sum_{k < n} (G (t_{k + 1}) - G (t_{k})) f (t_{k + 1})$ , [L5] gives $S (P) = G (t_{n}) f (t_{n}) - \sum_{k < n - 1} G (t_{k + 1}) (f (t_{k + 2}) - f (t_{k + 1})) = G (b) f (b) - \sum_{k < n - 1} x_{k + 1}$ , where $x_{j} : = G (t_{j}) d_{j}$ .

step 2.2L5L7construct

3.2

For $x \in I_{k}$ both $f (x)$ and $f (t_{k + 1})$ lie in $[m_{k}, M_{k}]$ , so $∣ (f (x) - f (t_{k + 1})) g (x) ∣ \leq K (M_{k} - m_{k})$ ; hence by [L2] and [L9], $- K (M_{k} - m_{k}) Δ_{k} \leq \int_{t_{k}}^{t_{k + 1}} (f - f (t_{k + 1})) g \leq K (M_{k} - m_{k}) Δ_{k}$ .

step 2.3givenL2L7L9L10

4.1

By [L6], $\sum_{j < n} x_{j} = x_{0} + \sum_{k < n - 1} x_{k + 1}$ , and $x_{0} = G (t_{0}) d_{0} = G (a) d_{0} = 0$ ; so, putting $T (P) : = \sum_{j < n} G (t_{j}) d_{j}$ , step 3.1 reads $S (P) = G (b) f (b) - T (P)$ .

step 3.1L3L6construct

4.2

Summing over $k < n$ with [L6], and telescoping $\sum_{k < n} (Ψ (t_{k + 1}) - Ψ (t_{k})) = Ψ (b) - Ψ (a) = \int_{a}^{b} f g$ , gives $∣ \int_{a}^{b} f g - S (P) ∣ \leq K (U (f, P) - L (f, P))$ .

step 1.1step 2.3step 3.2L6L7L10

5.1

$T (P)$ is $λ_{P} C$ for some $λ_{P} \in [m, M]$ , when $C \neq 0$ . By step 1.2, $m \leq G (t_{j}) \leq M$ for every $j$ . If $f$ is nondecreasing then $d_{j} \geq 0$ , so $m d_{j} \leq G (t_{j}) d_{j} \leq M d_{j}$ , and summing with [L6] and step 1.3 gives $m C \leq T (P) \leq M C$ with $C \geq 0$ ; if $f$ is nonincreasing then $d_{j} \leq 0$ , so $M d_{j} \leq G (t_{j}) d_{j} \leq m d_{j}$ , and summing gives $M C \leq T (P) \leq m C$ with $C \leq 0$ . Dividing by $C$ in the first case, and by the negative $C$ with the inequalities reversed in the second, gives $m \leq T (P) / C \leq M$ in both.

step 1.2step 1.3step 4.1L6L10construct

6.1

The case $C \neq 0$ . Put $λ : = (G (b) f (b) - \int_{a}^{b} f g) / C$ . By step 4.1, $\int_{a}^{b} f g - S (P) = \int_{a}^{b} f g - G (b) f (b) + T (P) = (λ_{P} - λ) C$ for every partition $P$ , where $λ_{P} = T (P) / C$ .

step 4.1step 5.1L10construct

7.1

By [L8] fix a partition $P$ with $U (f, P) - L (f, P) < ε ∣ C ∣ / (K + 1)$ , a positive real; then step 4.2 and step 6.1 give $∣ λ_{P} - λ ∣ ∣ C ∣ \leq K (U (f, P) - L (f, P)) < ε ∣ C ∣$ , so $∣ λ_{P} - λ ∣ < ε$ .

step 4.2step 6.1L8L10choose

8.1

Since $m \leq λ_{P} \leq M$ by step 5.1, it follows that $m - ε < λ < M + ε$ ; as $ε > 0$ was arbitrary, $m \leq λ \leq M$ .

step 5.1step 7.1L10

9.1

By step 1.2, $G [[a, b]] = [m, M]$ , so there is $ξ \in [a, b]$ with $G (ξ) = λ$ .

step 1.2step 8.1L4choose

10.1

Then $\int_{a}^{b} f g = G (b) f (b) - λ C = f (b) G (b) - G (ξ) (f (b) - f (a)) = f (a) G (ξ) + f (b) (G (b) - G (ξ))$ , and $G (ξ) = \int_{a}^{ξ} g$ with $G (b) - G (ξ) = \int_{ξ}^{b} g$ by [L3]; this is the stated identity.

step 6.1step 9.1L3algebra

11.1

The cases $C = 0$ and $C \neq 0$ are exhaustive, so the theorem holds in both.

step 2.1step 10.1L10∎

Remarks

The published summation-by-parts lemma was matched to its own indexing before it was used. Abel summation by parts: with $A_{n} = \sum_{k < n} a_{k}$ one has $\sum_{k < n} a_{k} b_{k} = A_{n} b_{n - 1} - \sum_{k < n - 1} A_{k + 1} (b_{k + 1} - b_{k})$ for every $n \geq 1$ reads $\sum_{k < n} α_{k} β_{k} = A_{n} β_{n - 1} - \sum_{k < n - 1} A_{k + 1} (β_{k + 1} - β_{k})$ with $A_{j} = \sum_{k < j} α_{k}$ , so $A_{0} = 0$ and the boundary value is $β_{n - 1}$ , not $β_{n}$ . Taking $β_{k} : = f (t_{k + 1})$ rather than $f (t_{k})$ is what makes that boundary value $f (t_{n}) = f (b)$ ; and the shifted sum on the right is a sum over $j = 1, \dots, n - 1$ whose missing $j = 0$ term is $G (t_{0}) d_{0} = 0$ , because the integral function vanishes at its base point. Both observations are step 3.1 and step 4.1, and the theorem would be off by a term without either.
The passage to the limit is an estimate, not a Riemann-sum convergence theorem. Step 4.2 bounds $∣ \int_{a}^{b} f g - S (P) ∣$ by $K (U (f, P) - L (f, P))$ for every partition, and the integrability of $f$ alone drives the right-hand side to $0$ . No tagged partition, no mesh condition and no appeal to The Darboux and Riemann definitions agree: a bounded $f$ on $[a, b]$ is Darboux integrable with integral $I$ if and only if for every real $ε > 0$ there is a real $δ > 0$ such that $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged partition of mesh below $δ$ is involved, and the approximating sums are not Riemann sums of $f g$ .
What is not proved here. Nothing is claimed about $ξ$ lying in the open interval, and nothing about the sharper form in which $f$ is assumed nonnegative and nonincreasing, where the conclusion becomes $\int_{a}^{b} f g = f (a) \int_{a}^{ξ} g$ . That refinement needs the one-sided normalisation of $f$ at $a$ and is not used anywhere on this page.

Depends on

Used by

Dependency tree · two levels

86 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Mean value theorem (Wikipedia) (standard reference, not scraped)
Summation by parts (Wikipedia) (standard reference, not scraped)
Encyclopedia of Mathematics, Lebesgue integral (standard reference, not scraped)

Bonnet's second mean value theorem: for ff monotone and gg integrable on [a,b][a,b] there is ξ∈[a,b]ξ∈[a,b] with ∫abfg=f(a)∫aξg+f(b)∫ξbg∫ab​fg=f(a)∫aξ​g+f(b)∫ξb​g