Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

The integral function of a bounded integrable f is Lipschitz, hence uniformly continuous

Statement

Let a<b be reals, let f:[a,b]→R be integrable (The lower and upper Darboux integrals of a bounded f on [a,b] as sup⁡PL(f,P) and inf⁡PU(f,P), Darboux integrability as their equality, and the notation ∫abf), let K≥0 be a real with ∣f(t)∣≤K for every t∈[a,b] (Lower bound, bounded below, bounded set), and let F be the integral function of f (The integral function F(x):=∫axf of an integrable f). Then

∣F(y)−F(x)∣  ≤  K ∣y−x∣for all x,y∈[a,b],

that is, F is Lipschitz with constant K on [a,b] (Lipschitz map, α-Hölder map for rational 0<α≤1, and contraction, Dictionary: for A⊆R with the metric d(x,y)=∣x−y∣, continuity and uniform continuity of f:A→R agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of R is compact in the open-cover sense of R exactly when it is a compact metric subspace). Consequently F is uniformly continuous on [a,b] (Uniform continuity of f:A→R: one δ serving every pair of points of A) and hence continuous there (Continuity of f:A→R at a point of A and on A: the ε-δ condition, its agreement with lim⁡x→cf(x)=f(c) at a limit point, and continuity at an isolated point).

No continuity of f is assumed. This is the strongest regularity of F available before the fundamental theorem, and it is what makes the hypotheses of that theorem visible as hypotheses: continuity of f at a point buys differentiability of F there, and integrability alone already buys this much everywhere.

Facts & Assumptions

Given: Reals a<b, an integrable f:[a,b]→R, a real K≥0 with ∣f∣≤K on [a,b], and the integral function F(x)=∫axf; points x,y∈[a,b].

[L1]

F(y)−F(x)=∫xyf for all x,y∈[a,b], in either order (The integral function F(x):=∫axf of an integrable f).

[L2]

∣f∣ is integrable on every [p,q]⊆[a,b] with p<q, and ∣∫pqf∣≤∫pq∣f∣ there (If f,g are integrable on [a,b] then so are ∣f∣, f2, fg, max⁡(f,g) and min⁡(f,g), and ∣∫abf∣≤∫ab∣f∣, claims 1 and 3).

[L4]

With oriented limits, ∫yxf=−∫xyf and ∫xxf=0 (The integral with oriented limits: ∫aaf:=0 and ∫baf:=−∫abf).

[L5]

Absolute value: ∣−t∣=∣t∣, ∣t∣≥0, and ∣t∣≤c follows from −c≤t≤c (Basic properties of the absolute value, Absolute value in an ordered field).

[L7]

Ordered-field arithmetic: the order is total and transitive, and multiplying an inequality by a nonnegative real preserves it (Ordered field, Complete ordered field (least-upper-bound property)).

Proof

technique · direct
1.1

The case x<y. By [L1], F(y)−F(x)=∫xyf, and [x,y]⊆[a,b] with x<y.

givenL1
1.2

The case x=y. Then F(y)−F(x)=0 and K∣y−x∣=0, so the inequality holds with equality.

L1L4L5
2.1

On [x,y] one has ∣f(t)∣≤K for every t, so by [L2] and [L3], ∣∫xyf∣≤∫xy∣f∣≤∫xyK=K (y−x).

step 1.1givenL2L3
3.1

Hence ∣F(y)−F(x)∣≤K(y−x)=K∣y−x∣ when x<y.

step 1.1step 2.1L5
4.1

The case y<x. Applying step 3.1 to the pair (y,x) gives ∣F(x)−F(y)∣≤K∣x−y∣, and ∣F(y)−F(x)∣=∣F(x)−F(y)∣ with ∣y−x∣=∣x−y∣ by [L5]; so the inequality holds here too.

step 3.1L5
5.1

The three cases x<y, x=y, y<x are exhaustive by [L7], so ∣F(y)−F(x)∣≤K∣y−x∣ for all x,y∈[a,b].

step 1.2step 3.1step 4.1L7
6.1

By [L6], F is therefore Lipschitz with constant K on [a,b], hence uniformly continuous on [a,b], hence continuous there.

step 5.1L6∎

Remarks

Depends on

Used by

Dependency tree · two levels

66 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