Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

A monotone function on [a,b][a,b] is Riemann integrable: for the uniform partition into NN parts the upper minus lower sum telescopes to f(b)f(a)(ba)/ι(N)|f(b) - f(a)|\,(b-a)/\iota(N)

Statement

Let a<ba < b be reals and let f:[a,b]Rf : [a,b] \to \mathbb{R} be monotone, that is nondecreasing or nonincreasing on [a,b][a,b] (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R\mathbb{R}, with the dictionary to monotone sequences). Then ff is bounded (Lower bound, bounded below, bounded set) and Riemann integrable on [a,b][a,b] (The lower and upper Darboux integrals of a bounded ff on [a,b][a,b] as supPL(f,P)\sup_P L(f,P) and infPU(f,P)\inf_P U(f,P), Darboux integrability as their equality, and the notation abf\int_a^b f).

Moreover, for the uniform partition UNU_N of [a,b][a,b] into N1N \ge 1 parts (Partition of [a,b][a,b] as a finite strictly increasing list a=t0<t1<<tn=ba = t_0 < t_1 < \dots < t_n = b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions),

U(f,UN)L(f,UN)  =  f(b)f(a)baι(N),U(f,U_N) - L(f,U_N) \;=\; \bigl|f(b) - f(a)\bigr| \cdot \frac{b-a}{\iota(N)} ,

where ι(N)\iota(N) is the canonical natural of NN in R\mathbb{R} (The canonical natural ι(n)=n1F\iota(n) = n \cdot 1_F of a field). The right-hand side is an equality, not an estimate: the sum i<N(Mimi)\sum_{i<N}(M_i - m_i) telescopes exactly, because on each subinterval a monotone function attains its extremes at the two endpoints.

No continuity is assumed, and none holds in general: a nondecreasing function may be discontinuous at every rational (Converse to Froda: for every at most countable ERE \subseteq \mathbb{R} there is a bounded nondecreasing f:RRf : \mathbb{R} \to \mathbb{R} whose set of discontinuities is exactly EE, every one of them a jump), and the companion page of this pair works out the integral of the floor function, the simplest discontinuous monotone integrand.

Facts & Assumptions

Given: Reals a<ba < b and a monotone f:[a,b]Rf : [a,b] \to \mathbb{R}. Let N1N \ge 1 be a natural number and let UN=(N,t)U_N = (N,t) be the uniform partition of [a,b][a,b] into NN parts, with subintervals Ii=[ti,ti+1]I_i = [t_i,t_{i+1}] and lengths Δi=(ba)/ι(N)\Delta_i = (b-a)/\iota(N) for i<Ni < N.

[L1]

ff is nondecreasing, meaning f(x)f(y)f(x) \le f(y) whenever xyx \le y in [a,b][a,b], or nonincreasing, meaning f(x)f(y)f(x) \ge f(y) whenever xyx \le y; these two cases are what "monotone" means and they exhaust it (Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of R\mathbb{R}, with the dictionary to monotone sequences).

[L2]

For the uniform partition: t0=at_0 = a, tN=bt_N = b, ti<ti+1t_i < t_{i+1}, every Δi=(ba)/ι(N)>0\Delta_i = (b-a)/\iota(N) > 0, and i<NΔi=ba\sum_{i<N}\Delta_i = b-a (Partition of [a,b][a,b] as a finite strictly increasing list a=t0<t1<<tn=ba = t_0 < t_1 < \dots < t_n = b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions).

[L3]

If a nonempty set SRS \subseteq \mathbb{R} has a greatest element then that element is supS\sup S, and if it has a least element then that element is infS\inf S (Maximum and minimum of a set, Greatest lower bound (infimum), Complete ordered field (least-upper-bound property)).

[L5]

Finite sums: scaling and telescoping, i<N(ci+1ci)=cNc0\sum_{i<N}(c_{i+1}-c_i) = c_N - c_0 (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

[L6]

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

[L8]

Ordered-field arithmetic and the absolute value: adding a constant and multiplying by a positive quantity preserve an inequality; the order is total and transitive; x=x|x| = x for x0x \ge 0 and x=x|x| = -x for x0x \le 0 (Basic properties of the absolute value, Order is preserved by adding a constant and by adding inequalities, Sign rules for products and monotonicity of multiplication, Ordered field, Complete ordered field (least-upper-bound property), Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length). 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 · cases
1.1

By [L1] there are two cases, ff nondecreasing and ff nonincreasing, and they exhaust the hypothesis. Every x[a,b]x \in [a,b] satisfies axba \le x \le b (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length).

givenL1cases
1.2

Case: ff is nondecreasing. Then f(a)f(x)f(b)f(a) \le f(x) \le f(b) for every x[a,b]x \in [a,b], so ff is bounded by [L8]; and for i<Ni < N and xIix \in I_i one has tixti+1t_i \le x \le t_{i+1}, hence f(ti)f(x)f(ti+1)f(t_i) \le f(x) \le f(t_{i+1}). Since f(ti)f(t_i) and f(ti+1)f(t_{i+1}) themselves lie in f[Ii]f[I_i], they are its least and greatest elements, so mi=f(ti)m_i = f(t_i) and Mi=f(ti+1)M_i = f(t_{i+1}) by [L3].

assume-case upgivenL2L3L8
1.3

Case: ff is nonincreasing. Then f(b)f(x)f(a)f(b) \le f(x) \le f(a) for every x[a,b]x \in [a,b], so ff is bounded; and for i<Ni < N and xIix \in I_i one has f(ti+1)f(x)f(ti)f(t_{i+1}) \le f(x) \le f(t_i), so mi=f(ti+1)m_i = f(t_{i+1}) and Mi=f(ti)M_i = f(t_i) by [L3].

assume-case downgivenL2L3L8
2.1

In the nondecreasing case, Mimi=f(ti+1)f(ti)M_i - m_i = f(t_{i+1}) - f(t_i), so by [L4], [L2] and [L5], U(f,UN)L(f,UN)=i<N(f(ti+1)f(ti))baι(N)=baι(N)(f(tN)f(t0))=baι(N)(f(b)f(a))U(f,U_N) - L(f,U_N) = \sum_{i<N}\bigl(f(t_{i+1}) - f(t_i)\bigr)\frac{b-a}{\iota(N)} = \frac{b-a}{\iota(N)}\bigl(f(t_N) - f(t_0)\bigr) = \frac{b-a}{\iota(N)}\bigl(f(b) - f(a)\bigr), and f(b)f(a)0f(b) - f(a) \ge 0, so this equals f(b)f(a)(ba)/ι(N)|f(b)-f(a)|(b-a)/\iota(N) by [L8].

step 1.2L2L4L5L8
2.2

In the nonincreasing case the same computation gives U(f,UN)L(f,UN)=baι(N)(f(a)f(b))U(f,U_N) - L(f,U_N) = \frac{b-a}{\iota(N)}\bigl(f(a) - f(b)\bigr) with f(a)f(b)0f(a) - f(b) \ge 0, which is again f(b)f(a)(ba)/ι(N)|f(b)-f(a)|(b-a)/\iota(N) by [L8]. The two cases of step 1.1 exhaust the hypothesis, so the displayed identity holds for every monotone ff, which is also bounded.

step 1.3L2L4L5L8cases-exhaustive
3.1

Let a real ε>0\varepsilon > 0 be given and put η:=ε((f(b)f(a)+1)(ba))1\eta := \varepsilon \cdot \bigl((|f(b)-f(a)| + 1)(b-a)\bigr)^{-1}, a positive real by [L8]. By [L7] fix a natural N1N \ge 1 with 1/ι(N)<η1/\iota(N) < \eta.

step 2.2L7L8choose
4.1

Then U(f,UN)L(f,UN)=f(b)f(a)(ba)/ι(N)(f(b)f(a)+1)(ba)/ι(N)<(f(b)f(a)+1)(ba)η=εU(f,U_N) - L(f,U_N) = |f(b)-f(a)|\,(b-a)/\iota(N) \le (|f(b)-f(a)|+1)(b-a)/\iota(N) < (|f(b)-f(a)|+1)(b-a)\,\eta = \varepsilon: the first inequality because (ba)/ι(N)>0(b-a)/\iota(N) > 0 and f(b)f(a)f(b)f(a)+1|f(b)-f(a)| \le |f(b)-f(a)|+1, and the second because (f(b)f(a)+1)(ba)>0(|f(b)-f(a)|+1)(b-a) > 0 and 1/ι(N)<η1/\iota(N) < \eta. So U(f,UN)L(f,UN)<εU(f,U_N) - L(f,U_N) < \varepsilon.

step 2.1step 2.2step 3.1L8
5.1

Since the real ε>0\varepsilon > 0 was arbitrary and step 4.1 produced a partition with UL<εU - L < \varepsilon, criterion [L6] applies: ff is bounded by steps 1.2 and 1.3 and Riemann integrable on [a,b][a,b].

step 1.2step 1.3step 4.1L6

Remarks

Depends on

Used by

Dependency tree · next 3 levels

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